(set-logic QF_S) (declare-fun var0 () String) (assert (str.in.re var0 (re.++ (re.+ (re.union (str.to.re "000") (str.to.re "111"))) (re.++ (re.+ (re.union (str.to.re "2") (str.to.re "333"))) (re.++ (re.* (re.+ (str.to.re "444"))) (re.++ (re.+ (re.union (str.to.re "555") (str.to.re "6"))) (re.++ (re.+ (re.* (str.to.re "7"))) (re.++ (re.+ (re.union (str.to.re "8") (str.to.re "99"))) (re.++ (re.union (re.union (str.to.re "aa") (str.to.re "bbb")) (re.union (str.to.re "cc") (str.to.re "d"))) (re.++ (re.* (re.union (str.to.re "eee") (str.to.re "ff"))) (re.++ (re.union (re.union (str.to.re "ggg") (str.to.re "h")) (re.union (str.to.re "iii") (str.to.re "jjj"))) (re.union (re.* (str.to.re "kk")) (re.* (str.to.re "l")))))))))))))) (assert (<= 476 (str.len var0))) (check-sat)