(set-logic QF_S)
(declare-fun var0 () String)
(assert (str.in.re var0 (re.++ (re.union (re.union (str.to.re "0") (str.to.re "111")) (re.union (str.to.re "222") (str.to.re "333"))) (re.++ (re.union (re.* (str.to.re "444")) (re.* (str.to.re "5"))) (re.++ (re.union (re.+ (str.to.re "666")) (re.+ (str.to.re "777"))) (re.++ (re.union (re.* (str.to.re "8")) (re.* (str.to.re "999"))) (re.++ (re.+ (re.+ (str.to.re "aaa"))) (re.++ (re.* (re.+ (str.to.re "bb"))) (re.++ (re.union (re.union (str.to.re "c") (str.to.re "ddd")) (re.union (str.to.re "eee") (str.to.re "f"))) (re.++ (re.+ (re.* (str.to.re "gg"))) (re.++ (re.+ (re.+ (str.to.re "hhh"))) (re.++ (re.* (re.union (str.to.re "i") (str.to.re "jjj"))) (re.++ (re.+ (re.* (str.to.re "kk"))) (re.++ (re.union (re.+ (str.to.re "ll")) (re.+ (str.to.re "m"))) (re.++ (re.+ (re.+ (str.to.re "n"))) (re.++ (re.union (re.union (str.to.re "o") (str.to.re "ppp")) (re.union (str.to.re "qq") (str.to.re "r"))) (re.++ (re.* (re.union (str.to.re "ss") (str.to.re "t"))) (re.++ (re.* (re.* (str.to.re "u"))) (re.++ (re.* (re.+ (str.to.re "vvv"))) (re.++ (re.union (re.* (str.to.re "ww")) (re.* (str.to.re "xx"))) (re.++ (re.union (re.+ (str.to.re "yy")) (re.+ (str.to.re "zzz"))) (re.++ (re.union (re.+ (str.to.re "A")) (re.+ (str.to.re "B"))) (re.++ (re.+ (re.+ (str.to.re "CCC"))) (re.++ (re.+ (re.+ (str.to.re "D"))) (re.++ (re.union (re.* (str.to.re "EE")) (re.* (str.to.re "F"))) (re.++ (re.+ (re.+ (str.to.re "GG"))) (re.++ (re.* (re.union (str.to.re "HHH") (str.to.re "III"))) (re.++ (re.union (re.+ (str.to.re "J")) (re.+ (str.to.re "KKK"))) (re.++ (re.* (re.union (str.to.re "LLL") (str.to.re "M"))) (re.++ (re.* (re.* (str.to.re "NN"))) (re.++ (re.* (re.union (str.to.re "OO") (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 "TT") (str.to.re "UUU"))) (re.++ (re.+ (re.union (str.to.re "VV") (str.to.re "WWW"))) (re.++ (re.union (re.+ (str.to.re "XX")) (re.+ (str.to.re "YYY"))) (re.++ (re.+ (re.union (str.to.re "ZZ") (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.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.* (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.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.+ (str.to.re "{{{")) (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 "111"))) (re.++ (re.+ (re.union (str.to.re "22") (str.to.re "3"))) (re.++ (re.union (re.+ (str.to.re "4")) (re.+ (str.to.re "555"))) (re.++ (re.union (re.union (str.to.re "66") (str.to.re "7")) (re.union (str.to.re "8") (str.to.re "9"))) (re.++ (re.+ (re.* (str.to.re "aaa"))) (re.union (re.union (str.to.re "bbb") (str.to.re "cc")) (re.union (str.to.re "dd") (str.to.re "ee")))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)