(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(assert (and (distinct (str.substr a 60 (str.len b)) "")))
(assert
 (or
  (distinct
   (ite (distinct
         (str.len (str.substr (str.replace (str.replace a b "") "29M8u" "")
                   204
                   (- 11 (str.len c) 234)))
         210) 209 248)
   (ite (= (str.at (str.replace (str.replace a b "") "29M8u" "") 234) "") 205 98)
   (ite (distinct (str.len (str.replace (str.replace a b "") "29M8u" "")) 41) 172 27)
   217)
  (< (* 131 (str.len (str.replace (str.replace a b "") "29M8u" "")) 235) 147)))
(check-sat)