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