(set-logic QF_S)
(declare-fun var0 () String)
(assert (RegexIn var0 (RegexConcat (RegexPlus (RegexUnion (Str2Reg "000") (Str2Reg "111"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "2") (Str2Reg "333"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "444"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "555") (Str2Reg "6"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "7"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "8") (Str2Reg "99"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "aa") (Str2Reg "bbb")) (RegexUnion (Str2Reg "cc") (Str2Reg "d"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "eee") (Str2Reg "ff"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "ggg") (Str2Reg "h")) (RegexUnion (Str2Reg "iii") (Str2Reg "jjj"))) (RegexUnion (RegexStar (Str2Reg "kk")) (RegexStar (Str2Reg "l"))))))))))))))
(assert (<= 476 (Length var0)))
(check-sat)