(set-option :incremental false)
(set-info :status sat)
(set-logic QF_UFLRA)
(declare-fun f0 (Real Real) Real)
(declare-fun f1 (Real) Real)
(declare-fun p0 (Real Real) Bool)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(check-sat-assuming ( (let ((_let_0 (+ v1 v1))) (let ((_let_1 (/ 5 3))) (let ((_let_2 (- (- v1)))) (let ((_let_3 (/ 15 15))) (let ((_let_4 (f0 (- v0 (- v1)) (- v1)))) (let ((_let_5 (/ 15 3))) (let ((_let_6 (f1 (+ v1 _let_3)))) (let ((_let_7 (< (/ (ite (p0 (- v1) (+ v1 _let_3)) 1 0) 1) (- v1)))) (let ((_let_8 (>= (- _let_0 (+ _let_2 v2)) _let_1))) (let ((_let_9 (< (+ _let_2 v2) (- v1)))) (let ((_let_10 (>= (- _let_2) v0))) (let ((_let_11 (= _let_2 _let_5))) (let ((_let_12 (<= _let_2 _let_1))) (let ((_let_13 (>= (+ _let_2 v2) (/ (ite (p0 (- v1) (+ v1 _let_3)) 1 0) 1)))) (let ((_let_14 (distinct (f0 (* 15.0 _let_1) _let_3) _let_3))) (let ((_let_15 (p0 _let_6 (- _let_0 (+ _let_2 v2))))) (let ((_let_16 (> _let_1 _let_2))) (let ((_let_17 (<= (/ (ite (p0 (- v1) (+ v1 _let_3)) 1 0) 1) _let_6))) (let ((_let_18 (p0 _let_5 (- _let_2)))) (let ((_let_19 (p0 _let_2 (+ v1 _let_3)))) (let ((_let_20 (<= (- v1) (+ _let_2 v2)))) (let ((_let_21 (< _let_1 v1))) (let ((_let_22 (>= (/ (ite (p0 (- v1) (+ v1 _let_3)) 1 0) 1) _let_4))) (let ((_let_23 (>= _let_1 (f0 (* 15.0 _let_1) _let_3)))) (let ((_let_24 (p0 (- v0 (- v1)) v2))) (let ((_let_25 (>= _let_0 (- v1)))) (let ((_let_26 (< (- _let_2) (- v1)))) (let ((_let_27 (< v2 _let_6))) (let ((_let_28 (< (/ (ite (p0 (- v1) (+ v1 _let_3)) 1 0) 1) _let_2))) (let ((_let_29 (= (+ _let_2 v2) (+ v1 _let_3)))) (let ((_let_30 (< (+ _let_2 v2) (+ v1 _let_3)))) (let ((_let_31 (<= (- _let_2) (f0 (* 15.0 _let_1) _let_3)))) (let ((_let_32 (distinct (- v1) _let_2))) (let ((_let_33 (>= (* 15.0 _let_1) _let_3))) (let ((_let_34 (ite (> (f0 (* 15.0 _let_1) _let_3) (/ (ite (p0 (- v1) (+ v1 _let_3)) 1 0) 1)) _let_1 (ite (= _let_1 _let_4) (- v1) (- v1))))) (let ((_let_35 (ite (> v2 _let_2) _let_6 (* 15.0 _let_1)))) (let ((_let_36 (ite _let_28 (- _let_0 (+ _let_2 v2)) (ite (> v0 (- _let_0 (+ _let_2 v2))) (- v0 (- v1)) _let_2)))) (let ((_let_37 (ite (> _let_3 _let_2) (ite (p0 (- v1) (+ v1 _let_3)) 1 0) _let_34))) (let ((_let_38 (ite (>= (+ _let_2 v2) (+ v1 _let_3)) _let_3 _let_6))) (let ((_let_39 (ite (p0 (- _let_0 (+ _let_2 v2)) _let_1) (f0 (* 15.0 _let_1) _let_3) v2))) (let ((_let_40 (ite (<= (+ _let_2 v2) (+ _let_2 v2)) _let_5 (f0 (* 15.0 _let_1) _let_3)))) (let ((_let_41 (ite _let_12 (- _let_2) (ite (p0 (+ v1 _let_3) _let_0) (- v0 (- v1)) _let_3)))) (let ((_let_42 (ite (p0 (- _let_0 (+ _let_2 v2)) (+ _let_2 v2)) _let_3 _let_34))) (let ((_let_43 (ite _let_22 _let_0 (ite (p0 (- v1) (+ v1 _let_3)) 1 0)))) (let ((_let_44 (ite _let_23 (- _let_0 (+ _let_2 v2)) (ite (distinct (- v1) (f0 (* 15.0 _let_1) _let_3)) (ite (distinct _let_6 _let_1) v1 (- v1)) (- v1))))) (let ((_let_45 (ite _let_31 (ite (= _let_1 _let_4) (- v1) (- v1)) _let_39))) (let ((_let_46 (ite (> (f0 (* 15.0 _let_1) _let_3) (- v1)) (ite (distinct (- v1) (f0 (* 15.0 _let_1) _let_3)) (ite (distinct _let_6 _let_1) v1 (- v1)) (- v1)) (- _let_2)))) (let ((_let_47 (ite (> (- v1) (f0 (* 15.0 _let_1) _let_3)) _let_46 _let_4))) (let ((_let_48 (ite (p0 v1 v1) (+ _let_2 v2) _let_44))) (let ((_let_49 (ite (= _let_1 _let_4) _let_37 _let_2))) (let ((_let_50 (ite (distinct (- v0 (- v1)) _let_3) v1 _let_48))) (let ((_let_51 (ite (= (+ _let_2 v2) _let_2) (f0 (* 15.0 _let_1) _let_3) _let_35))) (let ((_let_52 (ite (distinct (- v0 (- v1)) _let_3) _let_2 _let_48))) (let ((_let_53 (ite _let_11 (ite (>= _let_4 _let_2) (+ _let_2 v2) _let_35) _let_35))) (let ((_let_54 (ite (= v2 _let_2) _let_3 (- v1)))) (let ((_let_55 (ite (= _let_4 _let_3) (ite (distinct (+ _let_2 v2) _let_6) _let_34 _let_35) (- _let_0 (+ _let_2 v2))))) (let ((_let_56 (ite (<= _let_1 (+ _let_2 v2)) _let_5 (ite (> v0 (- _let_0 (+ _let_2 v2))) (- v0 (- v1)) _let_2)))) (let ((_let_57 (ite _let_17 _let_51 (ite _let_9 _let_46 _let_39)))) (let ((_let_58 (ite (= (- v1) _let_3) (ite (= _let_1 _let_4) v0 _let_4) _let_5))) (let ((_let_59 (ite (< _let_3 (- _let_0 (+ _let_2 v2))) _let_49 (ite (<= v2 _let_3) v1 (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39)))))) (let ((_let_60 (ite _let_12 _let_37 _let_55))) (let ((_let_61 (ite _let_30 _let_59 _let_56))) (let ((_let_62 (ite (distinct _let_3 _let_0) _let_37 _let_37))) (let ((_let_63 (ite _let_24 (- v1) (- _let_0 (+ _let_2 v2))))) (let ((_let_64 (ite _let_14 (ite _let_21 v0 (ite (> _let_2 _let_6) (+ v1 _let_3) (* 15.0 _let_1))) (- v0 (- v1))))) (let ((_let_65 (ite _let_11 (ite _let_17 (+ v1 _let_3) (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39))) (- _let_0 (+ _let_2 v2))))) (let ((_let_66 (ite _let_33 (+ v1 _let_3) _let_46))) (let ((_let_67 (ite _let_13 (- _let_2) _let_53))) (let ((_let_68 (ite _let_29 _let_36 _let_1))) (let ((_let_69 (ite (>= _let_2 _let_2) _let_65 (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39))))) (let ((_let_70 (ite (> _let_5 _let_1) (ite _let_9 _let_46 _let_39) (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39))))) (let ((_let_71 (ite _let_30 _let_2 (f0 (* 15.0 _let_1) _let_3)))) (let ((_let_72 (ite (= _let_2 (+ _let_2 v2)) _let_64 _let_71))) (let ((_let_73 (ite _let_24 (- _let_0 (+ _let_2 v2)) (ite _let_9 (ite (p0 (+ v1 _let_3) _let_0) (- v0 (- v1)) _let_3) _let_47)))) (let ((_let_74 (ite (p0 (/ (ite (p0 (- v1) (+ v1 _let_3)) 1 0) 1) _let_3) _let_6 _let_40))) (let ((_let_75 (ite (= _let_2 v2) (+ v1 _let_3) _let_41))) (let ((_let_76 (ite _let_29 _let_53 _let_40))) (let ((_let_77 (ite (< (- v0 (- v1)) (+ v1 _let_3)) _let_4 _let_73))) (let ((_let_78 (ite _let_21 _let_49 _let_63))) (let ((_let_79 (ite _let_15 _let_54 _let_70))) (let ((_let_80 (ite (> v0 (- _let_0 (+ _let_2 v2))) _let_41 _let_1))) (let ((_let_81 (ite (= _let_2 (- v1)) (- v1) (ite _let_27 _let_3 _let_6)))) (let ((_let_82 (ite (distinct _let_3 _let_3) _let_54 _let_44))) (let ((_let_83 (ite (>= (/ (ite (p0 (- v1) (+ v1 _let_3)) 1 0) 1) (+ v1 _let_3)) (ite (p0 (- v1) (+ v1 _let_3)) 1 0) v1))) (let ((_let_84 (ite _let_26 _let_48 _let_63))) (let ((_let_85 (ite (p0 (/ (ite (p0 (- v1) (+ v1 _let_3)) 1 0) 1) _let_3) _let_76 _let_6))) (let ((_let_86 (ite (= (+ v1 _let_3) v0) (ite _let_27 _let_3 _let_6) (+ v1 _let_3)))) (let ((_let_87 (ite (<= _let_6 v0) _let_6 (ite _let_9 (ite (p0 (+ v1 _let_3) _let_0) (- v0 (- v1)) _let_3) _let_47)))) (let ((_let_88 (ite (>= (+ _let_2 v2) (+ v1 _let_3)) _let_63 (ite _let_14 _let_70 (ite (>= v2 _let_5) _let_58 v0))))) (let ((_let_89 (ite (p0 _let_3 v1) _let_0 (ite (distinct _let_6 _let_1) v1 (- v1))))) (let ((_let_90 (ite _let_20 (f0 (* 15.0 _let_1) _let_3) _let_44))) (let ((_let_91 (ite (distinct (- v0 (- v1)) _let_3) _let_60 _let_82))) (let ((_let_92 (ite _let_15 (ite (distinct _let_6 _let_1) v1 (- v1)) v1))) (let ((_let_93 (ite _let_13 _let_50 (+ v1 _let_3)))) (let ((_let_94 (ite (<= _let_4 v2) _let_4 _let_42))) (let ((_let_95 (ite _let_25 _let_73 _let_47))) (let ((_let_96 (ite _let_26 (ite (distinct _let_6 _let_1) v1 (- v1)) _let_63))) (let ((_let_97 (ite (p0 (- v0 (- v1)) _let_1) _let_77 _let_58))) (let ((_let_98 (ite (<= _let_4 v2) (ite (<= v2 _let_3) v1 (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39))) _let_87))) (let ((_let_99 (ite (p0 _let_3 v1) (ite (distinct (+ _let_2 v2) _let_6) _let_34 _let_35) _let_48))) (let ((_let_100 (ite (<= v2 _let_2) _let_35 _let_84))) (let ((_let_101 (ite (>= (+ _let_2 v2) _let_0) (ite _let_14 _let_70 (ite (>= v2 _let_5) _let_58 v0)) _let_95))) (let ((_let_102 (ite (= (- v1) _let_1) _let_45 v2))) (let ((_let_103 (ite (= _let_4 _let_3) _let_0 _let_101))) (let ((_let_104 (ite (> (f0 (* 15.0 _let_1) _let_3) (- v1)) _let_62 (- v1)))) (let ((_let_105 (ite (<= (- v0 (- v1)) (/ (ite (p0 (- v1) (+ v1 _let_3)) 1 0) 1)) _let_42 _let_77))) (let ((_let_106 (ite (distinct (- v1) (f0 (* 15.0 _let_1) _let_3)) _let_58 _let_54))) (let ((_let_107 (ite _let_22 _let_5 _let_44))) (let ((_let_108 (ite (> (- _let_2) v0) _let_36 (ite _let_23 (- v0 (- v1)) _let_71)))) (let ((_let_109 (ite _let_19 v2 _let_40))) (let ((_let_110 (ite _let_9 _let_59 _let_82))) (let ((_let_111 (ite _let_28 _let_60 _let_79))) (let ((_let_112 (ite (> _let_3 _let_2) (ite (distinct _let_3 (- _let_0 (+ _let_2 v2))) (ite _let_27 _let_3 _let_6) _let_64) _let_95))) (let ((_let_113 (ite _let_18 _let_54 _let_58))) (let ((_let_114 (ite (> (- v1) v1) (f0 (* 15.0 _let_1) _let_3) _let_101))) (let ((_let_115 (ite _let_26 (ite (> v0 (- _let_0 (+ _let_2 v2))) (- v0 (- v1)) _let_2) _let_89))) (let ((_let_116 (ite _let_25 (ite (p0 (+ v1 _let_3) _let_0) (- v0 (- v1)) _let_3) _let_64))) (let ((_let_117 (ite (> (- _let_0 (+ _let_2 v2)) v1) (ite (p0 (- v1) (+ v1 _let_3)) 1 0) (ite _let_13 _let_44 _let_35)))) (let ((_let_118 (ite (distinct _let_6 _let_1) _let_56 _let_36))) (let ((_let_119 (ite _let_8 _let_112 _let_4))) (let ((_let_120 (or (distinct (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39)) (ite (distinct (- v1) (f0 (* 15.0 _let_1) _let_3)) (ite (distinct _let_6 _let_1) v1 (- v1)) (- v1))) (= _let_4 _let_3)))) (let ((_let_121 (= (= (= (xor (distinct (+ _let_2 v2) _let_6) (p0 (ite _let_17 (+ v1 _let_3) (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39))) (ite _let_13 _let_44 _let_35))) (distinct _let_3 _let_3)) (and (not (xor _let_20 (>= (ite _let_17 (+ v1 _let_3) (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39))) (ite (> v0 (- _let_0 (+ _let_2 v2))) (ite (<= v2 _let_3) v1 (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39))) _let_39)))) (p0 (ite (>= _let_4 _let_2) (+ _let_2 v2) _let_35) _let_103))) (> _let_105 (ite (distinct _let_6 _let_1) v1 (- v1)))))) (let ((_let_122 (and (or (=> (xor (and (or (= _let_97 v0) (> _let_1 _let_35)) (<= (ite (>= _let_4 _let_2) (+ _let_2 v2) _let_35) _let_93)) (= (ite _let_27 _let_3 _let_6) _let_92)) (not (distinct (ite (p0 _let_5 _let_1) _let_42 _let_5) _let_61))) (not (>= _let_77 (ite _let_14 _let_70 (ite (>= v2 _let_5) _let_58 v0))))) (ite (= (>= _let_68 (ite _let_9 (ite (p0 (+ v1 _let_3) _let_0) (- v0 (- v1)) _let_3) _let_47)) (not (= _let_0 _let_49))) (or (= (distinct (+ v1 _let_3) (ite (= _let_1 _let_4) (- v1) (- v1))) (p0 _let_81 _let_101)) (p0 _let_43 _let_100)) (or (not (= _let_1 _let_4)) (< _let_43 (ite (>= v2 _let_5) _let_58 v0))))))) (let ((_let_123 (not (and (or (> _let_41 _let_40) (or (and (< _let_34 _let_110) (=> (< _let_102 (ite (distinct (f0 (* 15.0 _let_1) _let_3) (- _let_0 (+ _let_2 v2))) _let_41 _let_46)) (and (>= _let_4 _let_2) (>= (ite (distinct _let_3 _let_0) v1 _let_39) (- v0 (- v1)))))) (=> (not (=> (ite (distinct _let_114 _let_72) (p0 (- v0 (- v1)) _let_1) (< (ite (distinct _let_3 (- _let_0 (+ _let_2 v2))) (ite _let_27 _let_3 _let_6) _let_64) _let_84)) (> v0 (ite (distinct _let_3 (- _let_0 (+ _let_2 v2))) (ite _let_27 _let_3 _let_6) _let_64)))) (not (p0 _let_5 _let_1))))) (and (= _let_107 v2) (= (> (+ v1 _let_3) _let_107) (>= _let_103 _let_112))))))) (let ((_let_124 (and (ite (or (>= _let_55 _let_52) (not (or (= (ite (ite (= v2 _let_2) (< _let_3 _let_62) (< (ite (<= v2 _let_3) v1 (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39))) _let_59)) (xor (p0 _let_115 _let_104) (>= _let_36 _let_50)) (or (and (xor (distinct _let_3 _let_92) (p0 (* 15.0 _let_1) (/ (ite (p0 (- v1) (+ v1 _let_3)) 1 0) 1))) (xor (distinct _let_3 _let_92) (p0 (* 15.0 _let_1) (/ (ite (p0 (- v1) (+ v1 _let_3)) 1 0) 1)))) (>= _let_69 _let_40))) (<= (ite (> v0 (- _let_0 (+ _let_2 v2))) (ite (<= v2 _let_3) v1 (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39))) _let_39) _let_66)) (=> (=> (p0 (ite (distinct (+ _let_2 v2) _let_6) _let_34 _let_35) (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39))) (= (=> (= (ite _let_9 (ite (p0 (+ v1 _let_3) _let_0) (- v0 (- v1)) _let_3) _let_47) _let_78) (<= _let_46 _let_78)) (> (- _let_2) v0))) (>= (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39)) _let_115))))) (not (<= _let_95 _let_87)) (or (xor (not (= _let_0 (ite _let_19 (+ v1 _let_3) (ite (distinct _let_3 _let_0) v1 _let_39)))) (ite (distinct _let_38 _let_87) (= _let_1 _let_114) (> _let_93 _let_101))) (= (=> (= (ite (p0 _let_5 _let_1) _let_42 _let_5) _let_58) (< _let_75 _let_3)) (=> (< _let_103 (- v0 (- v1))) (distinct _let_2 (/ (ite (p0 (- v1) (+ v1 _let_3)) 1 0) 1)))))) (and (=> (= (ite (p0 (+ v1 _let_3) _let_0) (- v0 (- v1)) _let_3) (ite _let_9 _let_46 _let_39)) (< _let_52 (ite (>= v0 v1) (ite (= _let_1 _let_4) v0 _let_4) _let_64))) (ite (xor (>= _let_116 _let_75) (not (ite (= _let_2 (- v1)) (= _let_37 _let_114) (> v2 _let_2)))) (=> (not _let_33) (or (and (or (and (> (f0 (* 15.0 _let_1) _let_3) (/ (ite (p0 (- v1) (+ v1 _let_3)) 1 0) 1)) (ite (p0 _let_108 (ite _let_9 _let_46 _let_39)) (distinct (- _let_2) (ite (p0 (+ v1 _let_3) _let_0) (- v0 (- v1)) _let_3)) (<= _let_94 _let_54))) (> (- _let_0 (+ _let_2 v2)) v1)) (distinct _let_111 _let_96)) (not (not (p0 _let_45 (- v1)))))) (not (or (= (< _let_45 _let_83) (< _let_67 (f0 (* 15.0 _let_1) _let_3))) (and (xor (< _let_107 _let_67) (not (= (ite _let_10 _let_82 (ite _let_17 (+ v1 _let_3) (ite (= _let_2 v2) (ite (distinct (- v1) (f0 (* 15.0 _let_1) _let_3)) (ite (distinct _let_6 _let_1) v1 (- v1)) (- v1)) _let_47))) (- v1)))) (xor (<= (ite (distinct (f0 (* 15.0 _let_1) _let_3) (- _let_0 (+ _let_2 v2))) _let_41 _let_46) _let_107) (p0 (- _let_0 (+ _let_2 v2)) (+ _let_2 v2))))))))))) (let ((_let_125 (not (and (> (ite _let_27 _let_3 _let_6) (ite (<= v2 _let_3) v1 (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39)))) (ite (= (ite (> (- v1) v1) (distinct _let_3 (- _let_2)) (distinct _let_3 (- _let_2))) (not (= _let_3 v2))) (or (or (> _let_92 _let_51) (= (distinct (ite _let_7 _let_36 (ite (distinct (- v1) (f0 (* 15.0 _let_1) _let_3)) (ite (distinct _let_6 _let_1) v1 (- v1)) (- v1))) _let_114) (and (>= v0 v1) (= (- v1) _let_3)))) (= _let_71 (ite (p0 (+ v1 _let_3) _let_0) (- v0 (- v1)) _let_3))) (not (= (<= _let_6 v0) (p0 _let_44 (ite _let_21 v0 (ite (> _let_2 _let_6) (+ v1 _let_3) (* 15.0 _let_1))))))))))) (ite (xor (ite (not (=> (ite (ite (xor (< _let_85 _let_94) (=> (=> (ite (> _let_3 _let_2) (= _let_104 _let_63) _let_22) (= _let_62 _let_61)) (< _let_77 _let_56))) (or (not _let_15) (and (xor (> _let_96 _let_57) (distinct _let_84 _let_70)) (>= (- v1) _let_59))) (= (<= v2 _let_3) (and (not (ite (> _let_84 _let_86) (not (> _let_77 _let_117)) (or (>= _let_4 _let_80) (= _let_1 (f0 (* 15.0 _let_1) _let_3))))) (not (= _let_2 (+ _let_2 v2)))))) (distinct _let_1 _let_47) (<= _let_91 _let_74)) (= (or (ite (xor (= _let_90 _let_103) (= (< _let_76 (ite (distinct (f0 (* 15.0 _let_1) _let_3) (- _let_0 (+ _let_2 v2))) _let_41 _let_46)) (< _let_3 (- _let_0 (+ _let_2 v2))))) (=> (> _let_92 _let_64) (distinct _let_57 (ite (distinct (f0 (* 15.0 _let_1) _let_3) (- _let_0 (+ _let_2 v2))) _let_41 _let_46))) (>= (ite (distinct _let_6 _let_1) v1 (- v1)) _let_43)) (xor (xor (<= (- v0 (- v1)) (/ (ite (p0 (- v1) (+ v1 _let_3)) 1 0) 1)) (< _let_45 (ite _let_14 _let_70 (ite (>= v2 _let_5) _let_58 v0)))) (=> (<= _let_101 _let_48) (and (<= _let_41 (ite _let_21 v0 (ite (> _let_2 _let_6) (+ v1 _let_3) (* 15.0 _let_1)))) (distinct (ite (>= v2 _let_5) _let_58 v0) _let_53))))) (ite (>= _let_40 (ite _let_23 (- v0 (- v1)) _let_71)) (xor (= (+ v1 _let_3) v0) (= (= (<= _let_41 _let_88) (distinct _let_107 _let_80)) (< _let_43 (ite (distinct (- v1) (f0 (* 15.0 _let_1) _let_3)) (ite (distinct _let_6 _let_1) v1 (- v1)) (- v1))))) _let_9)))) (or (or (xor (ite (>= (/ (ite (p0 (- v1) (+ v1 _let_3)) 1 0) 1) (+ v1 _let_3)) (>= _let_88 _let_106) (< (ite (distinct (- v1) (f0 (* 15.0 _let_1) _let_3)) (ite (distinct _let_6 _let_1) v1 (- v1)) (- v1)) _let_72)) (<= v1 _let_65)) (= _let_19 (<= _let_85 _let_59))) (ite (xor (=> (and (= _let_68 _let_40) (<= _let_45 _let_118)) (= (- v1) _let_110)) (= _let_102 _let_98)) (ite (= (and (> (- v0 (- v1)) _let_112) (xor (< (- v0 (- v1)) (+ v1 _let_3)) (ite (>= (ite (= _let_2 v2) (ite (distinct (- v1) (f0 (* 15.0 _let_1) _let_3)) (ite (distinct _let_6 _let_1) v1 (- v1)) (- v1)) _let_47) _let_75) (>= _let_110 (ite (<= v2 _let_3) v1 (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39)))) (distinct (- v0 (- v1)) _let_3)))) (xor (distinct _let_38 v0) _let_28)) (not (or (>= _let_97 _let_66) (or (< _let_45 _let_117) (ite (or (not (distinct (ite (> _let_2 _let_6) (+ v1 _let_3) (* 15.0 _let_1)) _let_41)) (< _let_37 _let_70)) (or (> _let_103 (- v1)) (>= _let_2 _let_2)) (not (>= _let_91 (ite _let_21 v0 (ite (> _let_2 _let_6) (+ v1 _let_3) (* 15.0 _let_1))))))))) (=> (= (+ _let_2 v2) _let_2) (= _let_100 _let_54))) (= (and (and (<= _let_77 _let_50) (= (ite (distinct _let_3 (- _let_0 (+ _let_2 v2))) (ite _let_27 _let_3 _let_6) _let_64) _let_106)) (>= _let_51 (ite (distinct (f0 (* 15.0 _let_1) _let_3) (- _let_0 (+ _let_2 v2))) _let_41 _let_46))) (xor (p0 _let_3 _let_73) (or (distinct _let_3 (- _let_0 (+ _let_2 v2))) (< (ite _let_10 _let_82 (ite _let_17 (+ v1 _let_3) (ite (= _let_2 v2) (ite (distinct (- v1) (f0 (* 15.0 _let_1) _let_3)) (ite (distinct _let_6 _let_1) v1 (- v1)) (- v1)) _let_47))) _let_41)))))) (or _let_122 _let_122)) (xor (=> _let_123 _let_123) (and (xor (not (xor (xor (>= (ite (>= v0 v1) (ite (= _let_1 _let_4) v0 _let_4) _let_64) (- v1)) (distinct (- v1) (f0 (* 15.0 _let_1) _let_3))) (> _let_51 _let_52))) (or (not (p0 _let_3 v1)) (not (distinct _let_93 _let_34)))) (= _let_121 _let_121)))) (or (= (and (not (not (=> (> (ite (distinct _let_6 _let_1) v1 (- v1)) _let_90) (not (p0 (ite _let_14 _let_70 (ite (>= v2 _let_5) _let_58 v0)) _let_105))))) (or (and (not (and (or (and (=> (>= _let_77 _let_82) (or (>= _let_3 _let_45) (p0 _let_113 _let_73))) (xor (> (- _let_0 (+ _let_2 v2)) (ite _let_9 (ite (p0 (+ v1 _let_3) _let_0) (- v0 (- v1)) _let_3) _let_47)) (xor (and (xor (not (>= _let_5 _let_45)) _let_13) (> _let_5 _let_1)) (or (ite (= _let_2 v2) (>= v0 _let_61) (> (ite (distinct _let_3 (- _let_2)) _let_34 _let_71) _let_88)) (p0 (- _let_0 (+ _let_2 v2)) _let_1))))) (>= (+ _let_2 v2) _let_0)) (not (=> (ite (> _let_2 _let_6) (= (p0 _let_107 _let_109) (distinct _let_101 _let_63)) _let_24) (ite _let_32 (not (p0 _let_42 _let_3)) (not (p0 _let_4 _let_40))))))) (and (=> (= (= _let_111 (ite (distinct _let_6 _let_1) v1 (- v1))) (< _let_81 _let_64)) (or (= _let_49 _let_103) (> (- v1) (f0 (* 15.0 _let_1) _let_3)))) (>= _let_81 _let_84))) (= (=> (xor (= (= (> _let_58 _let_48) (= _let_99 (ite (distinct (f0 (* 15.0 _let_1) _let_3) (- _let_0 (+ _let_2 v2))) _let_41 _let_46))) (p0 _let_78 _let_72)) (=> (= (=> (distinct _let_87 (f0 (* 15.0 _let_1) _let_3)) (distinct (- _let_2) (ite _let_19 (+ v1 _let_3) (ite (distinct _let_3 _let_0) v1 _let_39)))) (<= _let_72 (ite (distinct _let_6 _let_1) v1 (- v1)))) (xor (>= (+ _let_2 v2) (+ v1 _let_3)) _let_16))) (< _let_119 (ite _let_19 (+ v1 _let_3) (ite (distinct _let_3 _let_0) v1 _let_39)))) (and (= (> _let_79 (ite (<= v2 _let_3) v1 (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39)))) (=> (xor (< _let_4 _let_93) (xor (or (p0 (ite (>= v2 _let_5) _let_58 v0) _let_83) (= (- v1) _let_1)) (<= _let_98 _let_82))) (and (<= _let_1 (+ _let_2 v2)) (=> (p0 v1 v1) (< _let_39 _let_82))))) (p0 (/ (ite (p0 (- v1) (+ v1 _let_3)) 1 0) 1) _let_3))))) (xor _let_125 _let_125)) (not (xor (and (= (< _let_6 (ite (distinct _let_6 _let_1) v1 (- v1))) (or (> _let_107 (ite (> _let_2 _let_6) (+ v1 _let_3) (* 15.0 _let_1))) (ite (>= _let_79 _let_91) (p0 _let_108 _let_102) (and (p0 _let_4 (ite _let_21 v0 (ite (> _let_2 _let_6) (+ v1 _let_3) (* 15.0 _let_1)))) (> _let_67 _let_56))))) (= (not (ite (p0 _let_93 _let_49) (=> (> (f0 (* 15.0 _let_1) _let_3) (- v1)) (> (f0 (* 15.0 _let_1) _let_3) _let_76)) (xor (=> (<= _let_86 v2) (or (ite (or (= (ite (> v0 (- _let_0 (+ _let_2 v2))) (- v0 (- v1)) _let_2) (ite (distinct (- v1) (f0 (* 15.0 _let_1) _let_3)) (ite (distinct _let_6 _let_1) v1 (- v1)) (- v1))) (<= _let_53 (ite (distinct (+ _let_2 v2) _let_6) _let_34 _let_35))) (> _let_71 _let_95) _let_8) (= _let_120 _let_120))) _let_25))) (xor (<= _let_57 _let_3) (>= _let_84 _let_76)))) (or (xor (not (=> (or (=> (= (xor (< (ite _let_9 (ite (p0 (+ v1 _let_3) _let_0) (- v0 (- v1)) _let_3) _let_47) _let_78) (distinct _let_47 _let_40)) (<= (ite _let_16 _let_4 (- _let_2)) (- _let_0 (+ _let_2 v2)))) (>= v2 _let_5)) (< _let_65 _let_66)) (and (=> (> _let_79 _let_108) (distinct _let_6 (* 15.0 _let_1))) (>= _let_81 _let_107)))) (not (xor (=> (xor (xor (or (not (not (<= (ite (<= v2 _let_3) v1 (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39))) (ite (= _let_1 _let_4) (- v1) (- v1))))) (not (distinct (ite (>= v0 v1) (ite (= _let_1 _let_4) v0 _let_4) _let_64) _let_109))) (= (xor (<= v2 _let_2) (or (>= _let_43 (ite _let_17 (+ v1 _let_3) (ite (= _let_2 v2) (ite (distinct (- v1) (f0 (* 15.0 _let_1) _let_3)) (ite (distinct _let_6 _let_1) v1 (- v1)) (- v1)) _let_47))) (> _let_34 _let_88))) (xor (>= _let_100 (ite (>= v2 _let_5) _let_58 v0)) (ite (ite (distinct (f0 (* 15.0 _let_1) _let_3) (- _let_0 (+ _let_2 v2))) (= (ite _let_17 (+ v1 _let_3) (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39))) _let_117) (<= (+ _let_2 v2) (+ _let_2 v2))) (xor (>= _let_73 _let_115) (= _let_42 _let_110)) (and (> _let_96 _let_97) (=> (p0 (ite _let_27 _let_3 _let_6) _let_111) (= (>= _let_1 _let_106) (> (ite (>= v2 _let_5) _let_58 v0) _let_53)))))))) (or (=> (= _let_3 _let_2) (not (>= (ite (>= v2 _let_5) _let_58 v0) _let_118))) (xor (not _let_21) (<= _let_4 v2)))) (ite (and (>= _let_86 _let_68) (and (> _let_109 _let_39) (= (= (ite _let_9 _let_46 _let_39) _let_103) (= _let_44 (ite (distinct _let_3 _let_0) v1 _let_39))))) (= (<= _let_80 _let_108) (>= _let_63 _let_95)) (not (<= _let_61 (ite (> v0 (- _let_0 (+ _let_2 v2))) (- v0 (- v1)) _let_2))))) (or (and (ite (>= _let_74 _let_87) (not (distinct (ite (>= v0 v1) (ite (= _let_1 _let_4) v0 _let_4) _let_64) _let_116)) (p0 _let_69 v0)) _let_11) (= (>= (ite (= _let_1 _let_4) v0 _let_4) _let_73) (> (+ _let_2 v2) (ite (= _let_1 _let_4) v0 _let_4))))))) (= (ite _let_124 (or (not (xor (distinct _let_118 v1) (>= v1 _let_97))) (xor (=> (= v0 _let_78) (> _let_3 _let_96)) (and (and (< _let_3 _let_93) (<= (- _let_2) (ite (distinct _let_3 _let_0) v1 _let_39))) _let_29))) _let_124) (ite (ite (not (ite (not (= (- _let_2) _let_110)) (xor (not (< _let_117 _let_60)) (p0 _let_82 (- v1))) (=> (= (> (- v0 (- v1)) _let_68) (< (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39)) _let_108)) (p0 _let_117 _let_119)))) (not (p0 _let_37 _let_63)) (=> (=> (not (or (not (and (ite (xor (> _let_77 (ite (distinct _let_3 (- _let_0 (+ _let_2 v2))) (ite _let_27 _let_3 _let_6) _let_64)) (<= _let_83 _let_103)) (<= _let_99 _let_80) (and (<= _let_2 _let_73) (not _let_7))) (= _let_86 _let_73))) _let_31)) (=> (= (or (and (=> (>= (ite _let_9 (ite (p0 (+ v1 _let_3) _let_0) (- v0 (- v1)) _let_3) _let_47) _let_61) _let_12) (=> (= (= _let_49 _let_104) (<= (ite (distinct _let_3 _let_0) v1 _let_39) v1)) (and (= _let_95 (ite _let_9 (ite (p0 (+ v1 _let_3) _let_0) (- v0 (- v1)) _let_3) _let_47)) (distinct _let_74 _let_89)))) (or _let_10 (=> (distinct _let_62 _let_75) (ite (=> (p0 (ite (> _let_2 _let_6) (+ v1 _let_3) (* 15.0 _let_1)) _let_108) (and (>= (ite _let_32 _let_71 _let_77) _let_43) _let_30)) (p0 (+ v1 _let_3) _let_0) (or (p0 _let_69 _let_106) (<= _let_55 _let_41)))))) (= _let_47 _let_79)) (ite (or (or _let_14 (= _let_113 _let_117)) (= _let_63 _let_107)) (and (= (or (distinct _let_100 (ite (<= v2 _let_3) v1 (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39)))) (distinct _let_58 _let_75)) (ite (ite (= _let_49 _let_93) (p0 _let_107 _let_72) (and (distinct _let_80 _let_61) (= _let_63 (+ v1 _let_3)))) (distinct _let_79 _let_48) (= _let_49 (ite (= _let_1 _let_4) v0 _let_4)))) (=> (not (< _let_65 _let_51)) (p0 _let_112 _let_56))) _let_26))) (>= _let_92 _let_43))) (not (= (and (p0 (ite _let_9 _let_46 _let_39) (ite _let_17 (+ v1 _let_3) (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39)))) (p0 _let_96 _let_50)) (or (or (=> (or (= (ite _let_17 (+ v1 _let_3) (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39))) _let_109) (= _let_36 _let_65)) (not (= _let_5 _let_112))) (=> (distinct _let_6 _let_1) (< _let_77 _let_115))) (< _let_59 _let_3)))) (not (= _let_23 (xor (p0 _let_38 v2) (< _let_116 _let_97)))))))))) (and (and (not (and (= (<= (ite (<= v2 _let_3) v1 (ite (= _let_3 _let_2) _let_0 (ite (distinct _let_3 _let_0) v1 _let_39))) _let_47) (> _let_3 _let_61)) (and (or (>= _let_105 _let_74) (< _let_102 _let_53)) (or (<= _let_65 _let_84) (distinct _let_3 _let_0))))) (not (or (=> (= (not _let_18) (and (p0 _let_4 _let_66) (>= _let_110 _let_6))) (and (and (> v0 (- _let_0 (+ _let_2 v2))) (> _let_36 _let_37)) (ite (not _let_17) (<= _let_108 _let_94) (=> (> _let_49 v1) (>= _let_101 _let_78))))) (> _let_54 _let_111)))) _let_27)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ))