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