(set-logic QF_S)
(declare-fun var0 () String)
(assert (RegexIn var0 (RegexConcat (RegexUnion (RegexUnion (Str2Reg "00") (Str2Reg "11")) (RegexUnion (Str2Reg "22") (Str2Reg "333"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "4") (Str2Reg "55"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "66"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "7"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "888")) (RegexStar (Str2Reg "9"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "a"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "b")) (RegexPlus (Str2Reg "c"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "ddd") (Str2Reg "e")) (RegexUnion (Str2Reg "fff") (Str2Reg "gg"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "hhh"))) (RegexStar (RegexPlus (Str2Reg "iii"))))))))))))))
(check-sat)