(set-logic QF_S)
(declare-fun var0 () String)
(assert (str.in.re var0 (re.++ (re.* (re.union (re.+ (re.union (re.* (re.+ (re.* (re.+ (re.union (re.+ (re.+ (re.union (re.+ (re.* (str.to.re "00"))) (re.+ (re.+ (str.to.re "111")))))) (re.+ (re.union (re.union (re.+ (re.union (str.to.re "222") (str.to.re "333"))) (re.+ (re.union (str.to.re "44") (str.to.re "5")))) (re.union (re.+ (re.* (str.to.re "6"))) (re.+ (re.* (str.to.re "777"))))))))))) (re.* (re.union (re.union (re.* (re.* (re.* (re.+ (re.union (re.+ (re.+ (str.to.re "8"))) (re.+ (re.+ (str.to.re "9")))))))) (re.* (re.+ (re.* (re.union (re.+ (re.+ (re.union (str.to.re "aa") (str.to.re "b")))) (re.+ (re.+ (re.+ (str.to.re "c"))))))))) (re.union (re.union (re.+ (re.+ (re.* (re.+ (re.union (re.+ (str.to.re "d")) (re.+ (str.to.re "ee"))))))) (re.+ (re.+ (re.union (re.* (re.union (re.+ (str.to.re "fff")) (re.+ (str.to.re "ggg")))) (re.* (re.+ (re.union (str.to.re "hh") (str.to.re "ii")))))))) (re.union (re.* (re.+ (re.* (re.+ (re.union (re.union (str.to.re "jjj") (str.to.re "kkk")) (re.union (str.to.re "ll") (str.to.re "mm"))))))) (re.* (re.* (re.+ (re.+ (re.union (re.* (str.to.re "nnn")) (re.* (str.to.re "ooo"))))))))))))) (re.+ (re.* (re.* (re.+ (re.union (re.+ (re.union (re.union (re.+ (re.union (re.+ (re.+ (str.to.re "ppp"))) (re.+ (re.union (str.to.re "qq") (str.to.re "r"))))) (re.+ (re.union (re.* (re.* (str.to.re "s"))) (re.* (re.* (str.to.re "t")))))) (re.union (re.union (re.union (re.union (re.union (str.to.re "uu") (str.to.re "v")) (re.union (str.to.re "ww") (str.to.re "x"))) (re.union (re.union (str.to.re "yy") (str.to.re "zz")) (re.union (str.to.re "A") (str.to.re "BB")))) (re.union (re.+ (re.* (str.to.re "CC"))) (re.+ (re.union (str.to.re "DDD") (str.to.re "EE"))))) (re.union (re.* (re.* (re.union (str.to.re "FFF") (str.to.re "GGG")))) (re.* (re.* (re.+ (str.to.re "HHH")))))))) (re.+ (re.* (re.+ (re.union (re.+ (re.+ (re.* (str.to.re "II")))) (re.+ (re.+ (re.+ (str.to.re "JJJ"))))))))))))))) (re.union (re.+ (re.* (re.* (re.+ (re.+ (re.union (re.union (re.+ (re.union (re.* (re.* (re.union (re.+ (str.to.re "K")) (re.+ (str.to.re "L"))))) (re.* (re.* (re.+ (re.* (str.to.re "M"))))))) (re.+ (re.union (re.+ (re.union (re.* (re.* (str.to.re "NNN"))) (re.* (re.* (str.to.re "OOO"))))) (re.+ (re.* (re.* (re.* (str.to.re "P")))))))) (re.union (re.+ (re.union (re.* (re.* (re.+ (re.union (str.to.re "QQ") (str.to.re "RRR"))))) (re.* (re.* (re.union (re.union (str.to.re "SS") (str.to.re "TTT")) (re.union (str.to.re "UU") (str.to.re "V"))))))) (re.+ (re.union (re.* (re.* (re.+ (re.* (str.to.re "W"))))) (re.* (re.* (re.union (re.* (str.to.re "XXX")) (re.* (str.to.re "Y")))))))))))))) (re.+ (re.* (re.union (re.* (re.union (re.union (re.* (re.* (re.* (re.+ (re.+ (re.* (re.* (str.to.re "ZZ")))))))) (re.* (re.* (re.union (re.union (re.union (re.* (re.+ (str.to.re "!!"))) (re.* (re.* (str.to.re """")))) (re.union (re.* (re.union (str.to.re "##") (str.to.re "$"))) (re.* (re.+ (str.to.re "%"))))) (re.union (re.* (re.* (re.* (str.to.re "&&")))) (re.* (re.+ (re.* (str.to.re "'''"))))))))) (re.union (re.+ (re.* (re.* (re.union (re.+ (re.+ (re.+ (str.to.re "((")))) (re.+ (re.+ (re.union (str.to.re "))") (str.to.re "*")))))))) (re.+ (re.* (re.union (re.* (re.* (re.+ (re.+ (str.to.re "+"))))) (re.* (re.union (re.* (re.union (str.to.re ",") (str.to.re "---"))) (re.* (re.* (str.to.re ".."))))))))))) (re.* (re.* (re.* (re.+ (re.+ (re.* (re.union (re.* (re.union (re.+ (str.to.re "///")) (re.+ (str.to.re ":::")))) (re.* (re.+ (re.union (str.to.re ";;;") (str.to.re "<<<"))))))))))))))))))
(assert (<= 15 (str.len var0)))
(check-sat)