(set-logic QF_S) (declare-fun var0 () String) (assert (RegexIn var0 (RegexConcat (RegexPlus (RegexUnion (Str2Reg "0") (Str2Reg "11"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "22"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "3")) (RegexStar (Str2Reg "444"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "55"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "66") (Str2Reg "777"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "8"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "99"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "a")) (RegexStar (Str2Reg "b"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "ccc"))) (RegexStar (RegexStar (Str2Reg "dd")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexStar (Str2Reg "0"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "111"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "22") (Str2Reg "333"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "44"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "5"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "66"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "77")) (RegexPlus (Str2Reg "8"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "99") (Str2Reg "aa"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "bbb"))) (RegexPlus (RegexPlus (Str2Reg "c")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexPlus (RegexUnion (Str2Reg "000") (Str2Reg "11"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "222"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "3") (Str2Reg "4"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "55") (Str2Reg "66"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "777") (Str2Reg "888"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "999") (Str2Reg "a"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "b") (Str2Reg "c"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "dd") (Str2Reg "eee"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "fff"))) (RegexPlus (RegexStar (Str2Reg "ggg")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexUnion (Str2Reg "00") (Str2Reg "111"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "2")) (RegexPlus (Str2Reg "333"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "444"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "5") (Str2Reg "666")) (RegexUnion (Str2Reg "777") (Str2Reg "88"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "99") (Str2Reg "aa"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "bb") (Str2Reg "cc")) (RegexUnion (Str2Reg "dd") (Str2Reg "ee"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "fff") (Str2Reg "gg"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "hhh") (Str2Reg "i")) (RegexUnion (Str2Reg "j") (Str2Reg "k"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "l")) (RegexStar (Str2Reg "mmm"))) (RegexStar (RegexPlus (Str2Reg "nn")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexUnion (Str2Reg "0") (Str2Reg "11"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "22") (Str2Reg "333"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "444"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "55")) (RegexStar (Str2Reg "666"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "77"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "88") (Str2Reg "9"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "a"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "b") (Str2Reg "c")) (RegexUnion (Str2Reg "d") (Str2Reg "ee"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "f") (Str2Reg "gg"))) (RegexUnion (RegexPlus (Str2Reg "hhh")) (RegexPlus (Str2Reg "ii")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexUnion (Str2Reg "00") (Str2Reg "1"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "2") (Str2Reg "333")) (RegexUnion (Str2Reg "444") (Str2Reg "5"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "666") (Str2Reg "777")) (RegexUnion (Str2Reg "88") (Str2Reg "99"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "aa") (Str2Reg "bb"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "cc") (Str2Reg "dd"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "ee") (Str2Reg "f"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "g") (Str2Reg "hh")) (RegexUnion (Str2Reg "iii") (Str2Reg "jj"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "k") (Str2Reg "l")) (RegexUnion (Str2Reg "m") (Str2Reg "nn"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "o") (Str2Reg "pp"))) (RegexStar (RegexPlus (Str2Reg "qq")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexUnion (Str2Reg "00") (Str2Reg "111"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "22")) (RegexStar (Str2Reg "3"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "4") (Str2Reg "55"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "666")) (RegexStar (Str2Reg "7"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "88"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "999")) (RegexStar (Str2Reg "aa"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "bbb") (Str2Reg "ccc"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "dd"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "eee")) (RegexStar (Str2Reg "ff"))) (RegexUnion (RegexStar (Str2Reg "ggg")) (RegexStar (Str2Reg "hh")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexPlus (Str2Reg "0")) (RegexPlus (Str2Reg "111"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "222"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "33") (Str2Reg "444")) (RegexUnion (Str2Reg "5") (Str2Reg "66"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "7")) (RegexStar (Str2Reg "8"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "999") (Str2Reg "aa"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "bbb"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "c"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "d"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "eee"))) (RegexPlus (RegexPlus (Str2Reg "fff")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexUnion (Str2Reg "0") (Str2Reg "11")) (RegexUnion (Str2Reg "2") (Str2Reg "3"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "444"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "55") (Str2Reg "666"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "77"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "88") (Str2Reg "99"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "a") (Str2Reg "b"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "ccc") (Str2Reg "dd"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "eee")) (RegexPlus (Str2Reg "f"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "g") (Str2Reg "hh"))) (RegexStar (RegexStar (Str2Reg "ii")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexPlus (RegexStar (Str2Reg "00"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "11") (Str2Reg "22"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "33"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "44") (Str2Reg "55"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "66"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "77"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "88")) (RegexPlus (Str2Reg "99"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "a"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "bbb")) (RegexStar (Str2Reg "cc"))) (RegexStar (RegexPlus (Str2Reg "dd")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexStar (Str2Reg "00"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "1"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "22"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "333"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "444"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "5") (Str2Reg "6"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "7"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "88")) (RegexStar (Str2Reg "99"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "a"))) (RegexUnion (RegexUnion (Str2Reg "bbb") (Str2Reg "c")) (RegexUnion (Str2Reg "ddd") (Str2Reg "e")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexPlus (RegexUnion (Str2Reg "00") (Str2Reg "1"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "2"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "333"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "444") (Str2Reg "55")) (RegexUnion (Str2Reg "666") (Str2Reg "777"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "888") (Str2Reg "9"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "aa")) (RegexStar (Str2Reg "b"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "ccc") (Str2Reg "dd")) (RegexUnion (Str2Reg "e") (Str2Reg "f"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "ggg"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "hh") (Str2Reg "ii"))) (RegexPlus (RegexPlus (Str2Reg "jjj")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexPlus (RegexPlus (Str2Reg "000"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "11")) (RegexPlus (Str2Reg "2"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "33") (Str2Reg "4"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "5"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "6"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "777")) (RegexPlus (Str2Reg "88"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "9") (Str2Reg "aaa"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "b") (Str2Reg "c"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "dd"))) (RegexPlus (RegexStar (Str2Reg "e")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexPlus (RegexUnion (Str2Reg "000") (Str2Reg "111"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "222"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "333") (Str2Reg "4"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "555"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "6"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "77") (Str2Reg "888"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "9"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "a") (Str2Reg "bbb"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "c"))) (RegexUnion (RegexStar (Str2Reg "ddd")) (RegexStar (Str2Reg "ee")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexUnion (Str2Reg "000") (Str2Reg "11"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "22") (Str2Reg "333"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "444")) (RegexStar (Str2Reg "555"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "666")) (RegexStar (Str2Reg "7"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "88")) (RegexPlus (Str2Reg "999"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "aa") (Str2Reg "bb")) (RegexUnion (Str2Reg "c") (Str2Reg "ddd"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "eee"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "fff"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "ggg"))) (RegexPlus (RegexPlus (Str2Reg "h")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexPlus (Str2Reg "0")) (RegexPlus (Str2Reg "11"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "22")) (RegexPlus (Str2Reg "3"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "444") (Str2Reg "5"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "666"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "777"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "888") (Str2Reg "99")) (RegexUnion (Str2Reg "aaa") (Str2Reg "bb"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "c") (Str2Reg "dd")) (RegexUnion (Str2Reg "eee") (Str2Reg "f"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "ggg"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "hhh") (Str2Reg "iii"))) (RegexStar (RegexStar (Str2Reg "jj")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexStar (Str2Reg "000")) (RegexStar (Str2Reg "111"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "222")) (RegexPlus (Str2Reg "33"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "4") (Str2Reg "555"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "666")) (RegexPlus (Str2Reg "777"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "8")) (RegexStar (Str2Reg "99"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "aaa"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "bb")) (RegexPlus (Str2Reg "ccc"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "dd"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "eee"))) (RegexPlus (RegexPlus (Str2Reg "ff")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexPlus (Str2Reg "000"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "11") (Str2Reg "2"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "333") (Str2Reg "4"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "55"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "666")) (RegexPlus (Str2Reg "77"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "88") (Str2Reg "9"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "a")) (RegexStar (Str2Reg "bbb"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "c") (Str2Reg "ddd")) (RegexUnion (Str2Reg "eee") (Str2Reg "fff"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "g"))) (RegexPlus (RegexStar (Str2Reg "hh")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexUnion (Str2Reg "0") (Str2Reg "111")) (RegexUnion (Str2Reg "22") (Str2Reg "3"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "4") (Str2Reg "55")) (RegexUnion (Str2Reg "6") (Str2Reg "777"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "888")) (RegexPlus (Str2Reg "999"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "a") (Str2Reg "b"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "c") (Str2Reg "dd"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "ee")) (RegexStar (Str2Reg "fff"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "ggg"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "h") (Str2Reg "iii"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "jj"))) (RegexPlus (RegexStar (Str2Reg "kkk")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexStar (Str2Reg "0")) (RegexStar (Str2Reg "11"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "2"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "33") (Str2Reg "4"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "555")) (RegexPlus (Str2Reg "666"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "7") (Str2Reg "888"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "999") (Str2Reg "aa")) (RegexUnion (Str2Reg "bbb") (Str2Reg "c"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "dd") (Str2Reg "ee")) (RegexUnion (Str2Reg "f") (Str2Reg "ggg"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "h") (Str2Reg "ii"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "jj"))) (RegexUnion (RegexStar (Str2Reg "kk")) (RegexStar (Str2Reg "ll")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexPlus (RegexStar (Str2Reg "0"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "11"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "222") (Str2Reg "33")) (RegexUnion (Str2Reg "444") (Str2Reg "55"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "666") (Str2Reg "7")) (RegexUnion (Str2Reg "888") (Str2Reg "999"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "aa") (Str2Reg "b"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "cc")) (RegexPlus (Str2Reg "d"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "ee")) (RegexStar (Str2Reg "f"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "ggg"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "h"))) (RegexStar (RegexUnion (Str2Reg "ii") (Str2Reg "jj")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexStar (Str2Reg "00")) (RegexStar (Str2Reg "11"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "22"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "3")) (RegexStar (Str2Reg "44"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "55") (Str2Reg "666"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "777") (Str2Reg "88"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "9"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "aa") (Str2Reg "bbb"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "cc"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "d"))) (RegexPlus (RegexUnion (Str2Reg "ee") (Str2Reg "f")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexPlus (Str2Reg "0")) (RegexPlus (Str2Reg "1"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "222"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "33")) (RegexStar (Str2Reg "4"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "555"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "6"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "777"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "8")) (RegexStar (Str2Reg "999"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "a")) (RegexPlus (Str2Reg "b"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "c"))) (RegexUnion (RegexPlus (Str2Reg "dd")) (RegexPlus (Str2Reg "ee")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexPlus (RegexStar (Str2Reg "000"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "11"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "22"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "33"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "44") (Str2Reg "5"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "666")) (RegexPlus (Str2Reg "7"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "88") (Str2Reg "999"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "aa"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "bb")) (RegexStar (Str2Reg "ccc"))) (RegexUnion (RegexStar (Str2Reg "ddd")) (RegexStar (Str2Reg "eee")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexStar (Str2Reg "00")) (RegexStar (Str2Reg "1"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "22") (Str2Reg "3"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "444")) (RegexStar (Str2Reg "5"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "6") (Str2Reg "77")) (RegexUnion (Str2Reg "8") (Str2Reg "999"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "a") (Str2Reg "b"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "ccc") (Str2Reg "ddd"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "e")) (RegexPlus (Str2Reg "ff"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "g")) (RegexStar (Str2Reg "hh"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "iii"))) (RegexUnion (RegexUnion (Str2Reg "j") (Str2Reg "k")) (RegexUnion (Str2Reg "l") (Str2Reg "m")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexPlus (Str2Reg "0")) (RegexPlus (Str2Reg "111"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "2"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "333"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "444") (Str2Reg "55"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "666"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "77") (Str2Reg "88")) (RegexUnion (Str2Reg "99") (Str2Reg "a"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "bb"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "ccc"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "ddd") (Str2Reg "eee"))) (RegexPlus (RegexUnion (Str2Reg "f") (Str2Reg "g")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexUnion (Str2Reg "000") (Str2Reg "1")) (RegexUnion (Str2Reg "22") (Str2Reg "33"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "4") (Str2Reg "55")) (RegexUnion (Str2Reg "66") (Str2Reg "777"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "8"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "999"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "aaa")) (RegexStar (Str2Reg "bbb"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "cc") (Str2Reg "d"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "e"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "f") (Str2Reg "gg"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "hhh"))) (RegexPlus (RegexStar (Str2Reg "i")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexPlus (Str2Reg "000"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "11")) (RegexPlus (Str2Reg "2"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "333") (Str2Reg "4"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "555")) (RegexStar (Str2Reg "66"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "777") (Str2Reg "888"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "9")) (RegexStar (Str2Reg "aa"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "b"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "ccc") (Str2Reg "dd"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "ee"))) (RegexUnion (RegexStar (Str2Reg "ff")) (RegexStar (Str2Reg "gg")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexUnion (Str2Reg "000") (Str2Reg "111"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "22"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "33"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "4") (Str2Reg "555"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "666")) (RegexPlus (Str2Reg "77"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "888") (Str2Reg "9"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "a"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "bbb") (Str2Reg "ccc"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "d") (Str2Reg "e"))) (RegexUnion (RegexStar (Str2Reg "fff")) (RegexStar (Str2Reg "g")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexPlus (Str2Reg "0")) (RegexPlus (Str2Reg "11"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "2")) (RegexPlus (Str2Reg "3"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "4") (Str2Reg "555")) (RegexUnion (Str2Reg "666") (Str2Reg "777"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "88") (Str2Reg "99"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "aaa") (Str2Reg "b"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "cc")) (RegexStar (Str2Reg "d"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "ee"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "fff") (Str2Reg "ggg"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "h") (Str2Reg "i"))) (RegexPlus (RegexStar (Str2Reg "jj")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexStar (Str2Reg "00"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "11"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "22")) (RegexStar (Str2Reg "333"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "44")) (RegexStar (Str2Reg "55"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "666") (Str2Reg "7"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "88"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "99") (Str2Reg "aa")) (RegexUnion (Str2Reg "bb") (Str2Reg "c"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "dd") (Str2Reg "e"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "f") (Str2Reg "ggg"))) (RegexPlus (RegexStar (Str2Reg "hhh")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexStar (Str2Reg "0")) (RegexStar (Str2Reg "1"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "222"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "3"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "44") (Str2Reg "555"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "66") (Str2Reg "77")) (RegexUnion (Str2Reg "88") (Str2Reg "99"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "aa"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "bb"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "c")) (RegexStar (Str2Reg "ddd"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "eee")) (RegexStar (Str2Reg "ff"))) (RegexStar (RegexPlus (Str2Reg "gg")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexStar (Str2Reg "0"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "111") (Str2Reg "2")) (RegexUnion (Str2Reg "33") (Str2Reg "4"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "5")) (RegexStar (Str2Reg "66"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "77") (Str2Reg "88"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "99")) (RegexPlus (Str2Reg "aaa"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "b"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "c")) (RegexPlus (Str2Reg "dd"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "e")) (RegexStar (Str2Reg "f"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "ggg") (Str2Reg "hhh")) (RegexUnion (Str2Reg "iii") (Str2Reg "jjj"))) (RegexPlus (RegexStar (Str2Reg "k")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexUnion (Str2Reg "000") (Str2Reg "11"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "2")) (RegexStar (Str2Reg "3"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "444")) (RegexPlus (Str2Reg "55"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "666")) (RegexPlus (Str2Reg "7"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "88")) (RegexStar (Str2Reg "99"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "aa")) (RegexStar (Str2Reg "bbb"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "cc")) (RegexStar (Str2Reg "ddd"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "ee"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "fff"))) (RegexUnion (RegexPlus (Str2Reg "ggg")) (RegexPlus (Str2Reg "h")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexPlus (Str2Reg "0")) (RegexPlus (Str2Reg "111"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "22") (Str2Reg "333")) (RegexUnion (Str2Reg "44") (Str2Reg "555"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "66") (Str2Reg "7"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "88") (Str2Reg "9"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "aaa"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "b"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "cc") (Str2Reg "dd"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "eee"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "ff") (Str2Reg "gg"))) (RegexPlus (RegexStar (Str2Reg "hh")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexUnion (Str2Reg "00") (Str2Reg "111")) (RegexUnion (Str2Reg "2") (Str2Reg "3"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "444")) (RegexStar (Str2Reg "5"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "6"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "7"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "8")) (RegexPlus (Str2Reg "9"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "aaa") (Str2Reg "b"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "cc") (Str2Reg "d"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "e") (Str2Reg "f")) (RegexUnion (Str2Reg "ggg") (Str2Reg "h"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "i"))) (RegexPlus (RegexPlus (Str2Reg "jjj")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexUnion (Str2Reg "0") (Str2Reg "111")) (RegexUnion (Str2Reg "2") (Str2Reg "3"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "444")) (RegexPlus (Str2Reg "555"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "6")) (RegexStar (Str2Reg "7"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "8"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "999"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "aa"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "bbb") (Str2Reg "cc")) (RegexUnion (Str2Reg "ddd") (Str2Reg "eee"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "ff")) (RegexPlus (Str2Reg "gg"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "hh"))) (RegexPlus (RegexStar (Str2Reg "i")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexPlus (Str2Reg "000"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "1")) (RegexPlus (Str2Reg "2"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "333") (Str2Reg "44")) (RegexUnion (Str2Reg "555") (Str2Reg "6"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "777"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "888"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "999") (Str2Reg "aaa"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "bbb"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "cc") (Str2Reg "d"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "eee"))) (RegexUnion (RegexPlus (Str2Reg "f")) (RegexPlus (Str2Reg "ggg")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexPlus (Str2Reg "000"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "111"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "222")) (RegexStar (Str2Reg "33"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "444")) (RegexStar (Str2Reg "555"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "666") (Str2Reg "777"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "8") (Str2Reg "99"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "aa")) (RegexPlus (Str2Reg "bb"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "cc"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "dd") (Str2Reg "eee")) (RegexUnion (Str2Reg "f") (Str2Reg "ggg"))) (RegexPlus (RegexStar (Str2Reg "h")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexPlus (Str2Reg "000")) (RegexPlus (Str2Reg "11"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "222") (Str2Reg "333")) (RegexUnion (Str2Reg "44") (Str2Reg "5"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "6") (Str2Reg "7")) (RegexUnion (Str2Reg "8") (Str2Reg "999"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "aaa") (Str2Reg "bb"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "cc") (Str2Reg "ddd"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "e")) (RegexPlus (Str2Reg "ff"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "ggg"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "h"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "i"))) (RegexPlus (RegexPlus (Str2Reg "jjj")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexUnion (Str2Reg "0") (Str2Reg "1"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "2"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "333") (Str2Reg "444"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "555") (Str2Reg "6"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "777"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "8") (Str2Reg "9"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "aa"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "bb"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "c") (Str2Reg "d"))) (RegexPlus (RegexPlus (Str2Reg "e")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexPlus (Str2Reg "00")) (RegexPlus (Str2Reg "1"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "22") (Str2Reg "333")) (RegexUnion (Str2Reg "444") (Str2Reg "5"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "66") (Str2Reg "777"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "8") (Str2Reg "999"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "aaa"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "bbb") (Str2Reg "c"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "dd")) (RegexStar (Str2Reg "ee"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "fff"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "ggg"))) (RegexStar (RegexPlus (Str2Reg "hhh")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexPlus (RegexUnion (Str2Reg "000") (Str2Reg "1"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "2")) (RegexPlus (Str2Reg "3"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "44"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "555")) (RegexPlus (Str2Reg "66"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "7")) (RegexPlus (Str2Reg "88"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "99")) (RegexStar (Str2Reg "aa"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "bb") (Str2Reg "c")) (RegexUnion (Str2Reg "ddd") (Str2Reg "ee"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "f")) (RegexStar (Str2Reg "g"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "hhh"))) (RegexPlus (RegexPlus (Str2Reg "i")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexPlus (Str2Reg "000"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "1"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "22"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "333") (Str2Reg "4"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "555"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "66")) (RegexPlus (Str2Reg "777"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "8")) (RegexPlus (Str2Reg "999"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "aa"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "bbb")) (RegexStar (Str2Reg "cc"))) (RegexPlus (RegexPlus (Str2Reg "dd")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexStar (Str2Reg "00")) (RegexStar (Str2Reg "111"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "22") (Str2Reg "3"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "444") (Str2Reg "5")) (RegexUnion (Str2Reg "666") (Str2Reg "7"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "8"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "9"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "a")) (RegexPlus (Str2Reg "bb"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "ccc"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "ddd")) (RegexStar (Str2Reg "eee"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "f") (Str2Reg "ggg"))) (RegexUnion (RegexUnion (Str2Reg "hh") (Str2Reg "i")) (RegexUnion (Str2Reg "jjj") (Str2Reg "kkk")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexPlus (Str2Reg "0")) (RegexPlus (Str2Reg "1"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "2"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "333")) (RegexStar (Str2Reg "44"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "5") (Str2Reg "6"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "77") (Str2Reg "88")) (RegexUnion (Str2Reg "999") (Str2Reg "aa"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "bb"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "ccc"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "d"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "ee"))) (RegexStar (RegexUnion (Str2Reg "ff") (Str2Reg "g")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexStar (Str2Reg "000"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "111"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "222") (Str2Reg "3"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "4"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "555"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "666"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "7")) (RegexStar (Str2Reg "888"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "999") (Str2Reg "aaa")) (RegexUnion (Str2Reg "bbb") (Str2Reg "c"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "ddd"))) (RegexUnion (RegexPlus (Str2Reg "ee")) (RegexPlus (Str2Reg "f")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexPlus (RegexPlus (Str2Reg "000"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "1")) (RegexPlus (Str2Reg "222"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "33") (Str2Reg "44")) (RegexUnion (Str2Reg "5") (Str2Reg "6"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "7"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "888"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "9") (Str2Reg "aa")) (RegexUnion (Str2Reg "bbb") (Str2Reg "cc"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "dd") (Str2Reg "eee"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "fff") (Str2Reg "g")) (RegexUnion (Str2Reg "hh") (Str2Reg "iii"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "j"))) (RegexPlus (RegexStar (Str2Reg "k")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexPlus (RegexStar (Str2Reg "00"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "1"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "222") (Str2Reg "33")) (RegexUnion (Str2Reg "4") (Str2Reg "555"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "6") (Str2Reg "7")) (RegexUnion (Str2Reg "88") (Str2Reg "999"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "aaa") (Str2Reg "bbb"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "ccc"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "dd")) (RegexStar (Str2Reg "ee"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "fff"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "gg"))) (RegexUnion (RegexStar (Str2Reg "hh")) (RegexStar (Str2Reg "ii")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexStar (Str2Reg "00"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "11") (Str2Reg "22")) (RegexUnion (Str2Reg "3") (Str2Reg "4"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "5") (Str2Reg "666")) (RegexUnion (Str2Reg "7") (Str2Reg "8"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "99"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "aaa"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "bbb") (Str2Reg "ccc")) (RegexUnion (Str2Reg "dd") (Str2Reg "ee"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "fff") (Str2Reg "g")) (RegexUnion (Str2Reg "h") (Str2Reg "iii"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "jjj") (Str2Reg "k"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "ll") (Str2Reg "m"))) (RegexStar (RegexPlus (Str2Reg "nnn")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexStar (Str2Reg "0"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "11"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "2") (Str2Reg "3"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "4"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "55")) (RegexStar (Str2Reg "66"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "777") (Str2Reg "8")) (RegexUnion (Str2Reg "99") (Str2Reg "aaa"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "bb"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "cc"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "dd"))) (RegexPlus (RegexUnion (Str2Reg "ee") (Str2Reg "fff")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexPlus (RegexPlus (Str2Reg "000"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "111") (Str2Reg "22"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "333"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "44"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "5"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "666"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "777"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "88"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "999") (Str2Reg "a"))) (RegexUnion (RegexUnion (Str2Reg "bb") (Str2Reg "ccc")) (RegexUnion (Str2Reg "d") (Str2Reg "ee")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexUnion (RegexStar (Str2Reg "0")) (RegexStar (Str2Reg "11"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "222")) (RegexStar (Str2Reg "33"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "4"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "55") (Str2Reg "666")) (RegexUnion (Str2Reg "77") (Str2Reg "888"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "9") (Str2Reg "aa"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "bbb") (Str2Reg "cc")) (RegexUnion (Str2Reg "ddd") (Str2Reg "ee"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "fff") (Str2Reg "ggg"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "hhh")) (RegexStar (Str2Reg "i"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "jj"))) (RegexUnion (RegexPlus (Str2Reg "kk")) (RegexPlus (Str2Reg "l")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexPlus (RegexUnion (Str2Reg "00") (Str2Reg "111"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "2") (Str2Reg "33"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "44"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "555") (Str2Reg "666")) (RegexUnion (Str2Reg "777") (Str2Reg "8"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "999"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "aaa") (Str2Reg "b")) (RegexUnion (Str2Reg "ccc") (Str2Reg "d"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "e") (Str2Reg "fff")) (RegexUnion (Str2Reg "ggg") (Str2Reg "h"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "iii") (Str2Reg "jjj"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "kkk"))) (RegexStar (RegexStar (Str2Reg "lll")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexPlus (Str2Reg "0"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "1")) (RegexStar (Str2Reg "222"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "33") (Str2Reg "4")) (RegexUnion (Str2Reg "55") (Str2Reg "6"))) (RegexConcat (RegexUnion (RegexStar (Str2Reg "7")) (RegexStar (Str2Reg "88"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "9") (Str2Reg "aaa"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "bb")) (RegexPlus (Str2Reg "cc"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "d") (Str2Reg "e"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "fff") (Str2Reg "ggg")) (RegexUnion (Str2Reg "hh") (Str2Reg "i"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "j"))) (RegexUnion (RegexStar (Str2Reg "kkk")) (RegexStar (Str2Reg "ll")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexUnion (Str2Reg "0") (Str2Reg "1"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "22"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "3") (Str2Reg "44")) (RegexUnion (Str2Reg "555") (Str2Reg "66"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "77") (Str2Reg "88")) (RegexUnion (Str2Reg "9") (Str2Reg "aaa"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "b"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "cc") (Str2Reg "dd"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "ee"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "ff"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "g"))) (RegexStar (RegexPlus (Str2Reg "h")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexPlus (RegexUnion (Str2Reg "000") (Str2Reg "1"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "222") (Str2Reg "3")) (RegexUnion (Str2Reg "4") (Str2Reg "5"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "6"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "777")) (RegexPlus (Str2Reg "8"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "99"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "aa"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "bbb"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "cc")) (RegexPlus (Str2Reg "ddd"))) (RegexConcat (RegexStar (RegexUnion (Str2Reg "eee") (Str2Reg "ff"))) (RegexUnion (RegexStar (Str2Reg "gg")) (RegexStar (Str2Reg "h")))))))))))))) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexStar (Str2Reg "00"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "111")) (RegexPlus (Str2Reg "22"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "333")) (RegexPlus (Str2Reg "444"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "5"))) (RegexConcat (RegexPlus (RegexUnion (Str2Reg "6") (Str2Reg "77"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "888"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "999"))) (RegexConcat (RegexPlus (RegexPlus (Str2Reg "a"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "bbb")) (RegexPlus (Str2Reg "ccc"))) (RegexUnion (RegexStar (Str2Reg "d")) (RegexStar (Str2Reg "eee")))))))))))))) (check-sat)