(set-logic QF_S)
(declare-fun var0 () String)
(assert (RegexIn var0 (RegexConcat (RegexUnion (RegexUnion (Str2Reg "0") (Str2Reg "111")) (RegexUnion (Str2Reg "222") (Str2Reg "333"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "444")) (RegexStar (Str2Reg "5"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "666")) (RegexPlus (Str2Reg "777"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "8")) (RegexStar (Str2Reg "999"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "aaa"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "bb"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "c") (Str2Reg "ddd")) (RegexUnion (Str2Reg "eee") (Str2Reg "f"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "gg"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "hhh"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "i") (Str2Reg "jjj"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "kk"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "ll")) (RegexPlus (Str2Reg "m"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "n"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "o") (Str2Reg "ppp")) (RegexUnion (Str2Reg "qq") (Str2Reg "r"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "ss") (Str2Reg "t"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "u"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "vvv"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "ww")) (RegexStar (Str2Reg "xx"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "yy")) (RegexPlus (Str2Reg "zzz"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "A")) (RegexPlus (Str2Reg "B"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "CCC"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "D"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "EE")) (RegexStar (Str2Reg "F"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "GG"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "HHH") (Str2Reg "III"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "J")) (RegexPlus (Str2Reg "KKK"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "LLL") (Str2Reg "M"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "NN"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "OO") (Str2Reg "P"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "Q"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "R") (Str2Reg "SSS")) (RegexUnion (Str2Reg "TT") (Str2Reg "UUU"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "VV") (Str2Reg "WWW"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "XX")) (RegexPlus (Str2Reg "YYY"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "ZZ") (Str2Reg "!!"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "\"\"\""))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "#")) (RegexPlus (Str2Reg "$$"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "%") (Str2Reg "&&&")) (RegexUnion (Str2Reg "'''") (Str2Reg "(("))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg ")") (Str2Reg "***"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "+++"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg ",,") (Str2Reg "---"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "...") (Str2Reg "//"))) (RegexConcat (RegexStar (RegexStar (Str2Reg ":"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg ";") (Str2Reg "<<"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "="))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg ">>") (Str2Reg "???"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "@"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "[[["))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "\\\\\\") (Str2Reg "]]"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "^"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "___")) (RegexStar (Str2Reg "```"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "{{{")) (RegexPlus (Str2Reg "|"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "}}") (Str2Reg "~~"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "00"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "111"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "22") (Str2Reg "3"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "4")) (RegexPlus (Str2Reg "555"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "66") (Str2Reg "7")) (RegexUnion (Str2Reg "8") (Str2Reg "9"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "aaa"))) (RegexUnion (RegexUnion (Str2Reg "bbb") (Str2Reg "cc")) (RegexUnion (Str2Reg "dd") (Str2Reg "ee")))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)