(set-logic QF_S)
(declare-fun var0 () String)
(assert (RegexIn var0 (RegexConcat (RegexStar (RegexStar (Str2Reg "00"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "11"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "22")) (RegexStar (Str2Reg "33"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "44"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "5") (Str2Reg "66"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "7") (Str2Reg "88"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "999")) (RegexPlus (Str2Reg "aa"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "bbb"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "ccc"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "dd"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "ee"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "fff"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "g"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "h") (Str2Reg "ii"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "j") (Str2Reg "kk"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "l"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "mm") (Str2Reg "n"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "ooo")) (RegexStar (Str2Reg "pp"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "qq"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "rr") (Str2Reg "s"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "tt") (Str2Reg "uuu")) (RegexUnion (Str2Reg "vv") (Str2Reg "www"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "xx"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "yy"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "zzz") (Str2Reg "AA"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "B"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "CCC")) (RegexPlus (Str2Reg "D"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "E"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "F") (Str2Reg "G")) (RegexUnion (Str2Reg "H") (Str2Reg "I"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "JJJ") (Str2Reg "KK"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "LL") (Str2Reg "M"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "N") (Str2Reg "OOO")) (RegexUnion (Str2Reg "PP") (Str2Reg "QQ"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "R"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "SS") (Str2Reg "T")) (RegexUnion (Str2Reg "UUU") (Str2Reg "VVV"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "WW"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "XX"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "YY") (Str2Reg "Z"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "!!") (Str2Reg "\"\""))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "###"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "$$") (Str2Reg "%%%")) (RegexUnion (Str2Reg "&") (Str2Reg "''"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "(") (Str2Reg ")"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "**") (Str2Reg "+")) (RegexUnion (Str2Reg ",,") (Str2Reg "-"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg ".."))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "//"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "::"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg ";;;"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "<<") (Str2Reg "=")) (RegexUnion (Str2Reg ">") (Str2Reg "?"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "@"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "[[[")) (RegexStar (Str2Reg "\\\\\\"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "]]]"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "^^^"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "___") (Str2Reg "```"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "{{{") (Str2Reg "||"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "}}") (Str2Reg "~~"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "00"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "1"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "2")) (RegexPlus (Str2Reg "3"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "444")) (RegexStar (Str2Reg "55"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "666")) (RegexPlus (Str2Reg "77"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "888"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "99")) (RegexStar (Str2Reg "aaa"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "bbb") (Str2Reg "c"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "d") (Str2Reg "e"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "ff") (Str2Reg "g"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "hhh"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "iii")) (RegexStar (Str2Reg "jj"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "kkk") (Str2Reg "lll")) (RegexUnion (Str2Reg "mm") (Str2Reg "nn"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "ooo")) (RegexStar (Str2Reg "pp"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "qqq"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "rrr") (Str2Reg "sss"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "tt") (Str2Reg "uuu"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "vv"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "ww"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "xxx") (Str2Reg "yy"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "z"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "AA"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "BB"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "CCC"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "DD"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "EEE")) (RegexStar (Str2Reg "F"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "GGG")) (RegexStar (Str2Reg "HHH"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "II") (Str2Reg "J"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "KKK"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "LLL")) (RegexStar (Str2Reg "M"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "NNN"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "O")) (RegexPlus (Str2Reg "PP"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "QQ") (Str2Reg "RRR"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "SSS")) (RegexPlus (Str2Reg "T"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "U") (Str2Reg "VV")) (RegexUnion (Str2Reg "WW") (Str2Reg "XXX"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "Y"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "ZZZ"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "!!!")) (RegexPlus (Str2Reg "\""))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "###"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "$$"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "%%") (Str2Reg "&&")) (RegexUnion (Str2Reg "''") (Str2Reg "(("))) (RegexConcat (RegexStar (RegexStar (Str2Reg ")))"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "*"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "+++") (Str2Reg ",,"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "---") (Str2Reg ".")) (RegexUnion (Str2Reg "/") (Str2Reg "::"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg ";;") (Str2Reg "<")) (RegexUnion (Str2Reg "=") (Str2Reg ">>"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "???"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "@"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "[["))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "\\")) (RegexStar (Str2Reg "]]"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "^^") (Str2Reg "_")) (RegexUnion (Str2Reg "``") (Str2Reg "{{"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "||")) (RegexPlus (Str2Reg "}"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "~~"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "00"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "1"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "2") (Str2Reg "3"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "44"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "5"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "666") (Str2Reg "7")) (RegexUnion (Str2Reg "8") (Str2Reg "99"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "aa")) (RegexStar (Str2Reg "b"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "cc") (Str2Reg "dd")) (RegexUnion (Str2Reg "eee") (Str2Reg "ff"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "g"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "hh") (Str2Reg "iii"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "jj"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "kkk")) (RegexPlus (Str2Reg "l"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "mm"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "nn"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "oo"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "pp"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "qqq"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "rr"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "s"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "t"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "uu"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "vv"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "w"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "x") (Str2Reg "yy"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "z")) (RegexPlus (Str2Reg "AA"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "BBB"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "C"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "DDD") (Str2Reg "EE")) (RegexUnion (Str2Reg "FFF") (Str2Reg "GGG"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "H"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "II"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "J"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "K") (Str2Reg "L")) (RegexUnion (Str2Reg "MM") (Str2Reg "N"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "OO") (Str2Reg "P")) (RegexUnion (Str2Reg "QQ") (Str2Reg "RRR"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "SSS"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "T") (Str2Reg "U"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "VV")) (RegexPlus (Str2Reg "WWW"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "X"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "YY")) (RegexStar (Str2Reg "ZZZ"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "!!!"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "\"") (Str2Reg "##")) (RegexUnion (Str2Reg "$$$") (Str2Reg "%%%"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "&&&")) (RegexStar (Str2Reg "'"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "(") (Str2Reg "))"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "*"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "+")) (RegexPlus (Str2Reg ",,"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "--") (Str2Reg ".."))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "//")) (RegexPlus (Str2Reg "::"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg ";;"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "<<<")) (RegexPlus (Str2Reg "==="))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg ">>>") (Str2Reg "?")) (RegexUnion (Str2Reg "@@@") (Str2Reg "[[["))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "\\\\") (Str2Reg "]"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "^^"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "_"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "`")) (RegexPlus (Str2Reg "{{{"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "|"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "}}}"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "~~~") (Str2Reg "0"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "11")) (RegexPlus (Str2Reg "2"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "333") (Str2Reg "4")) (RegexUnion (Str2Reg "555") (Str2Reg "6"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "7") (Str2Reg "8")) (RegexUnion (Str2Reg "9") (Str2Reg "aaa"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "bb") (Str2Reg "cc"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "d") (Str2Reg "ee"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "fff") (Str2Reg "gg"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "hhh") (Str2Reg "i"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "jj")) (RegexPlus (Str2Reg "kk"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "ll"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "mm")) (RegexStar (Str2Reg "nn"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "oo"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "ppp"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "q"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "rrr")) (RegexStar (Str2Reg "sss"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "ttt")) (RegexStar (Str2Reg "u"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "v") (Str2Reg "w"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "xxx"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "y") (Str2Reg "z")) (RegexUnion (Str2Reg "AAA") (Str2Reg "BB"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "CC"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "DDD") (Str2Reg "E"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "F")) (RegexStar (Str2Reg "GGG"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "HH") (Str2Reg "II"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "JJJ"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "KK"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "L")) (RegexPlus (Str2Reg "MMM"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "NN"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "OO")) (RegexStar (Str2Reg "P"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "QQQ"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "RRR") (Str2Reg "S"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "T")) (RegexPlus (Str2Reg "UU"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "VV")) (RegexPlus (Str2Reg "WW"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "XX"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "YYY"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "ZZ"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "!!"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "\"\"\""))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "#") (Str2Reg "$$$"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "%%")) (RegexPlus (Str2Reg "&&&"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "'''") (Str2Reg "((")) (RegexUnion (Str2Reg "))") (Str2Reg "***"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "+") (Str2Reg ",,"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "---")) (RegexPlus (Str2Reg "..."))) (RegexUnion (RegexStar (Str2Reg "//")) (RegexStar (Str2Reg ":"))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)