(set-logic QF_S)
(declare-fun var0 () String)
(assert (RegexIn var0 (RegexConcat (RegexUnion (RegexUnion (Str2Reg "00") (Str2Reg "11")) (RegexUnion (Str2Reg "2") (Str2Reg "333"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "444") (Str2Reg "555")) (RegexUnion (Str2Reg "666") (Str2Reg "77"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "888") (Str2Reg "999"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "a"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "bbb") (Str2Reg "cc"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "ddd"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "eee"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "fff"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "ggg"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "hhh"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "ii"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "jjj") (Str2Reg "kk")) (RegexUnion (Str2Reg "ll") (Str2Reg "mmm"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "nnn")) (RegexStar (Str2Reg "oo"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "p") (Str2Reg "q"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "r"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "sss"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "t") (Str2Reg "uu")) (RegexUnion (Str2Reg "v") (Str2Reg "w"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "xxx")) (RegexPlus (Str2Reg "y"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "zzz") (Str2Reg "AAA"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "BBB"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "CCC") (Str2Reg "DDD")) (RegexUnion (Str2Reg "EEE") (Str2Reg "FF"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "GGG"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "HHH") (Str2Reg "I"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "J")) (RegexStar (Str2Reg "KKK"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "L")) (RegexPlus (Str2Reg "MM"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "N") (Str2Reg "OO"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "P"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "Q"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "R") (Str2Reg "SSS")) (RegexUnion (Str2Reg "T") (Str2Reg "UUU"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "V"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "WW")) (RegexStar (Str2Reg "XX"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "Y"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "ZZ"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "!!")) (RegexPlus (Str2Reg "\"\""))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "##"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "$$") (Str2Reg "%%%"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "&&") (Str2Reg "'"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "(") (Str2Reg ")))")) (RegexUnion (Str2Reg "***") (Str2Reg "+"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg ","))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "-") (Str2Reg "."))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "/") (Str2Reg ":")) (RegexUnion (Str2Reg ";;;") (Str2Reg "<"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "==") (Str2Reg ">>"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "?")) (RegexPlus (Str2Reg "@@@"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "[[") (Str2Reg "\\"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "]]]") (Str2Reg "^^"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "___"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "```")) (RegexPlus (Str2Reg "{{"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "||"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "}}"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "~") (Str2Reg "00"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "1")) (RegexStar (Str2Reg "22"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "33") (Str2Reg "444"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "55") (Str2Reg "66"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "777") (Str2Reg "888"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "9"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "aaa"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "bb")) (RegexPlus (Str2Reg "ccc"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "d")) (RegexStar (Str2Reg "e"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "ff") (Str2Reg "g"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "hhh")) (RegexStar (Str2Reg "ii"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "j") (Str2Reg "kk")) (RegexUnion (Str2Reg "l") (Str2Reg "mmm"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "nnn") (Str2Reg "oo")) (RegexUnion (Str2Reg "ppp") (Str2Reg "q"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "rr") (Str2Reg "sss")) (RegexUnion (Str2Reg "tt") (Str2Reg "u"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "vv"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "w"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "xxx")) (RegexPlus (Str2Reg "yy"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "z"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "AA"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "B"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "CCC")) (RegexPlus (Str2Reg "DD"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "EE") (Str2Reg "F"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "GG") (Str2Reg "HH"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "III") (Str2Reg "J"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "K")) (RegexStar (Str2Reg "LLL"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "MM"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "NN")) (RegexStar (Str2Reg "OOO"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "PP") (Str2Reg "Q")) (RegexUnion (Str2Reg "RR") (Str2Reg "SS"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "T"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "UUU"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "V")) (RegexPlus (Str2Reg "W"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "XX")) (RegexStar (Str2Reg "Y"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "ZZ")) (RegexStar (Str2Reg "!!!"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "\"\"") (Str2Reg "###")) (RegexUnion (Str2Reg "$") (Str2Reg "%"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "&&") (Str2Reg "'''"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "((("))) (RegexConcat (RegexStar (RegexUnion (Str2Reg ")))") (Str2Reg "**"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "+") (Str2Reg ",,"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "-"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "..."))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "//"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg ":::") (Str2Reg ";;"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "<"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "=")) (RegexPlus (Str2Reg ">>"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "?") (Str2Reg "@")) (RegexUnion (Str2Reg "[") (Str2Reg "\\\\\\"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "]]]") (Str2Reg "^^^")) (RegexUnion (Str2Reg "___") (Str2Reg "```"))) (RegexPlus (RegexPlus (Str2Reg "{"))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(assert (not (RegexIn var0 (RegexConcat (RegexUnion (RegexPlus (Str2Reg "00")) (RegexPlus (Str2Reg "111"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "2")) (RegexPlus (Str2Reg "3"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "4"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "55"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "66") (Str2Reg "777"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "888"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "999"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "aaa") (Str2Reg "bb"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "cc"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "dd"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "ee") (Str2Reg "ff")) (RegexUnion (Str2Reg "ggg") (Str2Reg "h"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "iii")) (RegexStar (Str2Reg "jjj"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "k")) (RegexPlus (Str2Reg "l"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "mmm") (Str2Reg "nn"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "oo") (Str2Reg "pp"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "qqq"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "r")) (RegexPlus (Str2Reg "ss"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "ttt") (Str2Reg "uu"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "v"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "w"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "x"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "y"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "zzz") (Str2Reg "AAA"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "BBB"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "C") (Str2Reg "DD"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "EEE"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "FF") (Str2Reg "G"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "H")) (RegexStar (Str2Reg "I"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "J"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "KKK"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "LL")) (RegexPlus (Str2Reg "MMM"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "N"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "OOO") (Str2Reg "P"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "Q") (Str2Reg "RR")) (RegexUnion (Str2Reg "SS") (Str2Reg "TTT"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "UUU")) (RegexPlus (Str2Reg "V"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "WW"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "XXX"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "YYY"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "Z"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "!!")) (RegexStar (Str2Reg "\"\""))) (RegexConcat (RegexStar (RegexStar (Str2Reg "###"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "$$$"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "%") (Str2Reg "&&"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "'''"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "(((")) (RegexPlus (Str2Reg ")"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "*") (Str2Reg "++"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg ",,") (Str2Reg "---"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg ".") (Str2Reg "//"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg ":::") (Str2Reg ";;;")) (RegexUnion (Str2Reg "<") (Str2Reg "=="))) (RegexConcat (RegexStar (RegexUnion (Str2Reg ">") (Str2Reg "??"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "@@@"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "[[["))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "\\\\\\")) (RegexStar (Str2Reg "]"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "^^"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "__"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "`") (Str2Reg "{{{"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "|||")) (RegexPlus (Str2Reg "}"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "~~"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "000") (Str2Reg "11"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "22"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "333") (Str2Reg "44"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "55") (Str2Reg "666"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "7") (Str2Reg "8")) (RegexUnion (Str2Reg "999") (Str2Reg "aaa"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "b"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "c") (Str2Reg "d"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "ee"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "f"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "ggg") (Str2Reg "hh"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "iii"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "jjj") (Str2Reg "k"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "ll"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "mm")) (RegexPlus (Str2Reg "n"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "ooo") (Str2Reg "p"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "qq"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "rr"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "sss") (Str2Reg "ttt"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "uu"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "v") (Str2Reg "www"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "xxx")) (RegexStar (Str2Reg "yy"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "z"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "AA") (Str2Reg "BB"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "CCC") (Str2Reg "D")) (RegexUnion (Str2Reg "EEE") (Str2Reg "FFF"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "GGG"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "HHH"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "I") (Str2Reg "J"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "KKK") (Str2Reg "LLL"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "M")) (RegexPlus (Str2Reg "NNN"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "OO")) (RegexStar (Str2Reg "PPP"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "Q") (Str2Reg "RRR"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "S")) (RegexPlus (Str2Reg "TT"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "UU"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "VVV"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "W") (Str2Reg "XXX"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "YYY")) (RegexStar (Str2Reg "ZZ"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "!!"))) (RegexPlus (RegexStar (Str2Reg "\"\"")))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)