(set-logic QF_S)
(declare-fun var0 () String)
(assert (str.in.re var0 (re.++ (re.union (re.union (str.to.re "00") (str.to.re "11")) (re.union (str.to.re "22") (str.to.re "333"))) (re.++ (re.+ (re.union (str.to.re "4") (str.to.re "55"))) (re.++ (re.+ (re.+ (str.to.re "66"))) (re.++ (re.* (re.+ (str.to.re "7"))) (re.++ (re.union (re.* (str.to.re "888")) (re.* (str.to.re "9"))) (re.++ (re.+ (re.+ (str.to.re "a"))) (re.++ (re.union (re.+ (str.to.re "b")) (re.+ (str.to.re "c"))) (re.++ (re.union (re.union (str.to.re "ddd") (str.to.re "e")) (re.union (str.to.re "fff") (str.to.re "gg"))) (re.++ (re.* (re.* (str.to.re "hhh"))) (re.* (re.+ (str.to.re "iii"))))))))))))))
(check-sat)