test/regress/regress3/incorrect1.smtv1.smt2


1
2
3
4
5
6
7
8

(set-option :incremental false)
(set-info :status sat)
(set-logic QF_UFLRA)
(declare-fun f0 (Real Real) Real)
(declare-fun f1 (Real Real) Real)
(declare-fun p0 (Real Real) Bool)
(declare-fun v0 () Real)
(check-sat-assuming ( (let ((_let_0 (f1 v0 v0))) (let ((_let_1 (* (* 6.0 v0) 7.0))) (let ((_let_2 (ite (p0 (/ 6 (- 6)) (/ 7 (- 6))) 1 0))) (let ((_let_3 (+ (/ 7 (- 6)) (* 6.0 v0)))) (let ((_let_4 (/ 6 6))) (let ((_let_5 (+ (/ 6 (- 6)) (/ _let_2 1)))) (let ((_let_6 (+ _let_5 _let_0))) (let ((_let_7 (/ 1 6))) (let ((_let_8 (- _let_3))) (let ((_let_9 (/ 6 (- 1)))) (let ((_let_10 (+ _let_5 _let_5))) (let ((_let_11 (/ 7 6))) (let ((_let_12 (- _let_7 (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))))) (let ((_let_13 (/ 1 (- 6)))) (let ((_let_14 (* 6.0 _let_4))) (let ((_let_15 (* 6.0 (- (/ 7 (- 6)))))) (let ((_let_16 (- _let_15))) (let ((_let_17 (+ _let_6 _let_4))) (let ((_let_18 (ite (p0 (* 6.0 v0) _let_16) 1 0))) (let ((_let_19 (* (- 1) _let_2))) (let ((_let_20 (/ 1 1))) (let ((_let_21 (ite (p0 _let_11 (- (/ 7 (- 6)) _let_0)) 1 0))) (let ((_let_22 (- (* 6.0 v0) (- (- (/ 7 (- 6))))))) (let ((_let_23 (- _let_20 v0))) (let ((_let_24 (- _let_4 (* 6.0 v0)))) (let ((_let_25 (ite (p0 _let_16 _let_8) 1 0))) (let ((_let_26 (+ _let_5 _let_20))) (let ((_let_27 (>= (/ 6 (- 6)) _let_23))) (let ((_let_28 (distinct (/ (- _let_2) 1) _let_3))) (let ((_let_29 (> _let_13 (f1 _let_9 (/ (- _let_2) 1))))) (let ((_let_30 (< _let_14 (/ _let_19 1)))) (let ((_let_31 (>= _let_20 _let_14))) (let ((_let_32 (<= (/ _let_2 1) _let_8))) (let ((_let_33 (>= _let_15 (/ _let_21 1)))) (let ((_let_34 (= (+ (* 6.0 v0) _let_11) (f0 (- v0) (/ _let_19 1))))) (let ((_let_35 (> _let_11 _let_17))) (let ((_let_36 (distinct _let_6 _let_0))) (let ((_let_37 (<= v0 _let_10))) (let ((_let_38 (< _let_15 _let_9))) (let ((_let_39 (> _let_0 _let_4))) (let ((_let_40 (>= _let_9 _let_11))) (let ((_let_41 (< (- (/ 7 (- 6))) _let_14))) (let ((_let_42 (= (+ (/ 7 (- 6)) v0) _let_10))) (let ((_let_43 (= (f1 _let_9 (/ (- _let_2) 1)) (/ (- _let_2) 1)))) (let ((_let_44 (<= (+ (/ 7 (- 6)) v0) (- _let_7)))) (let ((_let_45 (< (/ 7 (- 6)) _let_10))) (let ((_let_46 (p0 _let_5 (- _let_7)))) (let ((_let_47 (= (/ 6 (- 6)) (/ _let_25 1)))) (let ((_let_48 (>= (* (/ (- 6) 1) _let_10) (- (/ 7 (- 6)) _let_0)))) (let ((_let_49 (= (f1 _let_9 (/ (- _let_2) 1)) _let_0))) (let ((_let_50 (>= _let_24 (f0 (- v0) (/ _let_19 1))))) (let ((_let_51 (<= (/ 6 (- 7)) _let_15))) (let ((_let_52 (>= (* (/ (- 6) 1) _let_10) (/ 6 (- 6))))) (let ((_let_53 (<= (f1 _let_9 (/ (- _let_2) 1)) _let_22))) (let ((_let_54 (p0 v0 _let_13))) (let ((_let_55 (< _let_16 (- (- (/ 7 (- 6))))))) (let ((_let_56 (= _let_26 (/ _let_2 1)))) (let ((_let_57 (ite (< _let_9 (/ _let_21 1)) _let_6 (/ 6 (- 6))))) (let ((_let_58 (ite (p0 v0 (* 6.0 v0)) _let_11 (- (- (/ 7 (- 6))))))) (let ((_let_59 (ite _let_28 (f1 _let_9 (/ (- _let_2) 1)) (- _let_7)))) (let ((_let_60 (ite (distinct _let_26 (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) (/ 7 (- 6)) (* (/ (- 6) 1) _let_10)))) (let ((_let_61 (ite _let_46 _let_14 _let_7))) (let ((_let_62 (ite (distinct (/ 6 (- 6)) (/ 6 (- 6))) _let_4 _let_18))) (let ((_let_63 (ite (<= _let_12 (+ (* 6.0 v0) _let_11)) _let_1 (- _let_2)))) (let ((_let_64 (ite _let_44 (- (/ 7 (- 6)) _let_0) _let_22))) (let ((_let_65 (ite (> (/ (- _let_2) 1) _let_20) (+ (* 6.0 v0) _let_11) (f0 (- v0) (/ _let_19 1))))) (let ((_let_66 (ite (distinct (f1 _let_9 (/ (- _let_2) 1)) _let_17) _let_14 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6)))) (let ((_let_67 (ite (>= (f0 (- v0) (/ _let_19 1)) (+ (/ 7 (- 6)) v0)) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) _let_64))) (let ((_let_68 (ite _let_45 _let_24 _let_0))) (let ((_let_69 (ite _let_50 _let_15 (+ (* 6.0 v0) _let_11)))) (let ((_let_70 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (f0 (- v0) (/ _let_19 1)) _let_0))) (let ((_let_71 (ite (p0 (- (/ 7 (- 6)) _let_0) _let_11) _let_8 _let_20))) (let ((_let_72 (ite (< _let_24 (/ 6 (- 6))) v0 _let_66))) (let ((_let_73 (ite (p0 (/ _let_2 1) (/ 7 (- 6))) _let_18 (- (- (/ 7 (- 6))))))) (let ((_let_74 (ite _let_39 _let_4 _let_19))) (let ((_let_75 (ite (p0 _let_1 _let_5) (/ 6 (- 6)) (- v0)))) (let ((_let_76 (ite (<= v0 (/ _let_21 1)) _let_23 (ite (> (/ _let_2 1) _let_9) _let_25 _let_3)))) (let ((_let_77 (ite (distinct _let_26 (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) _let_24))) (let ((_let_78 (ite _let_36 _let_5 (+ (* 6.0 v0) _let_11)))) (let ((_let_79 (ite (= _let_1 (f1 _let_9 (/ (- _let_2) 1))) _let_15 _let_4))) (let ((_let_80 (ite (= _let_15 _let_12) (ite (p0 _let_17 _let_6) _let_0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)))) (let ((_let_81 (ite (= _let_9 (/ _let_25 1)) _let_16 (- (- (/ 7 (- 6))))))) (let ((_let_82 (ite (= _let_12 (- v0)) (- (- (/ 7 (- 6)))) _let_80))) (let ((_let_83 (ite (>= _let_9 (/ _let_25 1)) (ite (= v0 _let_6) _let_21 _let_63) _let_22))) (let ((_let_84 (ite _let_31 _let_80 _let_13))) (let ((_let_85 (ite _let_47 _let_76 (+ (* 6.0 v0) _let_11)))) (let ((_let_86 (ite (= (- v0) (/ 6 (- 6))) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) _let_24))) (let ((_let_87 (ite (> (/ 7 (- 6)) (* 6.0 v0)) _let_59 (ite (>= _let_1 _let_8) (+ (/ 7 (- 6)) v0) _let_19)))) (let ((_let_88 (ite (= (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_1) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)) _let_18))) (let ((_let_89 (ite (p0 (/ 6 (- 7)) (f0 (- v0) (/ _let_19 1))) _let_17 _let_74))) (let ((_let_90 (ite _let_54 (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1))) _let_0))) (let ((_let_91 (ite (distinct (/ _let_18 1) (+ (/ 7 (- 6)) v0)) (ite (<= (- _let_7) _let_14) (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (p0 _let_17 _let_6) _let_0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6))) (ite (>= _let_1 _let_8) (+ (/ 7 (- 6)) v0) _let_19)))) (let ((_let_92 (ite (>= _let_14 _let_0) (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65) _let_20))) (let ((_let_93 (ite _let_27 _let_7 (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13)))) (let ((_let_94 (ite (> (/ _let_2 1) _let_10) (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) _let_12 (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0))))) (let ((_let_95 (ite (distinct _let_4 (/ (- _let_2) 1)) _let_84 (/ 6 (- 6))))) (let ((_let_96 (ite (> _let_15 _let_4) _let_89 _let_18))) (let ((_let_97 (ite (>= (* (/ (- 6) 1) _let_10) _let_4) (ite (> _let_3 _let_12) _let_24 _let_2) (ite (> _let_5 _let_4) _let_22 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6)))))))) (let ((_let_98 (ite (> _let_10 _let_14) _let_93 (- (/ 7 (- 6)) _let_0)))) (let ((_let_99 (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) _let_79 (- _let_7)))) (let ((_let_100 (ite (distinct v0 (/ 6 (- 6))) _let_4 (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)))))) (let ((_let_101 (ite _let_27 _let_83 (ite (> (/ 7 (- 6)) _let_16) (- (/ 7 (- 6))) (ite _let_53 (- v0) _let_62))))) (let ((_let_102 (ite (>= (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) (- _let_7)) (/ 7 (- 6)) _let_22))) (let ((_let_103 (ite (p0 _let_5 _let_0) (ite (>= (f0 (- v0) (/ _let_19 1)) (+ (/ 7 (- 6)) v0)) _let_4 _let_82) (ite (p0 (/ _let_25 1) _let_8) _let_58 _let_16)))) (let ((_let_104 (ite (> _let_15 _let_4) _let_79 (ite (> (/ _let_19 1) _let_15) _let_80 (ite (p0 _let_26 _let_14) _let_9 (- _let_2)))))) (let ((_let_105 (ite (<= (- (/ 7 (- 6))) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) (ite (<= (/ _let_25 1) _let_16) _let_24 _let_82) (ite _let_37 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0)))))) (let ((_let_106 (ite _let_52 _let_60 _let_105))) (let ((_let_107 (ite (< (- (- (/ 7 (- 6)))) _let_11) (- _let_2) _let_57))) (let ((_let_108 (ite (< _let_23 _let_24) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65) (ite _let_29 _let_17 v0)))) (let ((_let_109 (ite (>= _let_11 (- v0)) _let_23 (ite (<= (- _let_7) _let_14) _let_20 _let_13)))) (let ((_let_110 (ite (> (- v0) (- (/ 7 (- 6)) _let_0)) (ite _let_44 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_20) (ite _let_51 _let_83 _let_63)))) (let ((_let_111 (ite (distinct _let_1 (/ _let_18 1)) _let_10 (* (/ (- 6) 1) _let_10)))) (let ((_let_112 (ite (>= (- v0) _let_13) _let_110 _let_108))) (let ((_let_113 (ite (p0 _let_22 (/ _let_25 1)) _let_97 _let_103))) (let ((_let_114 (ite (= _let_13 (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0) _let_83))) (let ((_let_115 (ite _let_49 _let_92 _let_75))) (let ((_let_116 (ite (p0 _let_15 (/ (- _let_2) 1)) _let_61 _let_103))) (let ((_let_117 (ite _let_32 (ite (>= _let_1 _let_8) (+ (/ 7 (- 6)) v0) _let_19) (ite (>= _let_11 _let_10) _let_80 _let_3)))) (let ((_let_118 (ite _let_30 (/ 6 (- 6)) _let_58))) (let ((_let_119 (ite (> (f0 (- v0) (/ _let_19 1)) _let_23) _let_6 _let_72))) (let ((_let_120 (ite (> _let_16 _let_20) (- _let_2) _let_84))) (let ((_let_121 (ite (>= _let_11 _let_10) (+ (/ 7 (- 6)) v0) (ite (>= (* 6.0 v0) _let_22) _let_20 _let_16)))) (let ((_let_122 (ite (= _let_10 _let_5) _let_0 _let_0))) (let ((_let_123 (ite (= _let_14 _let_12) _let_1 _let_102))) (let ((_let_124 (ite (= _let_13 _let_11) _let_75 _let_6))) (let ((_let_125 (ite (>= (- v0) _let_13) _let_92 _let_26))) (let ((_let_126 (ite (p0 _let_13 _let_1) (ite (>= (/ 6 (- 6)) _let_8) _let_12 _let_1) (ite (distinct _let_9 (/ _let_21 1)) (ite (<= (/ _let_18 1) (/ 6 (- 6))) (* (/ (- 6) 1) _let_10) (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65)) (ite (= _let_24 _let_8) _let_105 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22)))))) (let ((_let_127 (ite (>= (* (/ (- 6) 1) _let_10) _let_4) (ite (>= (/ 6 (- 6)) _let_8) _let_12 _let_1) _let_17))) (let ((_let_128 (ite (< _let_17 _let_20) _let_7 (ite (p0 _let_15 _let_6) _let_112 (ite (< (/ 6 (- 7)) (/ 6 (- 6))) (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_5))))) (let ((_let_129 (ite (< _let_21 _let_25) (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_74))) (let ((_let_130 (ite (<= _let_26 (- (/ 7 (- 6)) _let_0)) (ite (distinct (- _let_7) _let_4) _let_21 _let_97) (- _let_2)))) (let ((_let_131 (ite (<= _let_13 (- (/ 7 (- 6)))) _let_19 (ite (= _let_22 _let_7) (- _let_7) _let_14)))) (let ((_let_132 (ite (>= (* (/ (- 6) 1) _let_10) _let_4) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16) (- _let_7)))) (let ((_let_133 (ite (< (/ _let_18 1) _let_23) (ite _let_46 (ite (> (/ _let_2 1) _let_9) _let_25 _let_3) _let_66) _let_131))) (let ((_let_134 (ite (>= _let_3 _let_10) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite (>= _let_14 _let_0) (- _let_7) (* 6.0 v0))))) (let ((_let_135 (ite _let_41 _let_106 _let_3))) (let ((_let_136 (ite (= _let_14 (/ (- _let_2) 1)) _let_72 _let_100))) (let ((_let_137 (ite (= _let_1 (f1 _let_9 (/ (- _let_2) 1))) (ite (p0 (/ _let_25 1) _let_11) _let_110 _let_101) (/ 6 (- 7))))) (let ((_let_138 (ite (>= _let_1 _let_8) (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6))))))) (let ((_let_139 (ite (= _let_16 _let_16) (+ (* 6.0 v0) _let_11) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))))) (let ((_let_140 (ite (< _let_17 _let_20) (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (>= (/ 6 (- 6)) _let_8) _let_12 _let_1)))) (let ((_let_141 (ite _let_34 _let_134 _let_81))) (let ((_let_142 (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) (ite (distinct (- _let_7) _let_4) _let_21 _let_97) _let_125))) (let ((_let_143 (ite (<= _let_26 (/ _let_2 1)) (- _let_2) (ite (= (- v0) (/ 6 (- 6))) _let_72 _let_6)))) (let ((_let_144 (ite (< _let_13 (* 6.0 v0)) (ite _let_40 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76) _let_120) (- (- (/ 7 (- 6))))))) (let ((_let_145 (ite (distinct (f1 _let_9 (/ (- _let_2) 1)) (/ 6 (- 6))) _let_66 (ite (= _let_15 _let_12) _let_73 (ite _let_27 _let_20 _let_93))))) (let ((_let_146 (ite (= _let_16 (/ 6 (- 7))) _let_90 _let_120))) (let ((_let_147 (ite _let_32 _let_91 _let_131))) (let ((_let_148 (ite (>= _let_11 _let_10) (ite (p0 _let_15 _let_6) _let_112 (ite (< (/ 6 (- 7)) (/ 6 (- 6))) (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_5)) _let_101))) (let ((_let_149 (ite _let_56 (ite (= _let_22 _let_7) (- _let_7) _let_14) (ite (p0 v0 (* 6.0 v0)) _let_19 _let_1)))) (let ((_let_150 (ite _let_37 _let_3 _let_102))) (let ((_let_151 (ite (>= (* 6.0 v0) _let_22) _let_82 _let_6))) (let ((_let_152 (ite _let_39 _let_92 (ite (> (/ _let_19 1) _let_15) _let_80 (ite (p0 _let_26 _let_14) _let_9 (- _let_2)))))) (let ((_let_153 (ite (distinct (f0 (- v0) (/ _let_19 1)) _let_15) _let_112 (ite _let_40 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76) _let_120)))) (let ((_let_154 (ite (p0 _let_13 _let_1) _let_140 (ite (p0 (/ _let_25 1) _let_11) _let_110 _let_101)))) (let ((_let_155 (ite _let_40 _let_61 _let_16))) (let ((_let_156 (ite (<= _let_5 _let_8) _let_65 _let_103))) (let ((_let_157 (ite _let_28 _let_20 _let_76))) (let ((_let_158 (ite (p0 _let_17 _let_6) (ite (> (- (/ 7 (- 6))) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_100 _let_92) (ite _let_31 _let_77 (f0 (- v0) (/ _let_19 1)))))) (let ((_let_159 (ite _let_36 _let_127 (- _let_7)))) (let ((_let_160 (ite (distinct _let_26 _let_20) _let_122 (f1 _let_9 (/ (- _let_2) 1))))) (let ((_let_161 (ite (>= (/ _let_2 1) _let_4) _let_118 (ite _let_31 _let_77 (f0 (- v0) (/ _let_19 1)))))) (let ((_let_162 (ite _let_37 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_15))) (let ((_let_163 (ite (p0 _let_0 _let_13) _let_94 _let_91))) (let ((_let_164 (ite (< _let_3 (f1 _let_9 (/ (- _let_2) 1))) _let_5 _let_77))) (let ((_let_165 (ite (> (/ _let_2 1) (/ 7 (- 6))) (ite _let_34 _let_67 _let_14) (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57)))) (let ((_let_166 (ite (> _let_5 _let_24) (ite _let_43 _let_111 (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)))) (ite (>= (f0 (- v0) (/ _let_19 1)) (+ (/ 7 (- 6)) v0)) _let_4 _let_82)))) (let ((_let_167 (ite (p0 v0 (* 6.0 v0)) _let_65 (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0))))) (let ((_let_168 (ite (> (/ 7 (- 6)) (* 6.0 v0)) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) _let_163))) (let ((_let_169 (ite (<= v0 (/ _let_21 1)) _let_2 (ite (distinct (/ 6 (- 6)) (/ _let_18 1)) _let_58 _let_90)))) (let ((_let_170 (ite (<= (/ _let_25 1) _let_5) (ite (= _let_1 (f1 _let_9 (/ (- _let_2) 1))) _let_102 _let_60) _let_167))) (let ((_let_171 (ite (> _let_17 _let_15) _let_88 _let_76))) (let ((_let_172 (ite _let_54 _let_158 _let_59))) (let ((_let_173 (ite (<= _let_17 _let_1) _let_95 (ite (p0 _let_1 _let_5) _let_156 _let_115)))) (let ((_let_174 (ite _let_51 _let_57 _let_168))) (let ((_let_175 (ite (= _let_26 _let_4) _let_131 (ite _let_29 _let_62 (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)))))) (let ((_let_176 (ite _let_41 _let_65 (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)))) (let ((_let_177 (ite (>= _let_19 _let_21) _let_156 _let_81))) (let ((_let_178 (ite _let_35 _let_98 _let_14))) (let ((_let_179 (ite (distinct _let_22 (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_14 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6)))) (let ((_let_180 (ite (> _let_10 _let_14) (ite (p0 (/ _let_25 1) _let_8) _let_58 _let_16) (/ 6 (- 6))))) (let ((_let_181 (ite (p0 (/ _let_2 1) (/ (- _let_2) 1)) (ite _let_27 (* (/ (- 6) 1) _let_10) (ite (= (/ _let_18 1) _let_14) _let_75 (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1))))) (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65))))) (let ((_let_182 (<= (ite _let_42 _let_145 (/ 6 (- 6))) (ite _let_29 _let_17 v0)))) (let ((_let_183 (< _let_95 _let_88))) (let ((_let_184 (or (=> (and (or (= (or (= _let_94 (ite (= _let_15 _let_12) _let_73 (ite _let_27 _let_20 _let_93))) (> _let_15 _let_4)) (=> (= _let_112 (ite _let_48 (ite (= _let_22 _let_7) (- _let_7) _let_14) (ite _let_44 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_20))) (= (ite _let_54 _let_63 _let_25) (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0)))) (not (p0 _let_94 _let_93))) (and (or (ite (> _let_164 _let_125) (= (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_110) (= (= _let_75 (ite _let_40 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76) _let_120)) (>= (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65) _let_73))) (and (= (=> (or (ite (< _let_3 (f1 _let_9 (/ (- _let_2) 1))) (xor (distinct (/ 7 (- 6)) (ite (p0 _let_26 _let_14) _let_9 (- _let_2))) (= _let_95 (ite _let_53 (- v0) _let_62))) (= (ite (< _let_17 _let_5) _let_1 (+ (/ 7 (- 6)) v0)) (f0 (- v0) (/ _let_19 1)))) (= (distinct (ite (p0 _let_17 _let_6) _let_0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6)) (ite _let_42 (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)) _let_11)) _let_37)) (=> (>= (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6) _let_110) (=> (> (ite _let_55 (/ 6 (- 6)) _let_112) _let_96) (<= (- _let_7) _let_14)))) (xor (p0 (ite (> _let_3 _let_12) _let_24 _let_2) _let_124) (ite (xor (>= (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)) (ite _let_29 _let_17 v0)) _let_106) (p0 _let_181 _let_91)) (>= (ite (p0 _let_16 (- (/ 7 (- 6)))) (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) (ite (>= _let_11 _let_10) _let_80 _let_3)) (>= _let_3 _let_10)))) (=> (<= _let_157 _let_14) (distinct _let_26 (ite (< (/ 7 (- 6)) (* (/ (- 6) 1) _let_10)) _let_151 _let_89))))) (ite (= (ite _let_48 (ite (>= (/ _let_19 1) _let_8) _let_118 (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (p0 v0 (* 6.0 v0)) _let_19 _let_1)) _let_154) (or (distinct (ite (< (/ _let_2 1) _let_24) _let_10 _let_26) (* 6.0 v0)) (> _let_100 (ite (p0 _let_3 (+ (* 6.0 v0) _let_11)) _let_117 _let_98))) (= _let_140 _let_141)))) (and (<= (ite (distinct v0 (/ 6 (- 6))) _let_81 _let_91) _let_172) (or (xor (ite (xor (ite (>= _let_101 (ite (>= _let_20 _let_4) _let_123 _let_134)) (> _let_81 _let_150) (> _let_158 _let_26)) (and (and (>= (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16) (ite (<= (/ _let_25 1) _let_16) _let_24 _let_82)) (>= (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76) _let_58)) (distinct _let_105 (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0)))) (< (ite (p0 _let_26 _let_14) _let_9 (- _let_2)) (ite (>= (f0 (- v0) (/ _let_19 1)) (+ (/ 7 (- 6)) v0)) _let_4 _let_82)) (= _let_131 _let_83)) (ite (p0 (ite _let_38 _let_19 _let_80) _let_170) (<= _let_114 _let_119) (not (not (distinct (/ _let_19 1) _let_59))))) (or (=> (<= _let_145 (/ _let_21 1)) (< _let_0 _let_146)) (=> (<= _let_26 (- (/ 7 (- 6)) _let_0)) (ite (= (ite (> (f0 (- v0) (/ _let_19 1)) _let_23) _let_67 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6)) (/ (- _let_2) 1)) (or (ite (ite (> (- (/ 7 (- 6)) _let_0) _let_113) (= (ite (> (- (/ 7 (- 6))) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_100 _let_92) _let_100) (>= v0 (ite (<= (- _let_7) _let_14) _let_20 _let_13))) (ite (> (- (/ 7 (- 6)) _let_0) _let_113) (= (ite (> (- (/ 7 (- 6))) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_100 _let_92) _let_100) (>= v0 (ite (<= (- _let_7) _let_14) _let_20 _let_13))) (= _let_84 (ite _let_46 (ite (> (/ _let_2 1) _let_9) _let_25 _let_3) _let_66))) (> _let_158 _let_145)) (= _let_6 _let_129))))))) (xor (ite (not (=> (and (= _let_144 (ite (distinct _let_26 _let_20) (/ 6 (- 7)) _let_57)) (p0 (ite _let_51 _let_83 _let_63) _let_133)) (< (ite (p0 _let_26 _let_14) _let_9 (- _let_2)) _let_138))) (xor (not (> (ite _let_43 _let_102 _let_26) _let_14)) (ite (ite (< (ite (> (/ _let_2 1) _let_9) _let_25 _let_3) _let_111) (xor (> _let_100 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (- (- (/ 7 (- 6)))) _let_148)) (distinct (ite (<= (- _let_7) _let_14) (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (p0 _let_17 _let_6) _let_0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6))) (ite _let_29 _let_17 v0))) (= (ite _let_42 _let_145 (/ 6 (- 6))) (ite (<= (- _let_7) _let_14) (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (p0 _let_17 _let_6) _let_0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6))))) (= _let_59 (ite (p0 (/ _let_25 1) _let_11) _let_110 _let_101)) (p0 (ite (> (- v0) (- (/ 7 (- 6)) _let_0)) _let_89 _let_79) (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0))))) (and (or (>= _let_155 _let_96) (< (ite _let_34 (ite (distinct (/ 6 (- 6)) (/ _let_18 1)) _let_58 _let_90) _let_71) _let_130)) (or (or (and (=> (distinct _let_179 (ite _let_43 _let_111 (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))))) (<= _let_26 (/ _let_2 1))) (ite (p0 _let_122 _let_168) (< _let_85 _let_11) (< _let_75 _let_90))) (=> (xor (= _let_172 (ite (>= _let_1 _let_8) (+ (/ 7 (- 6)) v0) _let_19)) (not (<= _let_154 _let_100))) (ite (ite (<= (ite _let_30 _let_71 _let_151) _let_5) (p0 _let_65 (/ _let_19 1)) (p0 _let_172 _let_62)) (not (<= (f1 _let_9 (/ (- _let_2) 1)) (/ 6 (- 6)))) (distinct (ite (> (/ 7 (- 6)) _let_16) (- (/ 7 (- 6))) (ite _let_53 (- v0) _let_62)) _let_138)))) (or (not (= (= (or (p0 (ite (>= _let_1 _let_8) (+ (/ 7 (- 6)) v0) _let_19) (ite (> (/ _let_21 1) _let_4) _let_74 _let_1)) (>= (ite (> _let_3 _let_12) (* (/ (- 6) 1) _let_10) _let_75) (- (/ 7 (- 6))))) (not (<= (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16) (ite (= v0 _let_6) _let_21 _let_63)))) (xor (< _let_103 _let_113) (< _let_103 _let_113)))) (>= _let_62 _let_80))))) (not (= (ite (= (< _let_106 (ite (> _let_5 _let_4) _let_22 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6)))))) (p0 _let_15 (/ (- _let_2) 1))) (ite (=> (> _let_110 _let_152) (p0 _let_94 _let_113)) (= (f0 (- v0) (/ _let_19 1)) (ite (> (/ _let_2 1) _let_9) _let_25 _let_3)) (xor (=> (ite (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) (p0 _let_114 (ite (distinct (/ _let_21 1) (/ 6 (- 6))) (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14)) _let_130)) (>= _let_84 _let_79)) (> (/ (- _let_2) 1) _let_20) (p0 (ite (<= (- _let_7) _let_14) (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (p0 _let_17 _let_6) _let_0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6))) (/ _let_19 1))) (= _let_5 _let_119)) (not (>= (/ _let_2 1) _let_4)))) (=> (=> (and (distinct _let_164 _let_144) (< (ite (= (/ _let_18 1) _let_14) _let_75 (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1)))) (- (/ 7 (- 6))))) (=> (distinct _let_74 (/ _let_19 1)) (p0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6) _let_140))) (or (or (and (>= (/ _let_2 1) _let_14) (and (>= _let_11 (- v0)) (< _let_89 _let_170))) _let_55) (distinct _let_129 _let_158)))) (xor (ite (and (=> (<= (ite (> (/ _let_2 1) _let_9) _let_25 _let_3) (- (/ 7 (- 6)) _let_0)) (< _let_137 _let_110)) (ite (distinct _let_133 _let_12) (and (not (>= _let_24 _let_119)) (p0 _let_3 _let_58)) (= _let_82 (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)))) (xor (xor (xor (and (distinct _let_167 _let_73) (= _let_179 _let_14)) (p0 _let_119 _let_11)) (> _let_164 _let_155)) (not (<= _let_100 (ite (<= _let_0 (* 6.0 v0)) (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1))))))) (=> (and (> _let_17 _let_181) (< _let_17 _let_10)) (< _let_156 _let_117))) (ite (or (= (not (< _let_12 (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1))))) (not (p0 _let_95 _let_115))) (ite (<= (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_146 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6))))) _let_98) (not (distinct _let_125 (ite (>= (/ _let_18 1) _let_1) (- (/ 7 (- 6)) _let_0) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16)))) (distinct (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) v0)) (/ 7 (- 6)) _let_81) _let_92))) (ite (ite (ite (xor (>= (ite (= (- v0) (/ 6 (- 6))) _let_72 _let_6) _let_7) (<= (ite (p0 _let_1 _let_5) _let_156 _let_115) _let_157)) (> (/ _let_19 1) _let_163) _let_52) (= _let_175 (ite (> (/ 7 (- 6)) _let_16) (- (/ 7 (- 6))) (ite _let_53 (- v0) _let_62))) (= (p0 v0 (* 6.0 v0)) (and (> _let_122 _let_164) (>= (ite (< (+ (* 6.0 v0) _let_11) _let_5) _let_74 (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0))) _let_118)))) (ite _let_38 (< _let_141 _let_138) (<= _let_14 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57))) (xor (xor (or (> _let_105 (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76))) (> v0 (ite (= _let_22 _let_7) (- _let_7) _let_14))) (= (= (not (or (= _let_113 _let_112) (> _let_59 _let_148))) (= _let_133 _let_156)) (xor (not (< _let_137 _let_124)) (< _let_68 _let_110)))) (and (xor (< _let_115 _let_17) _let_49) (= (>= _let_175 _let_89) (and (ite (distinct _let_68 _let_181) (= (ite _let_44 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_20) _let_150) (<= _let_61 (ite (distinct _let_9 (/ _let_21 1)) (ite (<= (/ _let_18 1) (/ 6 (- 6))) (* (/ (- 6) 1) _let_10) (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65)) (ite (= _let_24 _let_8) _let_105 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22))))) (>= (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) _let_152 _let_112) _let_158)))))) (not (>= (ite (p0 _let_17 _let_6) _let_0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6)) _let_181)))))))))) (let ((_let_185 (and (= (=> (= (or (and (< (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) v0)) (/ 7 (- 6)) _let_81) (f0 (- v0) (/ _let_19 1))) (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6)))))) (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) (p0 _let_105 _let_136) (> _let_141 _let_115))) (>= _let_122 _let_113)) (<= (/ 6 (- 7)) (f0 (- v0) (/ _let_19 1)))) (and (p0 (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (ite _let_42 (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)) _let_11)) _let_32)) (and (xor (ite (or (xor (>= _let_108 _let_149) (distinct v0 (/ 6 (- 6)))) (xor (or (or (> _let_81 _let_174) (= (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16) _let_7)) (= (distinct v0 _let_123) (p0 _let_159 _let_136))) (>= _let_156 (- v0)))) (and (= _let_129 _let_74) (=> (=> (< (ite (> (/ _let_21 1) _let_4) _let_74 _let_1) (ite (distinct (/ _let_21 1) (/ 6 (- 6))) (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14)) _let_130)) (> (ite (<= _let_0 (* 6.0 v0)) (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1)))) (ite (<= (- _let_7) _let_14) _let_20 _let_13))) (=> (<= _let_70 _let_10) (< _let_65 (ite (<= (- _let_7) _let_14) (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (p0 _let_17 _let_6) _let_0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6))))))) (xor (not (=> (= (or (not (distinct (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0)) _let_129)) (xor (=> (> (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) _let_12 (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0)) (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57)) (<= _let_147 _let_106)) (> (/ _let_2 1) (/ 7 (- 6))))) (ite (= _let_20 (/ 6 (- 7))) (and (>= _let_14 _let_90) (> _let_176 _let_82)) (>= _let_127 _let_129))) (= (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16) _let_149))) (ite (>= (- v0) _let_13) (not (> (ite _let_42 _let_145 (/ 6 (- 6))) (ite (>= (/ 6 (- 6)) _let_8) _let_12 _let_1))) (> _let_166 _let_14)))) (ite (ite (> (* (/ (- 6) 1) _let_10) (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)) (ite _let_29 _let_17 v0))) (> (ite (<= (- _let_7) _let_14) _let_20 _let_13) (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6))))) (= (> (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)) _let_140) (>= _let_10 (ite (>= _let_11 _let_10) _let_80 _let_3)))) (or (or (or (distinct (/ _let_25 1) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) (distinct (ite (>= _let_14 _let_0) (- _let_7) (* 6.0 v0)) (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)))) (xor (xor (= (and (< (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) _let_124) (p0 _let_168 (/ _let_21 1))) (or (>= _let_147 _let_86) (= _let_26 _let_4))) (and (< _let_12 (ite _let_30 _let_71 _let_151)) (and (xor (= (ite _let_42 _let_145 (/ 6 (- 6))) _let_167) (p0 _let_128 (ite (= (/ _let_18 1) _let_14) _let_75 (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1)))))) (or (= (ite (>= _let_1 _let_8) (+ (/ 7 (- 6)) v0) _let_19) (/ _let_25 1)) (<= _let_147 (ite (p0 _let_16 (- (/ 7 (- 6)))) (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))))))) (not (<= _let_158 (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65))))) (or (ite (or (>= (/ _let_18 1) _let_1) (>= _let_111 _let_162)) (>= (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) (ite (>= _let_1 _let_8) (+ (/ 7 (- 6)) v0) _let_19)) (not (=> (< (ite (p0 (/ _let_25 1) _let_11) _let_110 _let_101) (ite (>= _let_14 _let_0) (- _let_7) (* 6.0 v0))) (< (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76) _let_146)))) (or (and (or (= (= _let_113 (ite (p0 _let_15 _let_6) _let_112 (ite (< (/ 6 (- 7)) (/ 6 (- 6))) (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_5))) (<= _let_169 (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1))))) (and (ite (<= (- v0) (- (- (/ 7 (- 6))))) (xor (distinct (ite (<= (- _let_7) _let_14) (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (p0 _let_17 _let_6) _let_0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6))) _let_138) (<= _let_82 _let_116)) (ite (= v0 _let_6) (and (= _let_22 _let_7) (< (ite (= v0 _let_6) _let_21 _let_63) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13))) (ite (or (xor (<= _let_163 _let_171) (distinct _let_89 (ite (distinct (/ _let_21 1) (/ 6 (- 6))) (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14)) _let_130))) (= _let_149 _let_114)) (< _let_21 _let_25) (or (p0 _let_9 (/ _let_25 1)) (<= _let_7 (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0)))))) (> _let_175 _let_116))) (xor (= (+ (* 6.0 v0) _let_11) _let_136) (or (>= (f0 (- v0) (/ _let_19 1)) (+ (/ 7 (- 6)) v0)) (distinct (/ _let_25 1) (+ (/ 7 (- 6)) v0))))) (not (and (> _let_153 _let_13) (=> (< _let_137 (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)) (ite _let_29 _let_17 v0))) (>= _let_14 _let_137))))))) (not (=> (<= _let_165 (ite (<= (/ _let_18 1) (/ 6 (- 6))) (* (/ (- 6) 1) _let_10) (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65))) (and (>= (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) v0)) (/ 7 (- 6)) _let_81) _let_135) (p0 (- v0) _let_151)))))) (xor (ite (or (xor (>= _let_108 _let_149) (distinct v0 (/ 6 (- 6)))) (xor (or (or (> _let_81 _let_174) (= (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16) _let_7)) (= (distinct v0 _let_123) (p0 _let_159 _let_136))) (>= _let_156 (- v0)))) (and (= _let_129 _let_74) (=> (=> (< (ite (> (/ _let_21 1) _let_4) _let_74 _let_1) (ite (distinct (/ _let_21 1) (/ 6 (- 6))) (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14)) _let_130)) (> (ite (<= _let_0 (* 6.0 v0)) (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1)))) (ite (<= (- _let_7) _let_14) _let_20 _let_13))) (=> (<= _let_70 _let_10) (< _let_65 (ite (<= (- _let_7) _let_14) (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (p0 _let_17 _let_6) _let_0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6))))))) (xor (not (=> (= (or (not (distinct (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0)) _let_129)) (xor (=> (> (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) _let_12 (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0)) (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57)) (<= _let_147 _let_106)) (> (/ _let_2 1) (/ 7 (- 6))))) (ite (= _let_20 (/ 6 (- 7))) (and (>= _let_14 _let_90) (> _let_176 _let_82)) (>= _let_127 _let_129))) (= (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16) _let_149))) (ite (>= (- v0) _let_13) (not (> (ite _let_42 _let_145 (/ 6 (- 6))) (ite (>= (/ 6 (- 6)) _let_8) _let_12 _let_1))) (> _let_166 _let_14)))) (ite (ite (> (* (/ (- 6) 1) _let_10) (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)) (ite _let_29 _let_17 v0))) (> (ite (<= (- _let_7) _let_14) _let_20 _let_13) (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6))))) (= (> (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)) _let_140) (>= _let_10 (ite (>= _let_11 _let_10) _let_80 _let_3)))) (or (or (or (distinct (/ _let_25 1) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) (distinct (ite (>= _let_14 _let_0) (- _let_7) (* 6.0 v0)) (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)))) (xor (xor (= (and (< (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) _let_124) (p0 _let_168 (/ _let_21 1))) (or (>= _let_147 _let_86) (= _let_26 _let_4))) (and (< _let_12 (ite _let_30 _let_71 _let_151)) (and (xor (= (ite _let_42 _let_145 (/ 6 (- 6))) _let_167) (p0 _let_128 (ite (= (/ _let_18 1) _let_14) _let_75 (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1)))))) (or (= (ite (>= _let_1 _let_8) (+ (/ 7 (- 6)) v0) _let_19) (/ _let_25 1)) (<= _let_147 (ite (p0 _let_16 (- (/ 7 (- 6)))) (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))))))) (not (<= _let_158 (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65))))) (or (ite (or (>= (/ _let_18 1) _let_1) (>= _let_111 _let_162)) (>= (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) (ite (>= _let_1 _let_8) (+ (/ 7 (- 6)) v0) _let_19)) (not (=> (< (ite (p0 (/ _let_25 1) _let_11) _let_110 _let_101) (ite (>= _let_14 _let_0) (- _let_7) (* 6.0 v0))) (< (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76) _let_146)))) (or (and (or (= (= _let_113 (ite (p0 _let_15 _let_6) _let_112 (ite (< (/ 6 (- 7)) (/ 6 (- 6))) (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_5))) (<= _let_169 (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1))))) (and (ite (<= (- v0) (- (- (/ 7 (- 6))))) (xor (distinct (ite (<= (- _let_7) _let_14) (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (p0 _let_17 _let_6) _let_0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6))) _let_138) (<= _let_82 _let_116)) (ite (= v0 _let_6) (and (= _let_22 _let_7) (< (ite (= v0 _let_6) _let_21 _let_63) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13))) (ite (or (xor (<= _let_163 _let_171) (distinct _let_89 (ite (distinct (/ _let_21 1) (/ 6 (- 6))) (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14)) _let_130))) (= _let_149 _let_114)) (< _let_21 _let_25) (or (p0 _let_9 (/ _let_25 1)) (<= _let_7 (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0)))))) (> _let_175 _let_116))) (xor (= (+ (* 6.0 v0) _let_11) _let_136) (or (>= (f0 (- v0) (/ _let_19 1)) (+ (/ 7 (- 6)) v0)) (distinct (/ _let_25 1) (+ (/ 7 (- 6)) v0))))) (not (and (> _let_153 _let_13) (=> (< _let_137 (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)) (ite _let_29 _let_17 v0))) (>= _let_14 _let_137))))))) (not (=> (<= _let_165 (ite (<= (/ _let_18 1) (/ 6 (- 6))) (* (/ (- 6) 1) _let_10) (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65))) (and (>= (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) v0)) (/ 7 (- 6)) _let_81) _let_135) (p0 (- v0) _let_151)))))))))) (let ((_let_186 (=> (not (and (or (and (or (not (distinct (- _let_7) _let_4)) (not (= _let_182 (<= _let_147 _let_146)))) (= (xor (> (ite (= _let_22 _let_7) (- _let_7) _let_14) (/ 7 (- 6))) (xor (> (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) (ite (distinct (- _let_7) _let_4) _let_21 _let_97)) (or (= _let_14 _let_159) (>= (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) v0)) (/ 7 (- 6)) _let_81))))) (<= (ite _let_43 _let_102 _let_26) (ite _let_34 (ite (distinct (/ 6 (- 6)) (/ _let_18 1)) _let_58 _let_90) _let_71)))) (not (or (ite (= _let_151 (ite (>= (f0 (- v0) (/ _let_19 1)) (+ (/ 7 (- 6)) v0)) _let_4 _let_82)) (= (<= (/ _let_25 1) _let_5) (>= (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0) (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22))) (= (not (> (/ 7 (- 6)) _let_16)) (<= _let_154 (ite (>= _let_14 _let_0) (- _let_7) (* 6.0 v0))))) (and (distinct _let_12 _let_15) (> v0 (ite (distinct _let_26 _let_20) (/ 6 (- 7)) _let_57)))))) (and (= (not (< v0 (/ _let_2 1))) (or (= (ite _let_46 (ite (> (/ _let_2 1) _let_9) _let_25 _let_3) _let_66) (ite (< (/ _let_2 1) _let_24) _let_10 _let_26)) (xor (p0 _let_85 _let_180) (p0 (ite (p0 _let_16 (- (/ 7 (- 6)))) (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) (- (/ 7 (- 6))))))) (= (not (xor (not (> _let_160 _let_123)) (>= _let_109 _let_123))) (= (not (not (=> (> (- _let_7) _let_66) (> (/ _let_2 1) _let_175)))) (ite (ite (xor (p0 _let_15 _let_6) (p0 _let_175 (ite _let_44 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_20))) _let_31 (= (or (< (/ _let_18 1) _let_23) (<= (* (/ (- 6) 1) _let_10) _let_117)) (> (ite (<= (- _let_7) _let_14) _let_20 _let_13) (f1 _let_9 (/ (- _let_2) 1))))) (> _let_155 (/ (- _let_2) 1)) (ite (>= (ite (distinct (/ 6 (- 6)) (/ _let_18 1)) _let_58 _let_90) _let_20) (and (xor (p0 (ite (>= (f0 (- v0) (/ _let_19 1)) (+ (/ 7 (- 6)) v0)) _let_4 _let_82) _let_169) (xor (> _let_137 _let_14) (distinct _let_116 (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))))) (p0 (- (- (/ 7 (- 6)))) _let_170)) (> (ite (p0 _let_17 _let_6) _let_0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6)) (+ (* 6.0 v0) _let_11))))))))) (and (or (or (ite (and (not (ite (<= (ite (= v0 _let_6) _let_21 _let_63) (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1)))) (> (ite (> _let_3 _let_12) (* (/ (- 6) 1) _let_10) _let_75) (ite (p0 (/ _let_25 1) _let_11) _let_110 _let_101)) (not (> _let_115 (ite (>= (/ 6 (- 6)) _let_8) _let_12 _let_1))))) (= (= (=> (>= _let_161 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6))))) (= (ite (and (>= _let_85 _let_105) (>= (ite (<= (/ _let_18 1) (/ 6 (- 6))) (* (/ (- 6) 1) _let_10) (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65)) (ite _let_34 (ite (distinct (/ 6 (- 6)) (/ _let_18 1)) _let_58 _let_90) _let_71))) (<= _let_118 (ite (>= (* 6.0 v0) _let_22) _let_20 _let_16)) (> _let_117 (ite _let_48 (ite (= _let_22 _let_7) (- _let_7) _let_14) (ite _let_44 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_20)))) (or (xor (> (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)) (ite (p0 _let_15 _let_6) _let_112 (ite (< (/ 6 (- 7)) (/ 6 (- 6))) (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_5))) (= (> (ite (<= _let_0 (* 6.0 v0)) (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1)))) _let_84) (not (p0 (+ (* 6.0 v0) _let_11) _let_68)))) (xor (ite (<= _let_127 (ite (distinct (/ _let_21 1) (/ 6 (- 6))) (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14)) _let_130)) _let_48 (= (ite (distinct (/ _let_21 1) (/ 6 (- 6))) (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14)) _let_130) _let_14)) (< _let_168 _let_156))))) (or (< (ite (>= _let_20 _let_4) _let_123 _let_134) _let_5) (distinct (ite _let_40 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76) _let_120) _let_148))) (=> (not (xor (distinct (+ (/ 7 (- 6)) v0) (ite (distinct v0 (/ 6 (- 6))) _let_81 _let_91)) (>= _let_177 _let_152))) (or (not (=> (p0 (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)) _let_81) (>= _let_14 _let_0))) (=> (>= _let_123 _let_17) (not (p0 (- (/ 7 (- 6)) _let_0) _let_171))))))) (=> (> (ite _let_54 _let_63 _let_25) _let_6) (or (or (xor (=> (=> (p0 _let_78 (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)))) (<= _let_127 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (- (- (/ 7 (- 6)))) _let_148))) (and (not (< _let_136 (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0))) (not (=> (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (< _let_77 (ite (distinct v0 (/ 6 (- 6))) _let_81 _let_91)))))) (<= (ite _let_43 _let_111 (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)))) _let_120)) (= (p0 _let_133 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57)) (or (< (ite (> (/ _let_2 1) _let_9) _let_25 _let_3) (ite (= _let_24 _let_8) _let_105 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22))) (distinct (ite (= _let_24 _let_8) _let_105 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22)) _let_155)))) (=> (< _let_69 _let_77) (p0 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (- (- (/ 7 (- 6)))) _let_148) _let_3)))) (xor (ite (=> (p0 (ite _let_43 _let_111 (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)))) _let_105) (<= _let_63 _let_68)) (and (ite (= (> (ite (>= (/ _let_18 1) _let_1) (- (/ 7 (- 6)) _let_0) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16)) _let_118) (< _let_125 (- (- (/ 7 (- 6)))))) (xor (ite (distinct (ite _let_40 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76) _let_120) _let_131) (< _let_17 _let_5) (>= _let_110 (ite (> (f0 (- v0) (/ _let_19 1)) _let_23) _let_67 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6)))) (<= _let_5 _let_8)) (> (+ (/ 7 (- 6)) v0) _let_17)) (xor (xor (ite (not (distinct _let_162 _let_171)) (>= (* 6.0 v0) _let_22) _let_182) (distinct _let_90 _let_74)) (and (p0 (ite (p0 _let_1 _let_5) _let_156 _let_115) (/ _let_2 1)) (= _let_135 (ite (= (- v0) (/ 6 (- 6))) _let_72 _let_6))))) (or (=> (=> (= (<= (ite _let_51 _let_83 _let_63) _let_95) (distinct (ite _let_51 _let_83 _let_63) (ite _let_54 _let_63 _let_25))) (p0 (ite _let_43 _let_102 _let_26) (ite (>= _let_14 _let_0) (- _let_7) (* 6.0 v0)))) (= (ite (>= (/ 6 (- 6)) _let_8) _let_12 _let_1) (ite _let_55 (/ 6 (- 6)) _let_112))) (or (=> (= _let_10 _let_5) (and (> _let_75 (ite _let_42 _let_145 (/ 6 (- 6)))) (or (>= _let_101 (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) _let_12 (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0))) (and (= (> _let_141 _let_176) (p0 _let_64 _let_80)) (< (ite (> _let_5 _let_4) _let_22 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6))))) _let_91))))) (not (not (>= _let_114 _let_132)))))) (not (=> (<= _let_176 _let_166) (>= _let_105 (+ (* 6.0 v0) _let_11)))))) (xor (ite (or (p0 (ite (distinct (/ 6 (- 6)) (/ _let_18 1)) _let_58 _let_90) (ite (>= _let_11 _let_10) _let_80 _let_3)) (xor (= _let_179 _let_95) (>= (ite (p0 (/ _let_25 1) _let_8) _let_58 _let_16) _let_177))) (= (ite _let_29 _let_17 v0) _let_145) (distinct (* 6.0 v0) _let_90)) (not (not (and (not (not _let_51)) (or (p0 _let_99 _let_24) (>= (- (/ 7 (- 6)) _let_0) _let_164))))))) (and (or (= (ite (= _let_22 _let_7) (- _let_7) _let_14) _let_70) (p0 _let_166 _let_130)) (xor (= (= (ite (> (/ _let_19 1) _let_15) _let_80 (ite (p0 _let_26 _let_14) _let_9 (- _let_2))) (ite (>= _let_1 _let_8) (+ (/ 7 (- 6)) v0) _let_19)) (= (p0 (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)) _let_126) (distinct _let_20 (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14))))) (not (p0 _let_127 (f1 _let_9 (/ (- _let_2) 1))))))) (or (and (=> (=> (p0 _let_3 (/ 7 (- 6))) (p0 _let_161 (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)))) (= (> (/ 7 (- 6)) (* 6.0 v0)) (> _let_131 _let_130))) (> _let_79 _let_17)) (or (not (xor (= (or (or (or (= _let_100 _let_91) (> _let_14 _let_73)) (<= (ite (distinct (/ _let_21 1) (/ 6 (- 6))) (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14)) _let_130) (ite (= _let_22 _let_7) (- _let_7) _let_14))) (>= v0 (ite _let_30 _let_71 _let_151))) (not (< _let_105 _let_4))) (ite (>= _let_164 _let_123) (not (= (not (= _let_14 _let_12)) (= _let_98 _let_100))) (= (= (ite _let_51 _let_83 _let_63) _let_61) (= (ite _let_54 _let_63 _let_25) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))))))) (> (ite (p0 _let_17 _let_6) _let_0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6)) (ite (= _let_22 _let_7) (- _let_7) _let_14)))))))) (or (=> (and (or (= (or (= (< _let_23 (* (/ (- 6) 1) _let_10)) (>= _let_156 _let_86)) (= (= (> _let_10 _let_14) (< _let_144 (/ _let_18 1))) (<= _let_167 (ite (> (/ _let_21 1) _let_4) _let_74 _let_1)))) (ite (and (=> (>= (ite _let_30 _let_71 _let_151) (ite (< (/ _let_2 1) _let_24) _let_10 _let_26)) (xor (<= _let_79 (/ 7 (- 6))) (= (xor (distinct (ite _let_31 _let_77 (f0 (- v0) (/ _let_19 1))) (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1)))) (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1)))) (=> (<= _let_71 _let_70) (< _let_9 (/ _let_21 1)))))) (and (= (<= _let_109 _let_74) (distinct _let_22 (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)))) (or (=> (and (distinct (ite _let_48 (ite (>= (/ _let_19 1) _let_8) _let_118 (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (p0 v0 (* 6.0 v0)) _let_19 _let_1)) _let_94) (p0 (ite _let_53 (- v0) _let_62) _let_14)) (and (>= (ite (distinct (- _let_7) _let_4) _let_21 _let_97) _let_104) (xor (= (ite (p0 (/ _let_25 1) _let_11) _let_110 _let_101) _let_131) (ite (<= _let_146 _let_158) (= _let_12 (- v0)) (and (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (= _let_85 (ite (> _let_3 _let_12) (* (/ (- 6) 1) _let_10) _let_75))))))) (ite (= (xor (< (ite (> _let_3 _let_12) (* (/ (- 6) 1) _let_10) _let_75) (ite _let_42 (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)) _let_11)) (p0 _let_62 _let_145)) (=> (ite (<= (* 6.0 v0) _let_104) (= _let_65 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22)) (< (ite _let_46 (ite (> (/ _let_2 1) _let_9) _let_25 _let_3) _let_66) _let_4)) (<= (ite _let_51 _let_83 _let_63) _let_0))) (> (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1))) (ite (= (- v0) (/ 6 (- 6))) _let_72 _let_6)) (>= _let_114 (ite (>= (f0 (- v0) (/ _let_19 1)) (+ (/ 7 (- 6)) v0)) _let_4 _let_82)))))) (=> (= _let_16 (/ 6 (- 7))) (= _let_178 (ite (p0 _let_26 _let_14) _let_9 (- _let_2)))) (not (not (= (= (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (- (- (/ 7 (- 6)))) _let_148) (f0 (- v0) (/ _let_19 1))) (>= (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) _let_177)))))) (xor (or (distinct (ite _let_31 _let_77 (f0 (- v0) (/ _let_19 1))) _let_128) (= _let_147 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) _let_152 _let_112))) (not (ite (<= _let_179 _let_118) (= (ite (= _let_4 (ite (p0 _let_3 (+ (* 6.0 v0) _let_11)) _let_117 _let_98)) (< (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6)))) _let_66) (= _let_137 _let_63)) (or (ite (p0 _let_26 _let_14) (xor (p0 _let_153 _let_75) (<= _let_10 _let_122)) (<= _let_0 (* 6.0 v0))) (ite (< (ite (p0 (/ _let_25 1) _let_8) _let_58 _let_16) (ite (> (/ _let_21 1) _let_4) _let_74 _let_1)) (p0 (ite (p0 _let_16 (- (/ 7 (- 6)))) (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_181) (= _let_97 _let_84)))) (< (/ _let_2 1) _let_24))))) (= (ite (not (< _let_70 (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13))) (= (= _let_131 (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1)))) (ite (>= _let_158 _let_96) (= (ite (< (/ 7 (- 6)) (* (/ (- 6) 1) _let_10)) _let_151 _let_89) (ite (= _let_1 (f1 _let_9 (/ (- _let_2) 1))) _let_102 _let_60)) (< (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6) (ite _let_54 _let_63 _let_25)))) (and (xor (distinct _let_146 (ite _let_29 _let_17 v0)) (>= _let_15 (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16))) (xor (and (>= _let_131 (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (not (p0 _let_97 (ite (p0 (/ _let_25 1) _let_8) _let_58 _let_16)))) (and (or (= (= (ite _let_55 (/ 6 (- 6)) _let_112) (ite (>= _let_20 _let_4) _let_123 _let_134)) (ite (= _let_169 _let_96) (= _let_152 (ite _let_55 (/ 6 (- 6)) _let_112)) _let_34)) (not (ite (>= (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) _let_94) (p0 _let_160 _let_73) (p0 _let_124 (ite (= _let_15 _let_12) _let_73 (ite _let_27 _let_20 _let_93)))))) (=> (= _let_127 _let_156) (<= (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (- (- (/ 7 (- 6)))) _let_148) (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22))))))) (ite (ite (ite (or (distinct _let_26 (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) (< (/ 7 (- 6)) (* (/ (- 6) 1) _let_10))) (and (= _let_98 (ite (= _let_15 _let_12) _let_73 (ite _let_27 _let_20 _let_93))) (= _let_96 _let_158)) (= (ite (distinct _let_114 _let_16) (ite (= (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) _let_152 _let_112) (ite (< (+ (* 6.0 v0) _let_11) _let_5) _let_74 (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0)))) (= _let_16 _let_16) (not (> (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) _let_163))) (xor (> _let_4 _let_62) (= (distinct _let_14 (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0)) (> _let_155 (ite (<= (/ _let_18 1) (/ 6 (- 6))) (* (/ (- 6) 1) _let_10) (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65)))))) (xor (>= (+ (/ 7 (- 6)) v0) _let_118) (>= _let_117 (ite _let_27 _let_20 _let_93))))) (or (p0 (- (- (/ 7 (- 6)))) (ite _let_31 _let_77 (f0 (- v0) (/ _let_19 1)))) (and (= (<= _let_83 (- (- (/ 7 (- 6))))) (>= _let_5 (ite (distinct v0 (/ 6 (- 6))) _let_81 _let_91))) (> _let_5 _let_24))) (distinct _let_69 _let_105)) (xor (p0 _let_0 _let_13) (and (> _let_140 _let_166) (not (> (ite (= _let_15 _let_12) _let_73 (ite _let_27 _let_20 _let_93)) _let_142)))) (= (not (not (ite (ite (>= _let_17 _let_10) (= _let_73 (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65)) (distinct _let_104 (/ 7 (- 6)))) (xor (<= (ite (< _let_17 _let_5) _let_1 (+ (/ 7 (- 6)) v0)) (/ _let_19 1)) (xor _let_40 (=> (<= (/ _let_18 1) _let_82) (= (p0 _let_91 (* (/ (- 6) 1) _let_10)) (< _let_104 (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1)))))))) (= (>= _let_74 (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16)) (>= _let_93 _let_126))))) (= (= _let_68 (ite _let_42 _let_145 (/ 6 (- 6)))) (>= _let_73 (ite _let_29 _let_17 v0))))))) (or _let_186 _let_186)) (not (and (=> (or (=> (not (= (>= _let_156 (ite _let_44 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_20)) (> _let_96 (ite (>= (f0 (- v0) (/ _let_19 1)) (+ (/ 7 (- 6)) v0)) _let_4 _let_82)))) (ite (<= _let_63 _let_119) (or (= (ite (xor (=> (= (<= (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) _let_3) (p0 _let_16 (- (/ 7 (- 6))))) (xor (>= (/ 6 (- 6)) (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)) (ite _let_29 _let_17 v0))) (<= _let_59 (/ _let_18 1)))) (<= _let_20 _let_1)) (= (ite (p0 v0 (* 6.0 v0)) _let_19 _let_1) (- _let_7)) (>= (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)) (ite _let_29 _let_17 v0)) (ite _let_40 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76) _let_120))) (xor (or (<= (ite (>= (f0 (- v0) (/ _let_19 1)) (+ (/ 7 (- 6)) v0)) _let_4 _let_82) _let_100) (=> (and (= (p0 _let_168 _let_86) (< _let_132 _let_71)) (<= (ite _let_43 _let_102 _let_26) _let_24)) (ite (< _let_85 _let_105) (< _let_76 (ite (<= _let_0 (* 6.0 v0)) (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1))))) (< _let_163 (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)))))) (= (>= _let_154 (ite (> (f0 (- v0) (/ _let_19 1)) _let_23) _let_67 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6))) (not (distinct (ite _let_30 _let_71 _let_151) (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22)))))) (and (=> (=> (= (>= _let_112 _let_100) (<= (ite (distinct (- _let_7) _let_4) _let_21 _let_97) (ite (< (/ 7 (- 6)) (* (/ (- 6) 1) _let_10)) _let_151 _let_89))) (= (p0 (* (/ (- 6) 1) _let_10) _let_148) (= _let_4 _let_95))) (< (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)) _let_131)) (not (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10))))) (= (ite (>= _let_24 _let_8) (distinct _let_74 (ite _let_44 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_20)) (or (> (ite (> _let_3 _let_12) _let_24 _let_2) _let_116) (>= _let_100 (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16)))) (ite (= (>= (ite _let_46 (ite (> (/ _let_2 1) _let_9) _let_25 _let_3) _let_66) _let_180) (<= (ite _let_48 (ite (>= (/ _let_19 1) _let_8) _let_118 (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (p0 v0 (* 6.0 v0)) _let_19 _let_1)) _let_3)) (distinct (+ (* 6.0 v0) _let_11) (ite (> (/ _let_21 1) _let_4) _let_74 _let_1)) (xor (distinct (f1 _let_9 (/ (- _let_2) 1)) (ite (<= (- _let_7) _let_14) (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (p0 _let_17 _let_6) _let_0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6)))) (<= _let_139 (ite (>= (/ _let_19 1) _let_8) _let_118 (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))))))))) (not (=> (and (xor (not (xor (=> (xor (= (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0) _let_106) (p0 (ite (p0 v0 (* 6.0 v0)) _let_19 _let_1) (ite (> _let_3 _let_12) (* (/ (- 6) 1) _let_10) _let_75))) (= (p0 (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) (ite (>= (/ _let_19 1) _let_8) _let_118 (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)))) (>= _let_126 _let_173))) (and (= (<= _let_92 (ite (> (f0 (- v0) (/ _let_19 1)) _let_23) _let_67 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6))) (p0 _let_58 (ite (distinct (/ _let_21 1) (/ 6 (- 6))) (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14)) _let_130))) (= (<= _let_87 _let_68) (= (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_1))))) (>= (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65) (ite (= _let_24 _let_8) _let_105 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22)))) (not (p0 (/ _let_25 1) _let_8))) (=> (<= (ite (p0 (/ _let_25 1) _let_8) _let_58 _let_16) _let_155) (ite (or (= (xor (p0 (ite _let_42 (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)) _let_11) (ite (= v0 _let_6) _let_21 _let_63)) (> _let_17 _let_15)) (= (distinct _let_15 _let_120) (> (- v0) (- (/ 7 (- 6)) _let_0)))) (ite (xor (and (> _let_165 (ite (= v0 _let_6) _let_21 _let_63)) (= _let_83 _let_14)) (> (/ _let_19 1) _let_15)) (= (p0 (ite (p0 v0 (* 6.0 v0)) _let_19 _let_1) _let_59) (p0 (ite (< _let_17 _let_5) _let_1 (+ (/ 7 (- 6)) v0)) _let_157)) (and (ite (<= _let_172 _let_120) (=> (> (/ 6 (- 6)) _let_148) (distinct (f0 (- v0) (/ _let_19 1)) _let_15)) (= (<= (f0 (- v0) (/ _let_19 1)) _let_1) (<= (ite (>= _let_20 _let_4) _let_123 _let_134) (ite _let_43 _let_102 _let_26)))) (not (>= (* (/ (- 6) 1) _let_10) _let_4))))) (and (distinct _let_1 (/ _let_18 1)) (not (distinct _let_160 (ite _let_45 _let_8 _let_6)))) (ite (ite (ite (distinct _let_99 _let_78) (< _let_178 _let_174) (p0 _let_126 _let_141)) (> _let_171 _let_180) (< (ite (>= (* 6.0 v0) _let_22) _let_20 _let_16) _let_16)) (<= _let_174 _let_94) (ite (distinct (ite _let_27 _let_20 _let_93) _let_180) (p0 _let_154 (/ 6 (- 6))) (= _let_103 _let_79)))))))) (and (or (or (or (and (and (not (ite (>= (ite _let_48 (ite (= _let_22 _let_7) (- _let_7) _let_14) (ite _let_44 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_20)) (ite (p0 _let_16 (- (/ 7 (- 6)))) (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) (=> (or (distinct _let_155 _let_164) (= (< _let_13 (+ (/ 7 (- 6)) v0)) (p0 _let_3 (+ (* 6.0 v0) _let_11)))) (< (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1))) _let_69)) (p0 _let_60 _let_135))) (xor (= (>= _let_158 _let_120) (= _let_126 _let_156)) (or (> _let_61 _let_12) (xor (not (= (< (- (/ 7 (- 6)) _let_0) _let_22) (<= (ite (distinct (/ _let_21 1) (/ 6 (- 6))) (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14)) _let_130) (- (/ 7 (- 6)) _let_0)))) (= (ite (>= (/ _let_18 1) _let_1) (- (/ 7 (- 6)) _let_0) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16)) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7))))))) (= (>= _let_164 _let_154) (xor (p0 _let_104 (ite _let_27 _let_20 _let_93)) (= (ite (p0 (/ _let_25 1) _let_11) _let_110 _let_101) _let_10)))) (= _let_0 _let_164)) (not (and (distinct _let_155 _let_122) (xor (or (ite (>= (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) (ite (p0 _let_17 _let_6) _let_0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6))) (=> (= _let_126 (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16)) (<= (/ _let_18 1) (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)))) (xor (distinct (f1 _let_9 (/ (- _let_2) 1)) _let_23) _let_42)) (ite (>= (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65) _let_120) (> (ite (>= _let_14 _let_0) (- _let_7) (* 6.0 v0)) (ite (= _let_24 _let_8) _let_105 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22))) (> (ite (>= _let_1 _let_8) (+ (/ 7 (- 6)) v0) _let_19) (- (/ 7 (- 6)))))) (=> (distinct (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1))) (+ (/ 7 (- 6)) v0)) (not (p0 (ite (p0 _let_3 (+ (* 6.0 v0) _let_11)) _let_117 _let_98) _let_127))))))) (ite (ite (=> (> _let_137 _let_63) (ite (p0 _let_83 _let_13) (p0 (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0)) _let_114) (> (ite (p0 _let_16 (- (/ 7 (- 6)))) (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_166))) (or (<= (ite (<= (/ _let_25 1) _let_16) _let_24 _let_82) (ite (<= (- _let_7) _let_14) _let_20 _let_13)) (= _let_103 _let_153)) (and (xor (> _let_172 (+ (* 6.0 v0) _let_11)) (> _let_174 _let_118)) (=> (= _let_115 (ite (>= (/ 6 (- 6)) _let_8) _let_12 _let_1)) (<= (+ (* 6.0 v0) _let_11) _let_119)))) (and (<= _let_116 _let_115) (and (<= (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0)) _let_16) (distinct _let_4 _let_15))) (xor (xor (> (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) _let_74) (=> (distinct _let_81 _let_173) (> _let_135 _let_145))) (xor (distinct _let_57 (* 6.0 v0)) (= (+ (* 6.0 v0) _let_11) _let_143))))) (and (= (= (or (= _let_111 (ite _let_27 _let_20 _let_93)) (and (not (> (/ 6 (- 6)) _let_114)) (= (ite (<= (- _let_7) _let_14) (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (p0 _let_17 _let_6) _let_0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6))) _let_58))) (or (=> (< (ite _let_29 _let_17 v0) (ite (>= _let_11 _let_10) _let_80 _let_3)) (distinct _let_152 _let_122)) (and (= (xor (or (< _let_134 (ite (>= (/ _let_18 1) _let_1) (- (/ 7 (- 6)) _let_0) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16))) (distinct _let_125 _let_131)) (< (ite (<= (/ _let_25 1) _let_16) _let_24 _let_82) (ite _let_48 (ite (>= (/ _let_19 1) _let_8) _let_118 (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (p0 v0 (* 6.0 v0)) _let_19 _let_1)))) (or (p0 (/ _let_2 1) (/ 7 (- 6))) (xor (> _let_134 _let_76) (ite (= (- v0) (ite (distinct (/ _let_21 1) (/ 6 (- 6))) (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14)) _let_130)) (< _let_157 (ite (> (/ _let_19 1) _let_15) _let_80 (ite (p0 _let_26 _let_14) _let_9 (- _let_2)))) (< _let_181 (ite (distinct v0 (/ 6 (- 6))) _let_81 _let_91)))))) (=> (<= _let_176 (ite (distinct v0 (/ 6 (- 6))) _let_81 _let_91)) (= (ite (<= (/ _let_25 1) _let_16) _let_24 _let_82) _let_118))))) (ite (xor (or (and (=> (xor (>= _let_138 (ite _let_43 _let_102 _let_26)) (<= _let_6 (/ 6 (- 6)))) (and (> _let_120 _let_87) (=> (>= _let_180 _let_59) (ite (p0 _let_95 _let_131) (= (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)) (ite (> (f0 (- v0) (/ _let_19 1)) _let_23) _let_67 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6))) (distinct _let_119 (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)))))) (and (p0 _let_105 (ite _let_31 _let_77 (f0 (- v0) (/ _let_19 1)))) (= (> _let_79 _let_63) (> (ite _let_44 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_20) (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76))))) (= (ite (<= (/ _let_25 1) _let_16) _let_24 _let_82) _let_4)) (<= (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) _let_12 (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0)) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16))) (=> (> (ite _let_27 _let_20 _let_93) _let_88) (xor (distinct (ite (= _let_22 _let_7) (- _let_7) _let_14) _let_100) (= _let_59 _let_113))) (xor (>= (ite (distinct (/ _let_21 1) (/ 6 (- 6))) (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14)) _let_130) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (distinct (ite _let_29 _let_17 v0) (ite (>= _let_11 _let_10) _let_80 _let_3))))) (=> (=> (= (= (=> (=> (< v0 _let_26) (< _let_78 _let_58)) (ite (p0 _let_140 (ite (= _let_1 (f1 _let_9 (/ (- _let_2) 1))) _let_102 _let_60)) (< (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16) _let_161) (<= (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) _let_4))) (< (ite _let_54 _let_63 _let_25) _let_63)) (p0 v0 (* 6.0 v0))) (and (xor (<= _let_17 _let_86) (<= _let_6 _let_80)) (or (= (= (ite _let_48 (ite (= _let_22 _let_7) (- _let_7) _let_14) (ite _let_44 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_20)) _let_108) (= (- v0) (/ 6 (- 6)))) (distinct (ite (>= (f0 (- v0) (/ _let_19 1)) (+ (/ 7 (- 6)) v0)) _let_4 _let_82) (ite _let_54 _let_63 _let_25))))) (xor (xor (or (ite _let_46 (> _let_4 _let_139) (p0 _let_9 (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65))) (distinct _let_4 _let_82)) (and (=> (= _let_180 _let_158) (=> (>= (- (/ 7 (- 6))) (ite _let_55 (/ 6 (- 6)) _let_112)) (<= (ite (< (+ (* 6.0 v0) _let_11) _let_5) _let_74 (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0))) (ite (>= _let_11 _let_10) _let_80 _let_3)))) (>= (/ _let_25 1) _let_149))) (distinct (ite (> _let_3 _let_12) _let_24 _let_2) (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0)))))))) (=> (= (ite (not (and (<= (ite (distinct _let_26 _let_20) (/ 6 (- 7)) _let_57) _let_86) (> _let_62 (ite (p0 (/ _let_25 1) _let_11) _let_110 _let_101)))) (ite (=> (= (xor (distinct _let_94 _let_59) (>= _let_154 _let_20)) (=> (>= _let_58 _let_121) (>= (ite _let_30 _let_71 _let_151) _let_152))) (= (xor (>= _let_173 _let_71) (=> (= (p0 _let_17 _let_6) (or (not (distinct (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0) _let_102)) (distinct (ite (> (/ _let_19 1) _let_15) _let_80 (ite (p0 _let_26 _let_14) _let_9 (- _let_2))) (ite (>= (* 6.0 v0) _let_22) _let_20 _let_16)))) (p0 (ite (> (/ _let_2 1) _let_9) _let_25 _let_3) (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57)))) (and (>= _let_19 _let_21) (>= (ite (> _let_5 _let_4) _let_22 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6))))) _let_137)))) (ite (ite (>= _let_146 (ite (<= (- _let_7) _let_14) _let_20 _let_13)) (ite (< _let_65 _let_157) (>= _let_20 _let_4) (ite (< _let_146 _let_156) (= _let_176 _let_114) (< _let_144 _let_64))) (<= _let_165 (- v0))) (ite (p0 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76) (f0 (- v0) (/ _let_19 1))) (<= (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0) (ite _let_34 (ite (distinct (/ 6 (- 6)) (/ _let_18 1)) _let_58 _let_90) _let_71)) (and (distinct _let_64 _let_93) (> _let_136 (ite (= _let_24 _let_8) _let_105 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22))))) (< _let_138 (ite (>= (/ 6 (- 6)) _let_8) _let_12 _let_1))) (and (>= (ite _let_43 _let_102 _let_26) (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_146 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6)))))) (>= _let_9 (/ _let_25 1)))) (not (ite (= (> (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) _let_92) (>= (/ 6 (- 6)) _let_8)) (> v0 _let_175) (distinct (ite (= (/ _let_18 1) _let_14) _let_75 (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1)))) (ite _let_40 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76) _let_120))))) (xor (xor (ite (and (=> (or (= (or (not (or (ite (=> (xor (<= _let_12 _let_11) (= (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65) (ite _let_43 _let_111 (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)))))) (p0 (/ _let_25 1) _let_11)) (or (ite (= (xor (> _let_176 _let_177) (< _let_140 _let_139)) (p0 (ite _let_45 _let_8 _let_6) (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57))) (xor (> _let_140 _let_142) (>= (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0) (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65))) (<= _let_168 _let_166)) (= _let_102 _let_9)) (> _let_61 _let_107)) (= (and (= (ite _let_45 _let_8 _let_6) (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65))) (distinct (ite (p0 _let_17 _let_6) _let_0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6)) _let_16)) (not (or (= _let_62 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0)) (not (p0 _let_99 (ite (> (/ 7 (- 6)) _let_16) (- (/ 7 (- 6))) (ite _let_53 (- v0) _let_62))))))))) (or (not (< _let_94 _let_22)) (< (ite _let_43 _let_102 _let_26) (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1)))))) (xor (and (p0 _let_162 (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14))) (distinct (ite (p0 (/ _let_25 1) _let_11) _let_110 _let_101) _let_162)) _let_43)) (not (xor (=> (or (ite (not (xor (distinct _let_66 (ite (>= _let_14 _let_0) (- _let_7) (* 6.0 v0))) (distinct _let_58 (ite (> _let_3 _let_12) _let_24 _let_2)))) (= (not _let_33) (p0 (- v0) _let_15)) (<= (ite (= _let_1 (f1 _let_9 (/ (- _let_2) 1))) _let_102 _let_60) (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0)))) (=> (> _let_152 (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) v0)) (/ 7 (- 6)) _let_81)) (p0 (ite (>= (/ _let_19 1) _let_8) _let_118 (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) _let_155))) (and (and (<= _let_73 _let_85) (>= (ite (p0 (/ _let_25 1) _let_11) _let_110 _let_101) (ite (> (/ _let_2 1) _let_9) _let_25 _let_3))) (= _let_118 (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0))))) (and (ite (=> (or (ite (not (= _let_82 _let_114)) (p0 (ite (<= (- _let_7) _let_14) (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (p0 _let_17 _let_6) _let_0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6))) _let_174) (>= (/ (- _let_2) 1) _let_85)) (p0 (ite (> (/ 7 (- 6)) _let_16) (- (/ 7 (- 6))) (ite _let_53 (- v0) _let_62)) (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)))) (and (p0 _let_133 _let_127) (> _let_134 _let_63))) (not (= (and (p0 _let_162 _let_148) (p0 (ite _let_37 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0))) _let_80)) (< _let_81 (ite _let_48 (ite (= _let_22 _let_7) (- _let_7) _let_14) (ite _let_44 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_20))))) (xor (or (< _let_166 _let_86) (< _let_152 (/ _let_25 1))) (ite (> _let_130 _let_85) (and (=> (<= _let_159 (ite (> (/ _let_19 1) _let_15) _let_80 (ite (p0 _let_26 _let_14) _let_9 (- _let_2)))) (<= _let_3 _let_168)) (or (p0 _let_1 _let_5) (= (ite (p0 (/ _let_25 1) _let_8) _let_58 _let_16) (ite (>= (/ _let_19 1) _let_8) _let_118 (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)))))) (or (not (= (/ 6 (- 6)) (ite (> (- (/ 7 (- 6))) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_100 _let_92))) (< _let_165 _let_81))))) (or (and (> _let_123 _let_147) (>= (ite (p0 _let_16 (- (/ 7 (- 6)))) (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_88)) (= (distinct (ite (= (- v0) (/ 6 (- 6))) _let_72 _let_6) _let_99) (not (= (ite (> (- v0) (- (/ 7 (- 6)) _let_0)) _let_89 _let_79) _let_147)))))))) (or (=> (< _let_171 _let_163) (p0 _let_78 _let_14)) (= (xor (>= (ite _let_53 (- v0) _let_62) (ite (p0 _let_26 _let_14) _let_9 (- _let_2))) (< (ite _let_48 (ite (= _let_22 _let_7) (- _let_7) _let_14) (ite _let_44 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_20)) _let_117)) (= (= (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)) (ite (= (<= _let_156 _let_145) (distinct (ite (distinct _let_26 _let_20) (/ 6 (- 7)) _let_57) (ite _let_34 _let_67 _let_14))) (=> (= _let_121 (- (/ 7 (- 6)))) (p0 (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (> (/ _let_21 1) _let_4) _let_74 _let_1))) (or (not (< (f0 (- v0) (/ _let_19 1)) (- _let_7))) (<= (ite (= v0 _let_6) _let_21 _let_63) (ite _let_29 _let_62 (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)))))))))) (ite (xor (and (xor (or (>= _let_58 _let_159) (<= _let_165 (ite (distinct (/ _let_21 1) (/ 6 (- 6))) (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14)) _let_130))) (p0 _let_13 _let_1)) (or (or (<= (ite (p0 (/ _let_25 1) _let_8) _let_58 _let_16) _let_154) (p0 _let_3 _let_140)) (not (< (ite _let_29 _let_62 (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76))) (ite (p0 (/ _let_25 1) _let_11) _let_110 _let_101))))) (ite (=> (not (<= _let_144 _let_174)) (distinct (ite (>= (/ 6 (- 6)) _let_8) _let_12 _let_1) _let_178)) (or (ite (p0 _let_103 (ite _let_38 _let_19 _let_80)) (= _let_13 (/ 6 (- 6))) (>= (ite _let_46 (ite (> (/ _let_2 1) _let_9) _let_25 _let_3) _let_66) _let_115)) (ite (ite (xor (= (ite (not (< _let_113 (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) v0)) (/ 7 (- 6)) _let_81))) (>= _let_58 (ite _let_30 _let_71 _let_151)) (xor (= (< v0 _let_105) (= (ite (> (- v0) (- (/ 7 (- 6)) _let_0)) _let_89 _let_79) (* (/ (- 6) 1) _let_10))) (= (ite _let_44 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_20) _let_64))) (and (>= _let_7 _let_81) (distinct _let_105 _let_167))) (distinct (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0) (ite (> (/ _let_19 1) _let_15) _let_80 (ite (p0 _let_26 _let_14) _let_9 (- _let_2))))) (= (or (distinct _let_67 _let_118) (> _let_92 _let_134)) (not (xor (>= (ite _let_53 (- v0) _let_62) _let_104) _let_54))) (= (ite (p0 _let_1 _let_5) _let_156 _let_115) _let_176)) (ite (xor (and (and (p0 _let_95 (ite (= _let_22 _let_7) (- _let_7) _let_14)) (< (ite (< (+ (* 6.0 v0) _let_11) _let_5) _let_74 (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0))) (ite (>= (* 6.0 v0) _let_22) _let_20 _let_16))) (p0 (ite (>= _let_20 _let_4) _let_123 _let_134) (ite _let_34 (ite (distinct (/ 6 (- 6)) (/ _let_18 1)) _let_58 _let_90) _let_71))) (=> (p0 _let_95 (ite (> (/ _let_2 1) _let_9) _let_25 _let_3)) (= (ite (= _let_24 _let_8) _let_105 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22)) _let_4))) (<= (ite (p0 (/ _let_25 1) _let_8) _let_58 _let_16) _let_77) (xor (= _let_7 _let_177) (and (>= (/ _let_19 1) _let_8) (and (< (ite (> _let_5 _let_4) _let_22 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6))))) _let_103) (not (= _let_106 (ite (p0 (/ _let_25 1) _let_8) _let_58 _let_16))))))) (and (< _let_9 (ite _let_27 (* (/ (- 6) 1) _let_10) (ite (= (/ _let_18 1) _let_14) _let_75 (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1)))))) (=> (< _let_160 _let_77) (<= v0 (/ _let_21 1)))))) (< _let_16 (ite _let_48 (ite (>= (/ _let_19 1) _let_8) _let_118 (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (p0 v0 (* 6.0 v0)) _let_19 _let_1))))) (= (ite (> _let_105 (* (/ (- 6) 1) _let_10)) (ite (> _let_122 (ite (distinct v0 (/ 6 (- 6))) _let_81 _let_91)) (<= _let_91 _let_24) (distinct (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) v0)) (/ 7 (- 6)) _let_81) _let_75)) (> _let_109 (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13))) (= (ite (= (>= _let_13 _let_6) (p0 (ite _let_43 _let_111 (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)))) (ite _let_51 _let_83 _let_63))) (= (< (/ 6 (- 7)) (/ 6 (- 6))) (< (/ _let_25 1) _let_20)) (not (= (=> (ite (distinct (ite (< (/ 6 (- 7)) (/ 6 (- 6))) (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_5) _let_101) (xor (p0 _let_90 _let_141) (>= (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (= _let_1 (f1 _let_9 (/ (- _let_2) 1))) _let_102 _let_60))) (> _let_108 _let_68)) (< (ite (distinct _let_26 _let_20) (/ 6 (- 7)) _let_57) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)))) (> (ite (distinct (- _let_7) _let_4) _let_21 _let_97) (+ (* 6.0 v0) _let_11))))) (=> (=> (>= _let_17 _let_22) (= _let_140 (ite (> (/ _let_21 1) _let_4) _let_74 _let_1))) (>= (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) (- _let_7))))) (and (or (<= _let_17 _let_1) (p0 _let_138 (ite (= (/ _let_18 1) _let_14) _let_75 (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1)))))) (and (=> (or (=> (= (p0 (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14)) _let_15) (= _let_96 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0))) (> (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (- (- (/ 7 (- 6)))) _let_148) (+ (* 6.0 v0) _let_11))) (distinct _let_114 _let_91)) (ite (> (ite (p0 v0 (* 6.0 v0)) _let_19 _let_1) _let_107) (= (<= (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) _let_152 _let_112) _let_92) (distinct (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) (/ 6 (- 6)))) (= (ite _let_37 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0))) _let_160))) (not (xor (= (or (< _let_155 _let_173) (and (distinct _let_169 _let_70) (<= (ite (< (/ 7 (- 6)) (* (/ (- 6) 1) _let_10)) _let_151 _let_89) (ite _let_45 _let_8 _let_6)))) (not (> (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_108))) (>= _let_74 _let_130))))))) (=> _let_185 _let_185) (and (not (= (not (distinct (ite (< (/ _let_2 1) _let_24) _let_10 _let_26) _let_147)) (or (> _let_75 _let_17) (<= _let_179 (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)))))) (=> (<= _let_168 _let_109) (xor (distinct (ite (= _let_1 (f1 _let_9 (/ (- _let_2) 1))) _let_102 _let_60) _let_91) (xor (= _let_8 (ite (= (- v0) (/ 6 (- 6))) _let_72 _let_6)) (not (> (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1))) (ite _let_51 _let_83 _let_63)))))))) (=> (not (= (= (xor (= _let_71 _let_176) (= (xor (and (distinct _let_169 _let_8) (<= (ite _let_43 _let_102 _let_26) _let_117)) (< _let_14 (ite (<= (- _let_7) _let_14) _let_20 _let_13))) (and (p0 _let_111 _let_76) (distinct (ite (>= (f0 (- v0) (/ _let_19 1)) (+ (/ 7 (- 6)) v0)) _let_4 _let_82) (ite (p0 _let_15 _let_6) _let_112 (ite (< (/ 6 (- 7)) (/ 6 (- 6))) (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_5)))))) (=> (= _let_129 _let_72) (or (> (ite (< (/ 6 (- 7)) (/ 6 (- 6))) (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_5) _let_0) (p0 _let_5 _let_0)))) (ite (p0 _let_13 _let_141) (or (and (or (> (ite (p0 _let_3 (+ (* 6.0 v0) _let_11)) _let_117 _let_98) _let_75) (< _let_60 (ite _let_53 (- v0) _let_62))) (p0 (ite (p0 v0 (* 6.0 v0)) _let_19 _let_1) _let_103)) (not (= (xor (< _let_170 _let_110) (= _let_1 _let_73)) (>= _let_13 _let_145)))) (or (= _let_105 (ite (p0 _let_3 (+ (* 6.0 v0) _let_11)) _let_117 _let_98)) (and (=> (= _let_145 _let_74) (and (p0 (ite (> (- (/ 7 (- 6))) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_100 _let_92) _let_13) (< (* (/ (- 6) 1) _let_10) (ite (p0 _let_1 _let_5) _let_156 _let_115)))) (=> (= (< _let_23 _let_24) (=> (=> (or (> (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65) (ite (distinct (/ _let_21 1) (/ 6 (- 6))) (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14)) _let_130)) (or (p0 _let_96 (ite _let_34 (ite (distinct (/ 6 (- 6)) (/ _let_18 1)) _let_58 _let_90) _let_71)) (=> (= (<= _let_149 _let_97) (>= _let_140 _let_99)) (> _let_26 (ite _let_44 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_20))))) (or (ite (> (f0 (- v0) (/ _let_19 1)) _let_164) (= _let_14 (/ (- _let_2) 1)) (<= _let_142 _let_130)) (=> (ite (distinct (ite _let_34 _let_67 _let_14) _let_122) (p0 (/ 7 (- 6)) _let_169) (not (<= (ite _let_37 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0))) (ite (> (- (/ 7 (- 6))) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_100 _let_92)))) (xor (and (>= _let_73 (/ _let_25 1)) (p0 (ite (p0 (/ _let_25 1) _let_8) _let_58 _let_16) _let_71)) (ite (= _let_158 (ite (< (/ 7 (- 6)) (* (/ (- 6) 1) _let_10)) _let_151 _let_89)) (> _let_146 _let_113) (not (< _let_74 _let_59))))))) (or (or (< _let_173 _let_65) (<= _let_127 _let_155)) (xor (> _let_129 (/ _let_19 1)) (distinct (ite (> (/ _let_21 1) _let_4) _let_74 _let_1) (ite _let_42 (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)) _let_11)))))) (xor (= (or (> (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) _let_100) (= (ite _let_40 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76) _let_120) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (=> (= _let_154 (ite (> _let_3 _let_12) _let_24 _let_2)) (= _let_13 (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)))) (distinct _let_124 (ite _let_51 _let_83 _let_63)) (and (= (= _let_153 (/ _let_18 1)) (distinct (ite (p0 _let_26 _let_14) _let_9 (- _let_2)) (ite _let_31 _let_77 (f0 (- v0) (/ _let_19 1))))) (= _let_69 _let_73)))) (< (ite (> _let_3 _let_12) (* (/ (- 6) 1) _let_10) _let_75) _let_170)))))))) (= (=> (and (<= (f0 (- v0) (/ _let_19 1)) _let_161) (= (ite (>= _let_11 _let_10) _let_80 _let_3) _let_89)) (not (>= _let_162 _let_160))) (>= (ite (< _let_17 _let_5) _let_1 (+ (/ 7 (- 6)) v0)) (ite (> _let_3 _let_12) _let_24 _let_2))))) (=> (and (ite (<= _let_90 (ite _let_34 _let_67 _let_14)) (< (/ _let_21 1) _let_81) (distinct _let_23 _let_85)) (distinct (ite (<= (- _let_7) _let_14) _let_20 _let_13) _let_141)) (xor (not (ite (xor (not (< (ite _let_42 (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)) _let_11) _let_98)) (= (p0 _let_74 (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)) (<= _let_14 _let_123))) (or (distinct _let_105 _let_68) (and (and (> _let_62 _let_1) (distinct _let_111 _let_103)) (p0 (ite _let_27 _let_20 _let_93) (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)))) (p0 _let_135 (ite (distinct (- _let_7) _let_4) _let_21 _let_97)))) (<= (ite (> _let_5 _let_4) _let_22 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16)))))) (xor (ite (ite (=> (xor (xor (and (< _let_124 (ite _let_45 _let_8 _let_6)) (>= _let_1 _let_8)) (= (ite (> (f0 (- v0) (/ _let_19 1)) _let_23) _let_67 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6)) (ite _let_37 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0))))) (or (= (/ 6 (- 6)) (- (/ 7 (- 6)))) (distinct (ite (p0 v0 (* 6.0 v0)) _let_19 _let_1) (ite (<= _let_0 (* 6.0 v0)) (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1))))))) (ite (xor (xor (not (= (= (f1 _let_9 (/ (- _let_2) 1)) (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1)))) (> _let_153 (ite (p0 _let_17 _let_6) _let_0 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6))))) (ite (ite (p0 _let_141 _let_124) (=> (= (> (ite (<= (/ _let_18 1) (/ 6 (- 6))) (* (/ (- 6) 1) _let_10) (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65)) (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) _let_12 (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0))) (= (>= _let_104 _let_129) (= (/ _let_18 1) _let_14))) (xor (>= (ite (p0 _let_16 (- (/ 7 (- 6)))) (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_160) (p0 (ite _let_48 (ite (= _let_22 _let_7) (- _let_7) _let_14) (ite _let_44 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_20)) _let_155))) (and (ite (distinct (/ _let_21 1) (/ 6 (- 6))) (or (= (ite _let_45 _let_8 _let_6) _let_0) (p0 (/ _let_18 1) (ite _let_27 _let_20 _let_93))) (xor (p0 (ite (> (/ _let_19 1) _let_15) _let_80 (ite (p0 _let_26 _let_14) _let_9 (- _let_2))) _let_72) (ite (<= (+ (/ 7 (- 6)) v0) (ite (> (f0 (- v0) (/ _let_19 1)) _let_23) _let_67 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6))) (p0 (ite (<= _let_0 (* 6.0 v0)) (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1)))) _let_166) (< _let_16 (/ _let_2 1))))) (= (xor (=> (= (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_146 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6))))) _let_78) (= (= (and (= _let_171 _let_120) (< _let_59 _let_93)) (<= _let_96 _let_105)) (>= _let_90 (ite _let_33 (ite (= _let_15 _let_12) _let_73 (ite _let_27 _let_20 _let_93)) _let_128)))) (=> (>= (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65) _let_1) _let_45)) (and (= (= _let_58 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0)) (=> (> (ite _let_30 _let_71 _let_151) (f0 (- v0) (/ _let_19 1))) (< (- (- (/ 7 (- 6)))) (ite (> (- v0) (- (/ 7 (- 6)) _let_0)) _let_89 _let_79)))) (= _let_61 (ite (= _let_22 _let_7) (- _let_7) _let_14)))))) (= (< _let_123 _let_151) (>= (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) (ite _let_29 _let_17 v0))) (= (distinct _let_95 (ite (= _let_1 (f1 _let_9 (/ (- _let_2) 1))) _let_102 _let_60)) (<= _let_96 _let_89)))) (and (and (<= (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) _let_156) (xor (or (not (> _let_126 (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)) (ite _let_29 _let_17 v0)))) (= (> _let_100 (ite (>= _let_11 _let_10) _let_80 _let_3)) (=> (= (ite (> _let_3 _let_12) (* (/ (- 6) 1) _let_10) _let_75) (ite (>= (f0 (- v0) (/ _let_19 1)) (+ (/ 7 (- 6)) v0)) _let_4 _let_82)) (or _let_50 (p0 _let_127 (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0))))))) (ite (> _let_98 _let_112) _let_29 (not (ite (> _let_143 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22)) (not (< (ite _let_51 _let_83 _let_63) _let_140)) (p0 _let_68 _let_142)))))) (<= (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0) _let_98))) (=> (or (p0 _let_14 _let_89) (xor (>= _let_62 _let_142) (distinct (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7))))) (=> (or (not (not (xor (distinct _let_160 (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_146 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6)))))) (= _let_16 (ite (distinct _let_9 (/ _let_21 1)) (ite (<= (/ _let_18 1) (/ 6 (- 6))) (* (/ (- 6) 1) _let_10) (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65)) (ite (= _let_24 _let_8) _let_105 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22))))))) (not (p0 (ite (distinct _let_9 (/ _let_21 1)) (ite (<= (/ _let_18 1) (/ 6 (- 6))) (* (/ (- 6) 1) _let_10) (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65)) (ite (= _let_24 _let_8) _let_105 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22))) (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_146 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6)))))))) (>= _let_13 _let_83))) (xor (= (or (=> (distinct _let_156 _let_94) (xor (p0 (/ 7 (- 6)) _let_121) (> _let_99 (ite (>= (* 6.0 v0) _let_22) _let_20 _let_16)))) (p0 (/ 6 (- 7)) (f0 (- v0) (/ _let_19 1)))) (not (distinct (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)) (ite _let_29 _let_17 v0)) _let_96))) (or (not (= (= (or (p0 (/ _let_19 1) _let_158) (distinct (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0) _let_23)) (xor (distinct _let_26 _let_151) (=> (distinct _let_134 _let_172) (or (<= _let_178 _let_71) (>= _let_9 (ite (p0 v0 (* 6.0 v0)) _let_19 _let_1)))))) (xor (= (= (p0 _let_133 _let_121) (= _let_175 (/ _let_19 1))) (not (> (ite (>= (f0 (- v0) (/ _let_19 1)) (+ (/ 7 (- 6)) v0)) _let_4 _let_82) (ite (> (f0 (- v0) (/ _let_19 1)) _let_23) _let_67 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6))))) (<= _let_11 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (- (- (/ 7 (- 6)))) _let_148))))) (= (=> (ite (or (ite (= (<= _let_98 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6))))) (<= _let_23 (ite (p0 _let_3 (+ (* 6.0 v0) _let_11)) _let_117 _let_98))) (<= (- (/ 7 (- 6))) _let_129) (distinct _let_141 (ite (p0 _let_15 _let_6) _let_112 (ite (< (/ 6 (- 7)) (/ 6 (- 6))) (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_5)))) (=> (and (distinct (ite _let_42 _let_145 (/ 6 (- 6))) _let_167) (<= _let_7 (ite (> (/ _let_19 1) _let_15) _let_80 (ite (p0 _let_26 _let_14) _let_9 (- _let_2))))) (> _let_143 _let_62))) (and (= _let_82 _let_181) (not (xor (distinct (f1 _let_9 (/ (- _let_2) 1)) (/ 6 (- 6))) (ite (<= _let_168 _let_83) (= _let_143 _let_8) (>= (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_146 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6))))) _let_150))))) (distinct (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) (ite _let_55 (/ 6 (- 6)) _let_112))) (p0 (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1))) (ite _let_55 (/ 6 (- 6)) _let_112))) (= (= (< (ite (= _let_15 _let_12) _let_73 (ite _let_27 _let_20 _let_93)) _let_16) (=> (< _let_136 (ite (p0 (/ _let_25 1) _let_11) _let_110 _let_101)) (< (ite _let_34 _let_67 _let_14) _let_59))) (= (distinct _let_9 (/ _let_21 1)) _let_28))))))) (ite (=> (and (xor (not (> _let_16 _let_20)) (=> (p0 (/ _let_25 1) (ite _let_29 _let_62 (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)))) (=> (distinct _let_4 (/ (- _let_2) 1)) (>= _let_136 _let_73)))) (not (=> (> _let_83 (ite (<= (/ _let_18 1) (/ 6 (- 6))) (* (/ (- 6) 1) _let_10) (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65))) (or (distinct (ite (p0 (/ _let_25 1) _let_11) _let_110 _let_101) (ite (<= (- _let_7) _let_14) _let_20 _let_13)) (> (ite (p0 (/ _let_25 1) _let_11) _let_110 _let_101) (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1)))))))) (not (=> (=> (or (or (xor (and (and (=> (<= (/ 6 (- 7)) (ite (= (- v0) (/ 6 (- 6))) _let_72 _let_6)) (not (=> (<= (/ 7 (- 6)) (ite (< (/ 6 (- 7)) (/ 6 (- 6))) (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_5)) (= (/ _let_18 1) _let_104)))) (>= _let_101 _let_26)) (<= _let_147 (ite (p0 _let_3 (+ (* 6.0 v0) _let_11)) _let_117 _let_98))) (distinct _let_177 (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)))) (=> (= (ite (= _let_15 _let_12) _let_73 (ite _let_27 _let_20 _let_93)) (ite (distinct (- _let_7) _let_4) _let_21 _let_97)) (and (=> (and (xor (= _let_172 _let_164) (p0 _let_155 (ite _let_42 (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)) _let_11))) (xor (>= _let_167 (/ _let_21 1)) (> _let_10 _let_4))) (=> (and (and (<= (* (/ (- 6) 1) _let_10) _let_66) (> (ite (>= _let_20 _let_4) _let_123 _let_134) (* (/ (- 6) 1) _let_10))) (and (ite (and (=> (distinct (ite (> (- (/ 7 (- 6))) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_100 _let_92) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16)) (>= _let_119 (ite (> (/ _let_19 1) _let_15) _let_80 (ite (p0 _let_26 _let_14) _let_9 (- _let_2))))) (distinct (/ _let_18 1) (+ (/ 7 (- 6)) v0))) (> (ite (<= (/ _let_25 1) _let_16) _let_24 _let_82) (ite (= _let_1 (f1 _let_9 (/ (- _let_2) 1))) _let_102 _let_60)) (>= _let_22 (ite (p0 _let_16 (- (/ 7 (- 6)))) (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)))) (not (>= (- (/ 7 (- 6))) (ite _let_43 _let_111 (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)))))))) (< _let_3 _let_101))) (>= (ite _let_43 _let_102 _let_26) _let_171)))) (= (<= (- _let_7) _let_73) (=> (> (ite _let_29 _let_17 v0) (ite _let_43 _let_111 (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))))) (= _let_1 (f1 _let_9 (/ (- _let_2) 1)))))) (=> (not (<= _let_23 _let_23)) (ite (> _let_119 _let_136) (distinct _let_6 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6)) (<= (ite (p0 v0 (* 6.0 v0)) _let_19 _let_1) _let_151)))) (xor (< _let_16 (ite (= _let_22 _let_7) (- _let_7) _let_14)) (distinct (ite (<= _let_0 (* 6.0 v0)) (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1)))) _let_162))))) (not (or (and (=> (ite (p0 (f1 _let_9 (/ (- _let_2) 1)) _let_143) (=> (or (< (/ _let_2 1) (ite (distinct _let_9 (/ _let_21 1)) (ite (<= (/ _let_18 1) (/ 6 (- 6))) (* (/ (- 6) 1) _let_10) (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65)) (ite (= _let_24 _let_8) _let_105 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22)))) (>= (/ _let_25 1) (ite _let_44 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_20))) (and (=> (p0 _let_157 _let_131) (or (not (<= (ite (< (/ _let_2 1) _let_24) _let_10 _let_26) _let_12)) (> _let_115 _let_165))) (not (< (ite (= v0 _let_6) _let_21 _let_63) _let_181)))) (ite (or (> (f0 (- v0) (/ _let_19 1)) _let_66) (p0 _let_10 (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0))) (not (not (> (ite (< (/ 7 (- 6)) (* (/ (- 6) 1) _let_10)) _let_151 _let_89) (/ (- _let_2) 1)))) (distinct (/ 6 (- 6)) (/ _let_18 1)))) (= (>= _let_88 _let_116) (>= _let_132 (ite (= _let_1 (f1 _let_9 (/ (- _let_2) 1))) _let_102 _let_60)))) (= _let_179 _let_138)) (or (not (= (< (- (- (/ 7 (- 6)))) _let_11) _let_41)) (= (ite (p0 (- (/ 7 (- 6)) _let_0) _let_11) (distinct (ite (p0 (/ _let_25 1) _let_8) _let_58 _let_16) _let_161) (xor (distinct _let_26 _let_20) (> (- (/ 7 (- 6))) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))))) (>= (ite (p0 _let_16 (- (/ 7 (- 6)))) (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_130))))) (ite (< _let_119 _let_100) (ite (or (distinct _let_112 _let_12) (xor (or (=> (p0 (ite (>= (/ 6 (- 6)) _let_8) _let_12 _let_1) _let_115) (>= _let_76 _let_105)) (= (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0) _let_139)) (and (or (distinct (/ 6 (- 6)) (/ 6 (- 6))) (p0 _let_162 _let_89)) (=> (and (xor (distinct _let_77 _let_147) (ite (> (/ _let_21 1) _let_4) (and (<= _let_57 (ite _let_42 (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)) _let_11)) (<= _let_75 (ite (> _let_3 _let_12) (* (/ (- 6) 1) _let_10) _let_75))) (= _let_15 _let_12))) (or (>= (ite (= (- v0) (/ 6 (- 6))) _let_72 _let_6) (ite _let_34 (ite (distinct (/ 6 (- 6)) (/ _let_18 1)) _let_58 _let_90) _let_71)) (or (= _let_23 _let_143) (<= _let_13 (- (/ 7 (- 6))))))) (p0 _let_16 (+ (/ 7 (- 6)) v0)))))) (<= _let_110 (f1 _let_9 (/ (- _let_2) 1))) (> (ite _let_43 _let_111 (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)))) (ite _let_27 (* (/ (- 6) 1) _let_10) (ite (= (/ _let_18 1) _let_14) _let_75 (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1))))))) (not (> _let_130 _let_112)))) (not (not (> _let_118 _let_175)))) (not (or (=> (xor (ite (distinct _let_22 (ite (p0 v0 (* 6.0 v0)) _let_19 _let_1)) (< _let_123 _let_65) (xor (or (distinct (ite (<= _let_0 (* 6.0 v0)) (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1)))) _let_123) (ite (not (>= _let_142 _let_15)) (p0 (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65) _let_155) (p0 _let_86 (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14))))) (=> (= _let_7 _let_150) (= _let_160 _let_23)))) (and (xor (not (=> (or (or (< (/ 6 (- 6)) (ite _let_43 _let_111 (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))))) (< _let_170 _let_20)) (>= _let_118 _let_99)) (> _let_0 (ite (= (- v0) (/ 6 (- 6))) _let_72 _let_6)))) (=> (=> (xor (<= _let_83 (ite (= _let_24 _let_8) _let_105 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22))) (p0 _let_136 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76))) (= (or (< _let_13 (* 6.0 v0)) (or (> (- (- (/ 7 (- 6)))) (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1)))) (< _let_175 (ite (> (/ _let_2 1) _let_9) _let_25 _let_3)))) (distinct _let_131 _let_142))) (= (ite _let_43 _let_102 _let_26) _let_147))) (or (or (distinct _let_68 _let_90) (distinct (ite (distinct _let_26 (f1 _let_9 (/ (- _let_2) 1))) (* 6.0 v0) v0) _let_180)) (ite (<= _let_7 (ite (distinct _let_26 _let_20) (/ 6 (- 7)) _let_57)) (xor (> (ite (<= (- _let_7) _let_14) _let_20 _let_13) _let_0) (>= (ite (>= (/ _let_18 1) _let_1) (- (/ 7 (- 6)) _let_0) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16)) _let_94)) (distinct (ite (distinct v0 (/ 6 (- 6))) _let_81 _let_91) (ite (> (/ _let_2 1) _let_9) _let_25 _let_3)))))) (=> (or (and (ite (>= (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)) (ite _let_29 _let_17 v0)) _let_23) (or _let_27 (=> (distinct (f1 _let_9 (/ (- _let_2) 1)) _let_17) (<= _let_162 _let_11))) (and (xor (=> (distinct (* (/ (- 6) 1) _let_10) _let_131) (= _let_134 _let_113)) (or (= (xor (p0 (ite (= _let_1 (f1 _let_9 (/ (- _let_2) 1))) _let_102 _let_60) _let_159) (= (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) _let_78)) (<= _let_12 (+ (* 6.0 v0) _let_11))) (= _let_23 _let_57))) (= (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0) (ite (= v0 _let_6) _let_21 _let_63)))) (or (= (p0 _let_131 _let_134) (<= (ite (distinct v0 (/ 6 (- 6))) _let_81 _let_91) _let_7)) (distinct _let_95 _let_91))) (or (> _let_5 _let_8) (= (>= (ite _let_45 _let_8 _let_6) _let_0) (<= (- (/ 7 (- 6))) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)))))) (not (ite (xor (= (not (not (<= _let_59 (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_146 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6)))))))) (= (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)) (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0))) (xor (>= (+ (/ 7 (- 6)) v0) _let_6) (= (>= (ite _let_34 (ite (distinct (/ 6 (- 6)) (/ _let_18 1)) _let_58 _let_90) _let_71) _let_120) (>= _let_60 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (- (- (/ 7 (- 6)))) _let_148))))) (or (distinct (ite (= _let_24 _let_8) _let_105 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22)) _let_24) (or (> (ite _let_55 (/ 6 (- 6)) _let_112) (ite (>= (/ _let_19 1) _let_8) _let_118 (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)))) (>= _let_83 (ite (p0 _let_16 (- (/ 7 (- 6)))) (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))))) (xor (xor (<= (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) (ite (= v0 _let_6) _let_21 _let_63)) (> _let_91 (ite (distinct (/ 6 (- 6)) (/ _let_18 1)) _let_58 _let_90))) (not (xor (distinct _let_106 _let_60) (> _let_142 _let_57)))))))) (and (= (or (not (ite (= (xor (<= _let_1 _let_172) (> (ite (> (/ _let_2 1) _let_9) _let_25 _let_3) (/ _let_18 1))) (> (ite _let_54 _let_63 _let_25) (ite (p0 (/ _let_25 1) _let_8) _let_58 _let_16))) (xor (p0 (ite (<= (/ _let_18 1) (/ 6 (- 6))) (* (/ (- 6) 1) _let_10) (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65)) (ite (distinct _let_9 (/ _let_21 1)) (ite (<= (/ _let_18 1) (/ 6 (- 6))) (* (/ (- 6) 1) _let_10) (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65)) (ite (= _let_24 _let_8) _let_105 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22)))) (not (<= (ite (> (- (/ 7 (- 6))) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_100 _let_92) (ite (< (/ 6 (- 7)) (/ 6 (- 6))) (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_5)))) (and (or (xor (or (p0 _let_57 (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) v0)) (/ 7 (- 6)) _let_81)) (p0 _let_89 (ite (distinct _let_9 (/ _let_21 1)) (ite (<= (/ _let_18 1) (/ 6 (- 6))) (* (/ (- 6) 1) _let_10) (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65)) (ite (= _let_24 _let_8) _let_105 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22))))) (xor (>= (ite _let_29 _let_17 v0) (ite _let_42 _let_145 (/ 6 (- 6)))) (ite (= (ite (>= (* 6.0 v0) _let_22) _let_20 _let_16) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) (> (ite (> (f0 (- v0) (/ _let_19 1)) _let_23) _let_67 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6)) (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)) (distinct (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1))) (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)))))) (>= (ite (distinct (/ _let_21 1) (/ 6 (- 6))) (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14)) _let_130) (ite _let_51 _let_83 _let_63))) (ite (ite (>= _let_11 _let_161) (> _let_113 (ite (> (/ _let_19 1) _let_15) _let_80 (ite (p0 _let_26 _let_14) _let_9 (- _let_2)))) (> _let_91 _let_12)) (p0 (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1))) _let_78) (distinct _let_90 _let_13))))) (= (=> (<= _let_168 _let_80) (= (p0 _let_11 _let_11) (distinct _let_145 (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_146 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6)))))))) (= (= (> _let_179 _let_121) (>= _let_69 _let_58)) (ite _let_183 (< (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) v0)) (/ 7 (- 6)) _let_81) (ite (> (f0 (- v0) (/ _let_19 1)) _let_23) _let_67 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6))) _let_183)))) (ite (xor (<= (/ 6 (- 6)) (ite _let_29 _let_17 v0)) (< _let_145 _let_134)) (=> (distinct _let_5 (ite (>= (/ _let_18 1) _let_1) (- (/ 7 (- 6)) _let_0) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16))) (p0 (/ (- _let_2) 1) (ite (= v0 _let_6) _let_21 _let_63))) _let_56)) (= (ite (<= (/ _let_18 1) (/ 6 (- 6))) (and (>= _let_152 _let_179) (< _let_24 (ite _let_44 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_20))) (p0 (/ _let_19 1) (ite _let_44 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_20))) (> _let_181 _let_128))))) (xor (and (=> (ite (xor (or (=> (not (ite (distinct _let_181 (ite (= _let_1 (f1 _let_9 (/ (- _let_2) 1))) _let_102 _let_60)) (xor (> (+ (* 6.0 v0) _let_11) (ite (> _let_3 _let_12) (* (/ (- 6) 1) _let_10) _let_75)) (< (ite (distinct (/ 6 (- 6)) (/ _let_18 1)) _let_58 _let_90) (ite (<= (/ _let_25 1) _let_16) _let_24 _let_82))) (not (< _let_171 _let_114)))) (xor (distinct (ite (>= _let_1 _let_8) (+ (/ 7 (- 6)) v0) _let_19) (ite (> (f0 (- v0) (/ _let_19 1)) _let_23) _let_67 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6))) (> (* (/ (- 6) 1) _let_10) (ite (> _let_3 _let_12) _let_24 _let_2)))) (not (not (or (> _let_112 _let_141) (and (p0 _let_76 (ite (> (/ 7 (- 6)) _let_16) (- (/ 7 (- 6))) (ite _let_53 (- v0) _let_62))) (< (ite (>= (/ 6 (- 6)) _let_8) _let_12 _let_1) (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22))))))) (or (>= _let_11 _let_10) (>= _let_6 _let_178))) (ite (= _let_22 (ite _let_27 (* (/ (- 6) 1) _let_10) (ite (= (/ _let_18 1) _let_14) _let_75 (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1)))))) (and (ite (> (ite (> (/ _let_21 1) _let_4) _let_74 _let_1) (/ 6 (- 7))) (= _let_130 (- (/ 7 (- 6)) _let_0)) (ite (< _let_180 _let_162) (>= (ite _let_46 (ite (> (/ _let_2 1) _let_9) _let_25 _let_3) _let_66) (/ _let_21 1)) (> _let_71 (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))))) (= (>= (/ 7 (- 6)) (ite (<= (/ _let_18 1) (/ 6 (- 6))) (* (/ (- 6) 1) _let_10) (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65))) (not (< _let_24 (/ 6 (- 6)))))) (> (* (/ (- 6) 1) _let_10) (ite (> (/ 7 (- 6)) _let_16) (- (/ 7 (- 6))) (ite _let_53 (- v0) _let_62)))) (ite (p0 (/ 6 (- 6)) (ite (= _let_22 _let_7) (- _let_7) _let_14)) (= (<= (ite (> (f0 (- v0) (/ _let_19 1)) _let_23) _let_67 (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6)) _let_128) (ite (= _let_82 (ite (<= _let_0 (* 6.0 v0)) (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1))))) (and (or (distinct _let_70 _let_95) (xor (>= (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6) _let_85) (>= (ite (p0 v0 (* 6.0 v0)) _let_19 _let_1) (ite (= v0 _let_6) _let_21 _let_63)))) (=> (< _let_114 (/ 6 (- 6))) (=> (>= (ite (= (/ _let_18 1) _let_14) _let_75 (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1)))) _let_176) (and (<= (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (- (- (/ 7 (- 6)))) _let_148) (* (/ (- 6) 1) _let_10)) (= _let_9 (/ _let_25 1)))))) (not (>= _let_125 (f1 _let_9 (/ (- _let_2) 1)))))) (= (= (>= (ite _let_40 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76) _let_120) _let_9) (< _let_17 _let_20)) (xor (ite (ite (distinct (ite (= _let_22 _let_7) (- _let_7) _let_14) (ite (> _let_5 _let_4) _let_22 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6)))))) (ite (=> (distinct (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76) _let_121) (p0 (ite (p0 _let_3 (+ (* 6.0 v0) _let_11)) _let_117 _let_98) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16))) (= (>= _let_17 (/ 6 (- 6))) (p0 _let_22 (/ _let_25 1))) (> (/ _let_2 1) _let_9)) (= (ite _let_44 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_20) _let_103)) (<= _let_138 _let_174) (=> (> _let_4 (/ 6 (- 6))) (p0 (ite (distinct (+ (* 6.0 v0) _let_11) (/ 7 (- 6))) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)) (ite _let_29 _let_17 v0)) _let_57))) (p0 (ite (p0 _let_16 (- (/ 7 (- 6)))) (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) (ite (p0 (/ _let_25 1) _let_11) _let_110 _let_101)))))) (ite (and (= (ite (> _let_17 (ite _let_48 (ite (>= (/ _let_19 1) _let_8) _let_118 (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (p0 v0 (* 6.0 v0)) _let_19 _let_1))) (not (<= _let_92 _let_63)) (>= _let_117 (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)))) (p0 (/ _let_2 1) (/ (- _let_2) 1))) (=> (xor (xor (= _let_94 _let_131) (>= (ite (< (/ 7 (- 6)) (* (/ (- 6) 1) _let_10)) _let_151 _let_89) _let_165)) (= (ite (<= _let_0 (* 6.0 v0)) (ite (<= (/ _let_25 1) _let_5) (ite (> (/ _let_2 1) _let_10) _let_58 (- _let_7)) (ite _let_53 (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57) _let_65)) (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1)))) _let_6)) (= (ite (< (/ 6 (- 7)) (/ 6 (- 6))) (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) _let_5) _let_176))) (and (> _let_118 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (- (- (/ 7 (- 6)))) _let_148)) (or (= (> (f0 (- v0) (/ _let_19 1)) _let_23) (= _let_78 _let_64)) (distinct _let_135 _let_7))) (=> (> _let_3 _let_12) (not (=> (not (< (ite _let_43 _let_102 _let_26) _let_154)) (distinct (ite _let_37 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22) (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0))) _let_23)))))) (or (> (/ _let_19 1) _let_161) (not (= (ite (= _let_138 (ite _let_51 _let_83 _let_63)) (distinct _let_94 (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16)) (= (p0 _let_112 _let_162) (p0 _let_71 _let_170))) (or (or (not (> (ite _let_40 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76) _let_120) (* (/ (- 6) 1) _let_10))) (or (and (=> (ite (= (ite (>= _let_20 _let_4) _let_123 _let_134) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)) (< (ite _let_53 (- v0) _let_62) (ite (distinct (/ _let_21 1) (/ 6 (- 6))) (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14)) _let_130)) (>= (/ 6 (- 6)) _let_24)) (and (> (ite _let_43 _let_102 _let_26) (ite (> _let_3 _let_12) _let_9 (ite _let_34 _let_67 _let_14))) (= (xor (distinct (ite (p0 (/ _let_25 1) _let_8) _let_58 _let_16) _let_122) (p0 (ite (> _let_3 _let_12) _let_24 _let_2) _let_120)) (not (or (>= (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_146 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6))))) (+ (* 6.0 v0) _let_11)) (> (ite (>= _let_20 _let_4) _let_123 _let_134) (ite (> _let_3 _let_12) _let_24 _let_2))))))) (and (> (ite (>= _let_1 _let_8) (+ (/ 7 (- 6)) v0) _let_19) (ite _let_53 (- v0) _let_62)) (< _let_64 (/ 6 (- 6))))) (or (xor (p0 _let_128 _let_178) (<= _let_81 _let_126)) (xor (= (and (not (not (ite (> _let_107 (ite (< (/ 7 (- 6)) (* (/ (- 6) 1) _let_10)) _let_151 _let_89)) (< (ite (= (/ _let_18 1) (f0 (- v0) (/ _let_19 1))) (* 6.0 v0) _let_6) _let_60) (p0 _let_16 _let_142)))) (xor (> _let_23 (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16)))) (< (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) _let_24))) (=> (=> (= v0 _let_145) (ite (=> (distinct v0 (/ 6 (- 6))) (<= _let_5 _let_9)) (> (ite _let_27 (* (/ (- 6) 1) _let_10) (ite (= (/ _let_18 1) _let_14) _let_75 (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1))))) _let_107) (<= _let_70 (ite (> (- (/ 7 (- 6))) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_100 _let_92)))) (< (/ 6 (- 7)) (ite _let_30 _let_71 _let_151)))) (distinct _let_118 _let_158))))) (not (< (ite (= _let_1 (f1 _let_9 (/ (- _let_2) 1))) _let_102 _let_60) (ite (p0 _let_3 (+ (* 6.0 v0) _let_11)) _let_117 _let_98)))))))) (= (=> (and (=> (or (= (ite (> (/ 7 (- 6)) _let_16) (- (/ 7 (- 6))) (ite _let_53 (- v0) _let_62)) _let_77) (and (<= (f1 _let_9 (/ (- _let_2) 1)) _let_87) (=> (p0 _let_79 _let_105) (<= (ite (>= _let_14 _let_0) (- _let_7) (* 6.0 v0)) _let_117)))) (ite (= (p0 (ite _let_34 (ite (distinct (/ 6 (- 6)) (/ _let_18 1)) _let_58 _let_90) _let_71) (ite (p0 _let_26 _let_14) _let_9 (- _let_2))) (= (= (distinct _let_62 _let_115) (distinct _let_125 (ite (>= (/ _let_18 1) _let_1) (- (/ 7 (- 6)) _let_0) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16)))) (and (>= (/ _let_18 1) (ite _let_29 _let_17 v0)) (>= _let_70 _let_131)))) (< _let_6 _let_4) (>= _let_155 _let_140))) (= (=> (= (=> (ite (p0 _let_147 (ite (= _let_24 _let_8) _let_105 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22))) (distinct _let_127 (/ 6 (- 6))) (= _let_124 _let_133)) (= (> _let_117 (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) v0)) (/ 7 (- 6)) _let_81)) (= _let_13 _let_11))) (= (= (>= (ite (= (/ _let_18 1) _let_14) _let_75 (ite (p0 (- v0) _let_15) _let_58 (f1 _let_9 (/ (- _let_2) 1)))) _let_57) (xor (< (ite (>= (f0 (- v0) (/ _let_19 1)) (+ (/ 7 (- 6)) v0)) _let_4 _let_82) _let_62) (< _let_16 _let_155))) (ite (not (or (p0 (ite (= _let_1 (f1 _let_9 (/ (- _let_2) 1))) _let_102 _let_60) _let_150) (< (ite _let_34 (ite (distinct (/ 6 (- 6)) (/ _let_18 1)) _let_58 _let_90) _let_71) _let_108))) (not (xor (and (> _let_86 _let_4) (> (ite _let_53 (- v0) _let_62) _let_154)) (>= _let_177 (ite (distinct (- _let_7) _let_4) _let_21 _let_97)))) (p0 _let_162 _let_165)))) (and (ite (p0 (ite (> _let_5 _let_4) _let_22 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6))))) (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6))))) (= (and (and (distinct _let_101 _let_88) (< _let_97 _let_3)) (ite (=> (<= _let_127 _let_144) (= _let_181 (ite _let_38 _let_19 _let_80))) _let_53 (= (ite (= v0 _let_6) _let_21 _let_63) (ite _let_31 _let_77 (f0 (- v0) (/ _let_19 1)))))) (<= (ite (p0 _let_1 _let_5) _let_156 _let_115) (ite _let_43 _let_102 _let_26))) (=> (>= (ite (>= _let_1 _let_8) (+ (/ 7 (- 6)) v0) _let_19) _let_140) (distinct _let_84 (ite _let_42 (ite (distinct _let_12 _let_15) _let_4 (ite (>= _let_13 _let_6) (ite _let_45 _let_8 _let_6) _let_76)) _let_11)))) (not (p0 (ite (>= (/ _let_18 1) _let_1) (- (/ 7 (- 6)) _let_0) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16)) _let_157)))) (ite (<= _let_81 _let_162) (= _let_24 _let_8) (distinct _let_4 _let_165)))) (not (ite (not (and _let_36 (or (=> (>= _let_16 _let_119) (xor (< _let_129 _let_100) (> _let_5 _let_4))) (> _let_68 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (- (- (/ 7 (- 6)))) _let_148))))) (=> (=> (ite (distinct _let_73 _let_93) (p0 _let_15 _let_11) (>= (ite (= _let_24 _let_8) _let_105 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22)) (ite (distinct (/ _let_25 1) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_146 (ite (< _let_13 (+ (/ 7 (- 6)) v0)) (ite (<= (/ 6 (- 7)) (* (/ (- 6) 1) _let_10)) (ite _let_53 (- v0) _let_62) _let_13) (- (/ 7 (- 6))))))) (=> (> (ite (p0 _let_16 (- (/ 7 (- 6)))) (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_20) (> (/ _let_2 1) _let_10))) (= (= (p0 (ite (< (/ _let_2 1) _let_24) _let_7 (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0)) _let_130) (>= _let_70 (ite (> (- (/ 7 (- 6))) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0))) _let_100 _let_92))) (<= _let_167 _let_151))) (xor (or (not (= _let_130 (ite _let_54 _let_63 _let_25))) _let_35) (=> (or (or (p0 (ite _let_29 _let_17 v0) _let_62) (>= _let_73 (ite (distinct _let_9 (/ _let_21 1)) (ite (<= (/ _let_18 1) (/ 6 (- 6))) (* (/ (- 6) 1) _let_10) (ite (> _let_4 (/ 6 (- 6))) _let_10 _let_65)) (ite (= _let_24 _let_8) _let_105 (ite (p0 _let_11 _let_11) (+ (/ 7 (- 6)) (+ (/ 7 (- 6)) v0)) _let_22))))) (< (+ (* 6.0 v0) _let_11) _let_5)) (or (= _let_153 (ite (> (/ 7 (- 6)) _let_16) (- (/ 7 (- 6))) (ite _let_53 (- v0) _let_62))) (<= _let_14 _let_14))))))) (= (not (= (= (not _let_47) (xor (= _let_61 (ite (distinct (- _let_7) _let_4) _let_21 _let_97)) _let_44)) (= _let_153 (ite (= _let_1 (f1 _let_9 (/ (- _let_2) 1))) _let_102 _let_60)))) (xor (=> (ite (> _let_127 (ite (<= (- _let_7) _let_14) _let_20 _let_13)) (not (distinct (ite (> (/ _let_19 1) _let_15) _let_80 (ite (p0 _let_26 _let_14) _let_9 (- _let_2))) _let_76)) (p0 (ite (> (f1 _let_9 (/ (- _let_2) 1)) (- (- (/ 7 (- 6))))) (ite (<= _let_20 _let_1) (f0 (- v0) (/ _let_19 1)) _let_16) (ite _let_47 (/ 6 (- 7)) (ite (> (/ (- _let_2) 1) _let_20) (f1 _let_9 (/ (- _let_2) 1)) _let_16))) (ite (> _let_5 (- (/ 7 (- 6)) _let_0)) _let_10 _let_57))) (<= (/ _let_25 1) _let_16)) (ite (< _let_97 _let_10) (not (and (= _let_118 (ite (> (/ _let_19 1) _let_15) _let_80 (ite (p0 _let_26 _let_14) _let_9 (- _let_2)))) (not _let_30))) (=> (= (ite (= (f1 _let_9 (/ (- _let_2) 1)) _let_17) (- (/ 7 (- 6)) _let_0) v0) _let_87) (> (ite (>= _let_24 _let_8) _let_25 (f1 _let_9 (/ (- _let_2) 1))) _let_127)))))))) (=> (=> _let_184 _let_184) (not (and (= _let_107 _let_110) (=> (or (< _let_140 _let_64) (and (distinct _let_148 _let_138) (>= _let_138 _let_123))) (not (or (>= _let_68 _let_94) (or (and (distinct _let_174 _let_85) (= _let_39 (distinct _let_147 _let_12))) (= (distinct _let_115 _let_92) (> _let_108 _let_175))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ))