(declare-fun b () String)
(declare-fun a () String)
(declare-fun c () String)
(assert (or (distinct (str.substr a 167 (str.len b)) "")))
(assert (let ((a!1 (str.len (str.substr (str.replace (str.replace a b "") "29M8u" "")
                                220
                                (* 92 (str.len c) 109))))
      (a!2 (= (str.at (str.replace (str.replace a b "") "29M8u" "") 141) ""))
      (a!3 (distinct (str.len (str.replace (str.replace a b "") "29M8u" ""))
                     200))
      (a!4 (to_real (str.len (str.replace (str.replace a b "") "29M8u" "")))))
  (or (distinct (ite (= a!1 121) 130 211)
                (ite a!2 168 213)
                (ite a!3 243 102)
                24)
      (< (/ (/ 29.0 a!4) 200.0) 109.0))))
(check-sat)