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