Collections of smt problems
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 

208 lines
37 KiB

; Romeinse cijfers
(declare-datatypes () ((Rom I V X L C D M)))
; Super lomp en gegenereerd
(define-fun ran ((x Int)) Bool
(or (= x 18) (= x 23) (= x 27) (= x 32) (= x 34) (= x 36) (= x 39) (= x 43) (= x 47) (= x 58) (= x 63) (= x 67) (= x 72) (= x 74) (= x 76) (= x 79) (= x 81) (= x 85) (= x 93) (= x 97) (= x 108) (= x 113) (= x 117) (= x 122) (= x 124) (= x 126) (= x 129) (= x 131) (= x 135) (= x 142) (= x 144) (= x 146) (= x 149) (= x 153) (= x 157) (= x 162) (= x 164) (= x 166) (= x 169) (= x 171) (= x 175) (= x 180) (= x 192) (= x 194) (= x 196) (= x 199) (= x 203) (= x 207) (= x 212) (= x 214) (= x 216) (= x 219) (= x 221) (= x 225) (= x 230) (= x 241) (= x 245) (= x 252) (= x 254) (= x 256) (= x 259) (= x 261) (= x 265) (= x 270) (= x 291) (= x 295) (= x 302) (= x 304) (= x 306) (= x 309) (= x 311) (= x 315) (= x 320) (= x 340) (= x 351) (= x 355) (= x 360) (= x 390) (= x 403) (= x 407) (= x 412) (= x 414) (= x 416) (= x 419) (= x 421) (= x 425) (= x 430) (= x 441) (= x 445) (= x 452) (= x 454) (= x 456) (= x 459) (= x 461) (= x 465) (= x 470) (= x 491) (= x 495) (= x 508) (= x 513) (= x 517) (= x 522) (= x 524) (= x 526) (= x 529) (= x 531) (= x 535) (= x 542) (= x 544) (= x 546) (= x 549) (= x 553) (= x 557) (= x 562) (= x 564) (= x 566) (= x 569) (= x 571) (= x 575) (= x 580) (= x 592) (= x 594) (= x 596) (= x 599) (= x 603) (= x 607) (= x 612) (= x 614) (= x 616) (= x 619) (= x 621) (= x 625) (= x 630) (= x 641) (= x 645) (= x 652) (= x 654) (= x 656) (= x 659) (= x 661) (= x 665) (= x 670) (= x 691) (= x 695) (= x 702) (= x 704) (= x 706) (= x 709) (= x 711) (= x 715) (= x 720) (= x 740) (= x 751) (= x 755) (= x 760) (= x 790) (= x 801) (= x 805) (= x 810) (= x 850) (= x 903) (= x 907) (= x 912) (= x 914) (= x 916) (= x 919) (= x 921) (= x 925) (= x 930) (= x 941) (= x 945) (= x 952) (= x 954) (= x 956) (= x 959) (= x 961) (= x 965) (= x 970) (= x 991) (= x 995) (= x 1008) (= x 1013) (= x 1017) (= x 1022) (= x 1024) (= x 1026) (= x 1029) (= x 1031) (= x 1035) (= x 1042) (= x 1044) (= x 1046) (= x 1049) (= x 1053) (= x 1057) (= x 1062) (= x 1064) (= x 1066) (= x 1069) (= x 1071) (= x 1075) (= x 1080) (= x 1092) (= x 1094) (= x 1096) (= x 1099) (= x 1103) (= x 1107) (= x 1112) (= x 1114) (= x 1116) (= x 1119) (= x 1121) (= x 1125) (= x 1130) (= x 1141) (= x 1145) (= x 1152) (= x 1154) (= x 1156) (= x 1159) (= x 1161) (= x 1165) (= x 1170) (= x 1191) (= x 1195) (= x 1202) (= x 1204) (= x 1206) (= x 1209) (= x 1211) (= x 1215) (= x 1220) (= x 1240) (= x 1251) (= x 1255) (= x 1260) (= x 1290) (= x 1301) (= x 1305) (= x 1310) (= x 1350) (= x 1402) (= x 1404) (= x 1406) (= x 1409) (= x 1411) (= x 1415) (= x 1420) (= x 1440) (= x 1451) (= x 1455) (= x 1460) (= x 1490) (= x 1503) (= x 1507) (= x 1512) (= x 1514) (= x 1516) (= x 1519) (= x 1521) (= x 1525) (= x 1530) (= x 1541) (= x 1545) (= x 1552) (= x 1554) (= x 1556) (= x 1559) (= x 1561) (= x 1565) (= x 1570) (= x 1591) (= x 1595) (= x 1602) (= x 1604) (= x 1606) (= x 1609) (= x 1611) (= x 1615) (= x 1620) (= x 1640) (= x 1651) (= x 1655) (= x 1660) (= x 1690) (= x 1701) (= x 1705) (= x 1710) (= x 1750) (= x 1800) (= x 1902) (= x 1904) (= x 1906) (= x 1909) (= x 1911) (= x 1915) (= x 1920) (= x 1940) (= x 1951) (= x 1955) (= x 1960) (= x 1990) (= x 2003) (= x 2007) (= x 2012) (= x 2014) (= x 2016) (= x 2019) (= x 2021) (= x 2025) (= x 2030) (= x 2041) (= x 2045) (= x 2052) (= x 2054) (= x 2056) (= x 2059) (= x 2061) (= x 2065) (= x 2070) (= x 2091) (= x 2095) (= x 2102) (= x 2104) (= x 2106) (= x 2109) (= x 2111) (= x 2115) (= x 2120) (= x 2140) (= x 2151) (= x 2155) (= x 2160) (= x 2190) (= x 2201) (= x 2205) (= x 2210) (= x 2250) (= x 2300) (= x 2401) (= x 2405) (= x 2410) (= x 2450) (= x 2502) (= x 2504) (= x 2506) (= x 2509) (= x 2511) (= x 2515) (= x 2520) (= x 2540) (= x 2551) (= x 2555) (= x 2560) (= x 2590) (= x 2601) (= x 2605) (= x 2610) (= x 2650) (= x 2700) (= x 2901) (= x 2905) (= x 2910) (= x 2950) (= x 3002) (= x 3004) (= x 3006) (= x 3009) (= x 3011) (= x 3015) (= x 3020) (= x 3040) (= x 3051) (= x 3055) (= x 3060) (= x 3090) (= x 3101) (= x 3105) (= x 3110) (= x 3150) (= x 3200) (= x 3400) (= x 3501) (= x 3505) (= x 3510) (= x 3550) (= x 3600) (= x 3900))
)
; Priem
(define-fun cran ((x Int)) Bool
(or (= x 23) (= x 43) (= x 47) (= x 67) (= x 79) (= x 97) (= x 113) (= x 131) (= x 149) (= x 157) (= x 199) (= x 241) (= x 311) (= x 419) (= x 421) (= x 461) (= x 491) (= x 557) (= x 569) (= x 571) (= x 599) (= x 607) (= x 619) (= x 641) (= x 659) (= x 661) (= x 691) (= x 709) (= x 751) (= x 907) (= x 919) (= x 941) (= x 991) (= x 1013) (= x 1031) (= x 1049) (= x 1069) (= x 1103) (= x 1301) (= x 1409) (= x 1451) (= x 1559) (= x 1609) (= x 1951) (= x 2003) (= x 2111) (= x 2551) (= x 3011))
)
(define-fun rom1 ((x Int) (y Rom)) Bool
(and (implies (and (>= x 18) (<= x 47)) (= y X)) (implies (and (>= x 58) (<= x 85)) (= y L)) (implies (and (>= x 93) (<= x 97)) (= y X)) (implies (and (>= x 108) (<= x 495)) (= y C)) (implies (and (>= x 508) (<= x 850)) (= y D)) (implies (and (>= x 903) (<= x 995)) (= y C)) (implies (and (>= x 1008) (<= x 3900)) (= y M)))
)
(define-fun rom2 ((x Int) (y Rom)) Bool
(and (implies (and (>= x 18) (<= x 18)) (= y V)) (implies (and (>= x 23) (<= x 39)) (= y X)) (implies (and (>= x 43) (<= x 47)) (= y L)) (implies (and (>= x 58) (<= x 58)) (= y V)) (implies (and (>= x 63) (<= x 85)) (= y X)) (implies (and (>= x 93) (<= x 97)) (= y C)) (implies (and (>= x 108) (<= x 108)) (= y V)) (implies (and (>= x 113) (<= x 149)) (= y X)) (implies (and (>= x 153) (<= x 180)) (= y L)) (implies (and (>= x 192) (<= x 199)) (= y X)) (implies (and (>= x 203) (<= x 390)) (= y C)) (implies (and (>= x 403) (<= x 495)) (= y D)) (implies (and (>= x 508) (<= x 508)) (= y V)) (implies (and (>= x 513) (<= x 549)) (= y X)) (implies (and (>= x 553) (<= x 580)) (= y L)) (implies (and (>= x 592) (<= x 599)) (= y X)) (implies (and (>= x 603) (<= x 850)) (= y C)) (implies (and (>= x 903) (<= x 995)) (= y M)) (implies (and (>= x 1008) (<= x 1008)) (= y V)) (implies (and (>= x 1013) (<= x 1049)) (= y X)) (implies (and (>= x 1053) (<= x 1080)) (= y L)) (implies (and (>= x 1092) (<= x 1099)) (= y X)) (implies (and (>= x 1103) (<= x 1490)) (= y C)) (implies (and (>= x 1503) (<= x 1800)) (= y D)) (implies (and (>= x 1902) (<= x 1990)) (= y C)) (implies (and (>= x 2003) (<= x 3900)) (= y M)))
)
(define-fun rom3 ((x Int) (y Rom)) Bool
(and (implies (and (>= x 18) (<= x 23)) (= y I)) (implies (and (>= x 27) (<= x 27)) (= y V)) (implies (and (>= x 32) (<= x 39)) (= y X)) (implies (and (>= x 43) (<= x 43)) (= y I)) (implies (and (>= x 47) (<= x 47)) (= y V)) (implies (and (>= x 58) (<= x 63)) (= y I)) (implies (and (>= x 67) (<= x 67)) (= y V)) (implies (and (>= x 72) (<= x 85)) (= y X)) (implies (and (>= x 93) (<= x 93)) (= y I)) (implies (and (>= x 97) (<= x 97)) (= y V)) (implies (and (>= x 108) (<= x 113)) (= y I)) (implies (and (>= x 117) (<= x 117)) (= y V)) (implies (and (>= x 122) (<= x 135)) (= y X)) (implies (and (>= x 142) (<= x 149)) (= y L)) (implies (and (>= x 153) (<= x 153)) (= y I)) (implies (and (>= x 157) (<= x 157)) (= y V)) (implies (and (>= x 162) (<= x 180)) (= y X)) (implies (and (>= x 192) (<= x 199)) (= y C)) (implies (and (>= x 203) (<= x 203)) (= y I)) (implies (and (>= x 207) (<= x 207)) (= y V)) (implies (and (>= x 212) (<= x 245)) (= y X)) (implies (and (>= x 252) (<= x 270)) (= y L)) (implies (and (>= x 291) (<= x 295)) (= y X)) (implies (and (>= x 302) (<= x 390)) (= y C)) (implies (and (>= x 403) (<= x 403)) (= y I)) (implies (and (>= x 407) (<= x 407)) (= y V)) (implies (and (>= x 412) (<= x 445)) (= y X)) (implies (and (>= x 452) (<= x 470)) (= y L)) (implies (and (>= x 491) (<= x 495)) (= y X)) (implies (and (>= x 508) (<= x 513)) (= y I)) (implies (and (>= x 517) (<= x 517)) (= y V)) (implies (and (>= x 522) (<= x 535)) (= y X)) (implies (and (>= x 542) (<= x 549)) (= y L)) (implies (and (>= x 553) (<= x 553)) (= y I)) (implies (and (>= x 557) (<= x 557)) (= y V)) (implies (and (>= x 562) (<= x 580)) (= y X)) (implies (and (>= x 592) (<= x 599)) (= y C)) (implies (and (>= x 603) (<= x 603)) (= y I)) (implies (and (>= x 607) (<= x 607)) (= y V)) (implies (and (>= x 612) (<= x 645)) (= y X)) (implies (and (>= x 652) (<= x 670)) (= y L)) (implies (and (>= x 691) (<= x 695)) (= y X)) (implies (and (>= x 702) (<= x 850)) (= y C)) (implies (and (>= x 903) (<= x 903)) (= y I)) (implies (and (>= x 907) (<= x 907)) (= y V)) (implies (and (>= x 912) (<= x 945)) (= y X)) (implies (and (>= x 952) (<= x 970)) (= y L)) (implies (and (>= x 991) (<= x 995)) (= y X)) (implies (and (>= x 1008) (<= x 1013)) (= y I)) (implies (and (>= x 1017) (<= x 1017)) (= y V)) (implies (and (>= x 1022) (<= x 1035)) (= y X)) (implies (and (>= x 1042) (<= x 1049)) (= y L)) (implies (and (>= x 1053) (<= x 1053)) (= y I)) (implies (and (>= x 1057) (<= x 1057)) (= y V)) (implies (and (>= x 1062) (<= x 1080)) (= y X)) (implies (and (>= x 1092) (<= x 1099)) (= y C)) (implies (and (>= x 1103) (<= x 1103)) (= y I)) (implies (and (>= x 1107) (<= x 1107)) (= y V)) (implies (and (>= x 1112) (<= x 1145)) (= y X)) (implies (and (>= x 1152) (<= x 1170)) (= y L)) (implies (and (>= x 1191) (<= x 1195)) (= y X)) (implies (and (>= x 1202) (<= x 1350)) (= y C)) (implies (and (>= x 1402) (<= x 1490)) (= y D)) (implies (and (>= x 1503) (<= x 1503)) (= y I)) (implies (and (>= x 1507) (<= x 1507)) (= y V)) (implies (and (>= x 1512) (<= x 1545)) (= y X)) (implies (and (>= x 1552) (<= x 1570)) (= y L)) (implies (and (>= x 1591) (<= x 1595)) (= y X)) (implies (and (>= x 1602) (<= x 1800)) (= y C)) (implies (and (>= x 1902) (<= x 1990)) (= y M)) (implies (and (>= x 2003) (<= x 2003)) (= y I)) (implies (and (>= x 2007) (<= x 2007)) (= y V)) (implies (and (>= x 2012) (<= x 2045)) (= y X)) (implies (and (>= x 2052) (<= x 2070)) (= y L)) (implies (and (>= x 2091) (<= x 2095)) (= y X)) (implies (and (>= x 2102) (<= x 2450)) (= y C)) (implies (and (>= x 2502) (<= x 2700)) (= y D)) (implies (and (>= x 2901) (<= x 2950)) (= y C)) (implies (and (>= x 3002) (<= x 3900)) (= y M)))
)
(define-fun rom4 ((x Int) (y Rom)) Bool
(and (implies (and (>= x 18) (<= x 34)) (= y I)) (implies (and (>= x 36) (<= x 36)) (= y V)) (implies (and (>= x 39) (<= x 74)) (= y I)) (implies (and (>= x 76) (<= x 76)) (= y V)) (implies (and (>= x 79) (<= x 79)) (= y I)) (implies (and (>= x 81) (<= x 85)) (= y X)) (implies (and (>= x 93) (<= x 124)) (= y I)) (implies (and (>= x 126) (<= x 126)) (= y V)) (implies (and (>= x 129) (<= x 129)) (= y I)) (implies (and (>= x 131) (<= x 135)) (= y X)) (implies (and (>= x 142) (<= x 144)) (= y I)) (implies (and (>= x 146) (<= x 146)) (= y V)) (implies (and (>= x 149) (<= x 164)) (= y I)) (implies (and (>= x 166) (<= x 166)) (= y V)) (implies (and (>= x 169) (<= x 169)) (= y I)) (implies (and (>= x 171) (<= x 180)) (= y X)) (implies (and (>= x 192) (<= x 194)) (= y I)) (implies (and (>= x 196) (<= x 196)) (= y V)) (implies (and (>= x 199) (<= x 214)) (= y I)) (implies (and (>= x 216) (<= x 216)) (= y V)) (implies (and (>= x 219) (<= x 219)) (= y I)) (implies (and (>= x 221) (<= x 230)) (= y X)) (implies (and (>= x 241) (<= x 245)) (= y L)) (implies (and (>= x 252) (<= x 254)) (= y I)) (implies (and (>= x 256) (<= x 256)) (= y V)) (implies (and (>= x 259) (<= x 259)) (= y I)) (implies (and (>= x 261) (<= x 270)) (= y X)) (implies (and (>= x 291) (<= x 295)) (= y C)) (implies (and (>= x 302) (<= x 304)) (= y I)) (implies (and (>= x 306) (<= x 306)) (= y V)) (implies (and (>= x 309) (<= x 309)) (= y I)) (implies (and (>= x 311) (<= x 340)) (= y X)) (implies (and (>= x 351) (<= x 360)) (= y L)) (implies (and (>= x 390) (<= x 390)) (= y X)) (implies (and (>= x 403) (<= x 414)) (= y I)) (implies (and (>= x 416) (<= x 416)) (= y V)) (implies (and (>= x 419) (<= x 419)) (= y I)) (implies (and (>= x 421) (<= x 430)) (= y X)) (implies (and (>= x 441) (<= x 445)) (= y L)) (implies (and (>= x 452) (<= x 454)) (= y I)) (implies (and (>= x 456) (<= x 456)) (= y V)) (implies (and (>= x 459) (<= x 459)) (= y I)) (implies (and (>= x 461) (<= x 470)) (= y X)) (implies (and (>= x 491) (<= x 495)) (= y C)) (implies (and (>= x 508) (<= x 524)) (= y I)) (implies (and (>= x 526) (<= x 526)) (= y V)) (implies (and (>= x 529) (<= x 529)) (= y I)) (implies (and (>= x 531) (<= x 535)) (= y X)) (implies (and (>= x 542) (<= x 544)) (= y I)) (implies (and (>= x 546) (<= x 546)) (= y V)) (implies (and (>= x 549) (<= x 564)) (= y I)) (implies (and (>= x 566) (<= x 566)) (= y V)) (implies (and (>= x 569) (<= x 569)) (= y I)) (implies (and (>= x 571) (<= x 580)) (= y X)) (implies (and (>= x 592) (<= x 594)) (= y I)) (implies (and (>= x 596) (<= x 596)) (= y V)) (implies (and (>= x 599) (<= x 614)) (= y I)) (implies (and (>= x 616) (<= x 616)) (= y V)) (implies (and (>= x 619) (<= x 619)) (= y I)) (implies (and (>= x 621) (<= x 630)) (= y X)) (implies (and (>= x 641) (<= x 645)) (= y L)) (implies (and (>= x 652) (<= x 654)) (= y I)) (implies (and (>= x 656) (<= x 656)) (= y V)) (implies (and (>= x 659) (<= x 659)) (= y I)) (implies (and (>= x 661) (<= x 670)) (= y X)) (implies (and (>= x 691) (<= x 695)) (= y C)) (implies (and (>= x 702) (<= x 704)) (= y I)) (implies (and (>= x 706) (<= x 706)) (= y V)) (implies (and (>= x 709) (<= x 709)) (= y I)) (implies (and (>= x 711) (<= x 740)) (= y X)) (implies (and (>= x 751) (<= x 760)) (= y L)) (implies (and (>= x 790) (<= x 790)) (= y X)) (implies (and (>= x 801) (<= x 850)) (= y C)) (implies (and (>= x 903) (<= x 914)) (= y I)) (implies (and (>= x 916) (<= x 916)) (= y V)) (implies (and (>= x 919) (<= x 919)) (= y I)) (implies (and (>= x 921) (<= x 930)) (= y X)) (implies (and (>= x 941) (<= x 945)) (= y L)) (implies (and (>= x 952) (<= x 954)) (= y I)) (implies (and (>= x 956) (<= x 956)) (= y V)) (implies (and (>= x 959) (<= x 959)) (= y I)) (implies (and (>= x 961) (<= x 970)) (= y X)) (implies (and (>= x 991) (<= x 995)) (= y C)) (implies (and (>= x 1008) (<= x 1024)) (= y I)) (implies (and (>= x 1026) (<= x 1026)) (= y V)) (implies (and (>= x 1029) (<= x 1029)) (= y I)) (implies (and (>= x 1031) (<= x 1035)) (= y X)) (implies (and (>= x 1042) (<= x 1044)) (= y I)) (implies (and (>= x 1046) (<= x 1046)) (= y V)) (implies (and (>= x 1049) (<= x 1064)) (= y I)) (implies (and (>= x 1066) (<= x 1066)) (= y V)) (implies (and (>= x 1069) (<= x 1069)) (= y I)) (implies (and (>= x 1071) (<= x 1080)) (= y X)) (implies (and (>= x 1092) (<= x 1094)) (= y I)) (implies (and (>= x 1096) (<= x 1096)) (= y V)) (implies (and (>= x 1099) (<= x 1114)) (= y I)) (implies (and (>= x 1116) (<= x 1116)) (= y V)) (implies (and (>= x 1119) (<= x 1119)) (= y I)) (implies (and (>= x 1121) (<= x 1130)) (= y X)) (implies (and (>= x 1141) (<= x 1145)) (= y L)) (implies (and (>= x 1152) (<= x 1154)) (= y I)) (implies (and (>= x 1156) (<= x 1156)) (= y V)) (implies (and (>= x 1159) (<= x 1159)) (= y I)) (implies (and (>= x 1161) (<= x 1170)) (= y X)) (implies (and (>= x 1191) (<= x 1195)) (= y C)) (implies (and (>= x 1202) (<= x 1204)) (= y I)) (implies (and (>= x 1206) (<= x 1206)) (= y V)) (implies (and (>= x 1209) (<= x 1209)) (= y I)) (implies (and (>= x 1211) (<= x 1240)) (= y X)) (implies (and (>= x 1251) (<= x 1260)) (= y L)) (implies (and (>= x 1290) (<= x 1290)) (= y X)) (implies (and (>= x 1301) (<= x 1350)) (= y C)) (implies (and (>= x 1402) (<= x 1404)) (= y I)) (implies (and (>= x 1406) (<= x 1406)) (= y V)) (implies (and (>= x 1409) (<= x 1409)) (= y I)) (implies (and (>= x 1411) (<= x 1440)) (= y X)) (implies (and (>= x 1451) (<= x 1460)) (= y L)) (implies (and (>= x 1490) (<= x 1490)) (= y X)) (implies (and (>= x 1503) (<= x 1514)) (= y I)) (implies (and (>= x 1516) (<= x 1516)) (= y V)) (implies (and (>= x 1519) (<= x 1519)) (= y I)) (implies (and (>= x 1521) (<= x 1530)) (= y X)) (implies (and (>= x 1541) (<= x 1545)) (= y L)) (implies (and (>= x 1552) (<= x 1554)) (= y I)) (implies (and (>= x 1556) (<= x 1556)) (= y V)) (implies (and (>= x 1559) (<= x 1559)) (= y I)) (implies (and (>= x 1561) (<= x 1570)) (= y X)) (implies (and (>= x 1591) (<= x 1595)) (= y C)) (implies (and (>= x 1602) (<= x 1604)) (= y I)) (implies (and (>= x 1606) (<= x 1606)) (= y V)) (implies (and (>= x 1609) (<= x 1609)) (= y I)) (implies (and (>= x 1611) (<= x 1640)) (= y X)) (implies (and (>= x 1651) (<= x 1660)) (= y L)) (implies (and (>= x 1690) (<= x 1690)) (= y X)) (implies (and (>= x 1701) (<= x 1800)) (= y C)) (implies (and (>= x 1902) (<= x 1904)) (= y I)) (implies (and (>= x 1906) (<= x 1906)) (= y V)) (implies (and (>= x 1909) (<= x 1909)) (= y I)) (implies (and (>= x 1911) (<= x 1940)) (= y X)) (implies (and (>= x 1951) (<= x 1960)) (= y L)) (implies (and (>= x 1990) (<= x 1990)) (= y X)) (implies (and (>= x 2003) (<= x 2014)) (= y I)) (implies (and (>= x 2016) (<= x 2016)) (= y V)) (implies (and (>= x 2019) (<= x 2019)) (= y I)) (implies (and (>= x 2021) (<= x 2030)) (= y X)) (implies (and (>= x 2041) (<= x 2045)) (= y L)) (implies (and (>= x 2052) (<= x 2054)) (= y I)) (implies (and (>= x 2056) (<= x 2056)) (= y V)) (implies (and (>= x 2059) (<= x 2059)) (= y I)) (implies (and (>= x 2061) (<= x 2070)) (= y X)) (implies (and (>= x 2091) (<= x 2095)) (= y C)) (implies (and (>= x 2102) (<= x 2104)) (= y I)) (implies (and (>= x 2106) (<= x 2106)) (= y V)) (implies (and (>= x 2109) (<= x 2109)) (= y I)) (implies (and (>= x 2111) (<= x 2140)) (= y X)) (implies (and (>= x 2151) (<= x 2160)) (= y L)) (implies (and (>= x 2190) (<= x 2190)) (= y X)) (implies (and (>= x 2201) (<= x 2300)) (= y C)) (implies (and (>= x 2401) (<= x 2450)) (= y D)) (implies (and (>= x 2502) (<= x 2504)) (= y I)) (implies (and (>= x 2506) (<= x 2506)) (= y V)) (implies (and (>= x 2509) (<= x 2509)) (= y I)) (implies (and (>= x 2511) (<= x 2540)) (= y X)) (implies (and (>= x 2551) (<= x 2560)) (= y L)) (implies (and (>= x 2590) (<= x 2590)) (= y X)) (implies (and (>= x 2601) (<= x 2700)) (= y C)) (implies (and (>= x 2901) (<= x 2950)) (= y M)) (implies (and (>= x 3002) (<= x 3004)) (= y I)) (implies (and (>= x 3006) (<= x 3006)) (= y V)) (implies (and (>= x 3009) (<= x 3009)) (= y I)) (implies (and (>= x 3011) (<= x 3040)) (= y X)) (implies (and (>= x 3051) (<= x 3060)) (= y L)) (implies (and (>= x 3090) (<= x 3090)) (= y X)) (implies (and (>= x 3101) (<= x 3400)) (= y C)) (implies (and (>= x 3501) (<= x 3600)) (= y D)) (implies (and (>= x 3900) (<= x 3900)) (= y C)))
)
(define-fun rom5 ((x Int) (y Rom)) Bool
(and (implies (and (>= x 18) (<= x 32)) (= y I)) (implies (and (>= x 34) (<= x 34)) (= y V)) (implies (and (>= x 36) (<= x 36)) (= y I)) (implies (and (>= x 39) (<= x 39)) (= y X)) (implies (and (>= x 43) (<= x 72)) (= y I)) (implies (and (>= x 74) (<= x 74)) (= y V)) (implies (and (>= x 76) (<= x 76)) (= y I)) (implies (and (>= x 79) (<= x 79)) (= y X)) (implies (and (>= x 81) (<= x 81)) (= y I)) (implies (and (>= x 85) (<= x 85)) (= y V)) (implies (and (>= x 93) (<= x 122)) (= y I)) (implies (and (>= x 124) (<= x 124)) (= y V)) (implies (and (>= x 126) (<= x 126)) (= y I)) (implies (and (>= x 129) (<= x 129)) (= y X)) (implies (and (>= x 131) (<= x 131)) (= y I)) (implies (and (>= x 135) (<= x 135)) (= y V)) (implies (and (>= x 142) (<= x 142)) (= y I)) (implies (and (>= x 144) (<= x 144)) (= y V)) (implies (and (>= x 146) (<= x 146)) (= y I)) (implies (and (>= x 149) (<= x 149)) (= y X)) (implies (and (>= x 153) (<= x 162)) (= y I)) (implies (and (>= x 164) (<= x 164)) (= y V)) (implies (and (>= x 166) (<= x 166)) (= y I)) (implies (and (>= x 169) (<= x 169)) (= y X)) (implies (and (>= x 171) (<= x 171)) (= y I)) (implies (and (>= x 175) (<= x 175)) (= y V)) (implies (and (>= x 180) (<= x 180)) (= y X)) (implies (and (>= x 192) (<= x 192)) (= y I)) (implies (and (>= x 194) (<= x 194)) (= y V)) (implies (and (>= x 196) (<= x 196)) (= y I)) (implies (and (>= x 199) (<= x 199)) (= y X)) (implies (and (>= x 203) (<= x 212)) (= y I)) (implies (and (>= x 214) (<= x 214)) (= y V)) (implies (and (>= x 216) (<= x 216)) (= y I)) (implies (and (>= x 219) (<= x 219)) (= y X)) (implies (and (>= x 221) (<= x 221)) (= y I)) (implies (and (>= x 225) (<= x 225)) (= y V)) (implies (and (>= x 230) (<= x 230)) (= y X)) (implies (and (>= x 241) (<= x 241)) (= y I)) (implies (and (>= x 245) (<= x 245)) (= y V)) (implies (and (>= x 252) (<= x 252)) (= y I)) (implies (and (>= x 254) (<= x 254)) (= y V)) (implies (and (>= x 256) (<= x 256)) (= y I)) (implies (and (>= x 259) (<= x 259)) (= y X)) (implies (and (>= x 261) (<= x 261)) (= y I)) (implies (and (>= x 265) (<= x 265)) (= y V)) (implies (and (>= x 270) (<= x 270)) (= y X)) (implies (and (>= x 291) (<= x 291)) (= y I)) (implies (and (>= x 295) (<= x 295)) (= y V)) (implies (and (>= x 302) (<= x 302)) (= y I)) (implies (and (>= x 304) (<= x 304)) (= y V)) (implies (and (>= x 306) (<= x 306)) (= y I)) (implies (and (>= x 309) (<= x 309)) (= y X)) (implies (and (>= x 311) (<= x 311)) (= y I)) (implies (and (>= x 315) (<= x 315)) (= y V)) (implies (and (>= x 320) (<= x 320)) (= y X)) (implies (and (>= x 340) (<= x 340)) (= y L)) (implies (and (>= x 351) (<= x 351)) (= y I)) (implies (and (>= x 355) (<= x 355)) (= y V)) (implies (and (>= x 360) (<= x 360)) (= y X)) (implies (and (>= x 390) (<= x 390)) (= y C)) (implies (and (>= x 403) (<= x 412)) (= y I)) (implies (and (>= x 414) (<= x 414)) (= y V)) (implies (and (>= x 416) (<= x 416)) (= y I)) (implies (and (>= x 419) (<= x 419)) (= y X)) (implies (and (>= x 421) (<= x 421)) (= y I)) (implies (and (>= x 425) (<= x 425)) (= y V)) (implies (and (>= x 430) (<= x 430)) (= y X)) (implies (and (>= x 441) (<= x 441)) (= y I)) (implies (and (>= x 445) (<= x 445)) (= y V)) (implies (and (>= x 452) (<= x 452)) (= y I)) (implies (and (>= x 454) (<= x 454)) (= y V)) (implies (and (>= x 456) (<= x 456)) (= y I)) (implies (and (>= x 459) (<= x 459)) (= y X)) (implies (and (>= x 461) (<= x 461)) (= y I)) (implies (and (>= x 465) (<= x 465)) (= y V)) (implies (and (>= x 470) (<= x 470)) (= y X)) (implies (and (>= x 491) (<= x 491)) (= y I)) (implies (and (>= x 495) (<= x 495)) (= y V)) (implies (and (>= x 508) (<= x 522)) (= y I)) (implies (and (>= x 524) (<= x 524)) (= y V)) (implies (and (>= x 526) (<= x 526)) (= y I)) (implies (and (>= x 529) (<= x 529)) (= y X)) (implies (and (>= x 531) (<= x 531)) (= y I)) (implies (and (>= x 535) (<= x 535)) (= y V)) (implies (and (>= x 542) (<= x 542)) (= y I)) (implies (and (>= x 544) (<= x 544)) (= y V)) (implies (and (>= x 546) (<= x 546)) (= y I)) (implies (and (>= x 549) (<= x 549)) (= y X)) (implies (and (>= x 553) (<= x 562)) (= y I)) (implies (and (>= x 564) (<= x 564)) (= y V)) (implies (and (>= x 566) (<= x 566)) (= y I)) (implies (and (>= x 569) (<= x 569)) (= y X)) (implies (and (>= x 571) (<= x 571)) (= y I)) (implies (and (>= x 575) (<= x 575)) (= y V)) (implies (and (>= x 580) (<= x 580)) (= y X)) (implies (and (>= x 592) (<= x 592)) (= y I)) (implies (and (>= x 594) (<= x 594)) (= y V)) (implies (and (>= x 596) (<= x 596)) (= y I)) (implies (and (>= x 599) (<= x 599)) (= y X)) (implies (and (>= x 603) (<= x 612)) (= y I)) (implies (and (>= x 614) (<= x 614)) (= y V)) (implies (and (>= x 616) (<= x 616)) (= y I)) (implies (and (>= x 619) (<= x 619)) (= y X)) (implies (and (>= x 621) (<= x 621)) (= y I)) (implies (and (>= x 625) (<= x 625)) (= y V)) (implies (and (>= x 630) (<= x 630)) (= y X)) (implies (and (>= x 641) (<= x 641)) (= y I)) (implies (and (>= x 645) (<= x 645)) (= y V)) (implies (and (>= x 652) (<= x 652)) (= y I)) (implies (and (>= x 654) (<= x 654)) (= y V)) (implies (and (>= x 656) (<= x 656)) (= y I)) (implies (and (>= x 659) (<= x 659)) (= y X)) (implies (and (>= x 661) (<= x 661)) (= y I)) (implies (and (>= x 665) (<= x 665)) (= y V)) (implies (and (>= x 670) (<= x 670)) (= y X)) (implies (and (>= x 691) (<= x 691)) (= y I)) (implies (and (>= x 695) (<= x 695)) (= y V)) (implies (and (>= x 702) (<= x 702)) (= y I)) (implies (and (>= x 704) (<= x 704)) (= y V)) (implies (and (>= x 706) (<= x 706)) (= y I)) (implies (and (>= x 709) (<= x 709)) (= y X)) (implies (and (>= x 711) (<= x 711)) (= y I)) (implies (and (>= x 715) (<= x 715)) (= y V)) (implies (and (>= x 720) (<= x 720)) (= y X)) (implies (and (>= x 740) (<= x 740)) (= y L)) (implies (and (>= x 751) (<= x 751)) (= y I)) (implies (and (>= x 755) (<= x 755)) (= y V)) (implies (and (>= x 760) (<= x 760)) (= y X)) (implies (and (>= x 790) (<= x 790)) (= y C)) (implies (and (>= x 801) (<= x 801)) (= y I)) (implies (and (>= x 805) (<= x 805)) (= y V)) (implies (and (>= x 810) (<= x 810)) (= y X)) (implies (and (>= x 850) (<= x 850)) (= y L)) (implies (and (>= x 903) (<= x 912)) (= y I)) (implies (and (>= x 914) (<= x 914)) (= y V)) (implies (and (>= x 916) (<= x 916)) (= y I)) (implies (and (>= x 919) (<= x 919)) (= y X)) (implies (and (>= x 921) (<= x 921)) (= y I)) (implies (and (>= x 925) (<= x 925)) (= y V)) (implies (and (>= x 930) (<= x 930)) (= y X)) (implies (and (>= x 941) (<= x 941)) (= y I)) (implies (and (>= x 945) (<= x 945)) (= y V)) (implies (and (>= x 952) (<= x 952)) (= y I)) (implies (and (>= x 954) (<= x 954)) (= y V)) (implies (and (>= x 956) (<= x 956)) (= y I)) (implies (and (>= x 959) (<= x 959)) (= y X)) (implies (and (>= x 961) (<= x 961)) (= y I)) (implies (and (>= x 965) (<= x 965)) (= y V)) (implies (and (>= x 970) (<= x 970)) (= y X)) (implies (and (>= x 991) (<= x 991)) (= y I)) (implies (and (>= x 995) (<= x 995)) (= y V)) (implies (and (>= x 1008) (<= x 1022)) (= y I)) (implies (and (>= x 1024) (<= x 1024)) (= y V)) (implies (and (>= x 1026) (<= x 1026)) (= y I)) (implies (and (>= x 1029) (<= x 1029)) (= y X)) (implies (and (>= x 1031) (<= x 1031)) (= y I)) (implies (and (>= x 1035) (<= x 1035)) (= y V)) (implies (and (>= x 1042) (<= x 1042)) (= y I)) (implies (and (>= x 1044) (<= x 1044)) (= y V)) (implies (and (>= x 1046) (<= x 1046)) (= y I)) (implies (and (>= x 1049) (<= x 1049)) (= y X)) (implies (and (>= x 1053) (<= x 1062)) (= y I)) (implies (and (>= x 1064) (<= x 1064)) (= y V)) (implies (and (>= x 1066) (<= x 1066)) (= y I)) (implies (and (>= x 1069) (<= x 1069)) (= y X)) (implies (and (>= x 1071) (<= x 1071)) (= y I)) (implies (and (>= x 1075) (<= x 1075)) (= y V)) (implies (and (>= x 1080) (<= x 1080)) (= y X)) (implies (and (>= x 1092) (<= x 1092)) (= y I)) (implies (and (>= x 1094) (<= x 1094)) (= y V)) (implies (and (>= x 1096) (<= x 1096)) (= y I)) (implies (and (>= x 1099) (<= x 1099)) (= y X)) (implies (and (>= x 1103) (<= x 1112)) (= y I)) (implies (and (>= x 1114) (<= x 1114)) (= y V)) (implies (and (>= x 1116) (<= x 1116)) (= y I)) (implies (and (>= x 1119) (<= x 1119)) (= y X)) (implies (and (>= x 1121) (<= x 1121)) (= y I)) (implies (and (>= x 1125) (<= x 1125)) (= y V)) (implies (and (>= x 1130) (<= x 1130)) (= y X)) (implies (and (>= x 1141) (<= x 1141)) (= y I)) (implies (and (>= x 1145) (<= x 1145)) (= y V)) (implies (and (>= x 1152) (<= x 1152)) (= y I)) (implies (and (>= x 1154) (<= x 1154)) (= y V)) (implies (and (>= x 1156) (<= x 1156)) (= y I)) (implies (and (>= x 1159) (<= x 1159)) (= y X)) (implies (and (>= x 1161) (<= x 1161)) (= y I)) (implies (and (>= x 1165) (<= x 1165)) (= y V)) (implies (and (>= x 1170) (<= x 1170)) (= y X)) (implies (and (>= x 1191) (<= x 1191)) (= y I)) (implies (and (>= x 1195) (<= x 1195)) (= y V)) (implies (and (>= x 1202) (<= x 1202)) (= y I)) (implies (and (>= x 1204) (<= x 1204)) (= y V)) (implies (and (>= x 1206) (<= x 1206)) (= y I)) (implies (and (>= x 1209) (<= x 1209)) (= y X)) (implies (and (>= x 1211) (<= x 1211)) (= y I)) (implies (and (>= x 1215) (<= x 1215)) (= y V)) (implies (and (>= x 1220) (<= x 1220)) (= y X)) (implies (and (>= x 1240) (<= x 1240)) (= y L)) (implies (and (>= x 1251) (<= x 1251)) (= y I)) (implies (and (>= x 1255) (<= x 1255)) (= y V)) (implies (and (>= x 1260) (<= x 1260)) (= y X)) (implies (and (>= x 1290) (<= x 1290)) (= y C)) (implies (and (>= x 1301) (<= x 1301)) (= y I)) (implies (and (>= x 1305) (<= x 1305)) (= y V)) (implies (and (>= x 1310) (<= x 1310)) (= y X)) (implies (and (>= x 1350) (<= x 1350)) (= y L)) (implies (and (>= x 1402) (<= x 1402)) (= y I)) (implies (and (>= x 1404) (<= x 1404)) (= y V)) (implies (and (>= x 1406) (<= x 1406)) (= y I)) (implies (and (>= x 1409) (<= x 1409)) (= y X)) (implies (and (>= x 1411) (<= x 1411)) (= y I)) (implies (and (>= x 1415) (<= x 1415)) (= y V)) (implies (and (>= x 1420) (<= x 1420)) (= y X)) (implies (and (>= x 1440) (<= x 1440)) (= y L)) (implies (and (>= x 1451) (<= x 1451)) (= y I)) (implies (and (>= x 1455) (<= x 1455)) (= y V)) (implies (and (>= x 1460) (<= x 1460)) (= y X)) (implies (and (>= x 1490) (<= x 1490)) (= y C)) (implies (and (>= x 1503) (<= x 1512)) (= y I)) (implies (and (>= x 1514) (<= x 1514)) (= y V)) (implies (and (>= x 1516) (<= x 1516)) (= y I)) (implies (and (>= x 1519) (<= x 1519)) (= y X)) (implies (and (>= x 1521) (<= x 1521)) (= y I)) (implies (and (>= x 1525) (<= x 1525)) (= y V)) (implies (and (>= x 1530) (<= x 1530)) (= y X)) (implies (and (>= x 1541) (<= x 1541)) (= y I)) (implies (and (>= x 1545) (<= x 1545)) (= y V)) (implies (and (>= x 1552) (<= x 1552)) (= y I)) (implies (and (>= x 1554) (<= x 1554)) (= y V)) (implies (and (>= x 1556) (<= x 1556)) (= y I)) (implies (and (>= x 1559) (<= x 1559)) (= y X)) (implies (and (>= x 1561) (<= x 1561)) (= y I)) (implies (and (>= x 1565) (<= x 1565)) (= y V)) (implies (and (>= x 1570) (<= x 1570)) (= y X)) (implies (and (>= x 1591) (<= x 1591)) (= y I)) (implies (and (>= x 1595) (<= x 1595)) (= y V)) (implies (and (>= x 1602) (<= x 1602)) (= y I)) (implies (and (>= x 1604) (<= x 1604)) (= y V)) (implies (and (>= x 1606) (<= x 1606)) (= y I)) (implies (and (>= x 1609) (<= x 1609)) (= y X)) (implies (and (>= x 1611) (<= x 1611)) (= y I)) (implies (and (>= x 1615) (<= x 1615)) (= y V)) (implies (and (>= x 1620) (<= x 1620)) (= y X)) (implies (and (>= x 1640) (<= x 1640)) (= y L)) (implies (and (>= x 1651) (<= x 1651)) (= y I)) (implies (and (>= x 1655) (<= x 1655)) (= y V)) (implies (and (>= x 1660) (<= x 1660)) (= y X)) (implies (and (>= x 1690) (<= x 1690)) (= y C)) (implies (and (>= x 1701) (<= x 1701)) (= y I)) (implies (and (>= x 1705) (<= x 1705)) (= y V)) (implies (and (>= x 1710) (<= x 1710)) (= y X)) (implies (and (>= x 1750) (<= x 1750)) (= y L)) (implies (and (>= x 1800) (<= x 1800)) (= y C)) (implies (and (>= x 1902) (<= x 1902)) (= y I)) (implies (and (>= x 1904) (<= x 1904)) (= y V)) (implies (and (>= x 1906) (<= x 1906)) (= y I)) (implies (and (>= x 1909) (<= x 1909)) (= y X)) (implies (and (>= x 1911) (<= x 1911)) (= y I)) (implies (and (>= x 1915) (<= x 1915)) (= y V)) (implies (and (>= x 1920) (<= x 1920)) (= y X)) (implies (and (>= x 1940) (<= x 1940)) (= y L)) (implies (and (>= x 1951) (<= x 1951)) (= y I)) (implies (and (>= x 1955) (<= x 1955)) (= y V)) (implies (and (>= x 1960) (<= x 1960)) (= y X)) (implies (and (>= x 1990) (<= x 1990)) (= y C)) (implies (and (>= x 2003) (<= x 2012)) (= y I)) (implies (and (>= x 2014) (<= x 2014)) (= y V)) (implies (and (>= x 2016) (<= x 2016)) (= y I)) (implies (and (>= x 2019) (<= x 2019)) (= y X)) (implies (and (>= x 2021) (<= x 2021)) (= y I)) (implies (and (>= x 2025) (<= x 2025)) (= y V)) (implies (and (>= x 2030) (<= x 2030)) (= y X)) (implies (and (>= x 2041) (<= x 2041)) (= y I)) (implies (and (>= x 2045) (<= x 2045)) (= y V)) (implies (and (>= x 2052) (<= x 2052)) (= y I)) (implies (and (>= x 2054) (<= x 2054)) (= y V)) (implies (and (>= x 2056) (<= x 2056)) (= y I)) (implies (and (>= x 2059) (<= x 2059)) (= y X)) (implies (and (>= x 2061) (<= x 2061)) (= y I)) (implies (and (>= x 2065) (<= x 2065)) (= y V)) (implies (and (>= x 2070) (<= x 2070)) (= y X)) (implies (and (>= x 2091) (<= x 2091)) (= y I)) (implies (and (>= x 2095) (<= x 2095)) (= y V)) (implies (and (>= x 2102) (<= x 2102)) (= y I)) (implies (and (>= x 2104) (<= x 2104)) (= y V)) (implies (and (>= x 2106) (<= x 2106)) (= y I)) (implies (and (>= x 2109) (<= x 2109)) (= y X)) (implies (and (>= x 2111) (<= x 2111)) (= y I)) (implies (and (>= x 2115) (<= x 2115)) (= y V)) (implies (and (>= x 2120) (<= x 2120)) (= y X)) (implies (and (>= x 2140) (<= x 2140)) (= y L)) (implies (and (>= x 2151) (<= x 2151)) (= y I)) (implies (and (>= x 2155) (<= x 2155)) (= y V)) (implies (and (>= x 2160) (<= x 2160)) (= y X)) (implies (and (>= x 2190) (<= x 2190)) (= y C)) (implies (and (>= x 2201) (<= x 2201)) (= y I)) (implies (and (>= x 2205) (<= x 2205)) (= y V)) (implies (and (>= x 2210) (<= x 2210)) (= y X)) (implies (and (>= x 2250) (<= x 2250)) (= y L)) (implies (and (>= x 2300) (<= x 2300)) (= y C)) (implies (and (>= x 2401) (<= x 2401)) (= y I)) (implies (and (>= x 2405) (<= x 2405)) (= y V)) (implies (and (>= x 2410) (<= x 2410)) (= y X)) (implies (and (>= x 2450) (<= x 2450)) (= y L)) (implies (and (>= x 2502) (<= x 2502)) (= y I)) (implies (and (>= x 2504) (<= x 2504)) (= y V)) (implies (and (>= x 2506) (<= x 2506)) (= y I)) (implies (and (>= x 2509) (<= x 2509)) (= y X)) (implies (and (>= x 2511) (<= x 2511)) (= y I)) (implies (and (>= x 2515) (<= x 2515)) (= y V)) (implies (and (>= x 2520) (<= x 2520)) (= y X)) (implies (and (>= x 2540) (<= x 2540)) (= y L)) (implies (and (>= x 2551) (<= x 2551)) (= y I)) (implies (and (>= x 2555) (<= x 2555)) (= y V)) (implies (and (>= x 2560) (<= x 2560)) (= y X)) (implies (and (>= x 2590) (<= x 2590)) (= y C)) (implies (and (>= x 2601) (<= x 2601)) (= y I)) (implies (and (>= x 2605) (<= x 2605)) (= y V)) (implies (and (>= x 2610) (<= x 2610)) (= y X)) (implies (and (>= x 2650) (<= x 2650)) (= y L)) (implies (and (>= x 2700) (<= x 2700)) (= y C)) (implies (and (>= x 2901) (<= x 2901)) (= y I)) (implies (and (>= x 2905) (<= x 2905)) (= y V)) (implies (and (>= x 2910) (<= x 2910)) (= y X)) (implies (and (>= x 2950) (<= x 2950)) (= y L)) (implies (and (>= x 3002) (<= x 3002)) (= y I)) (implies (and (>= x 3004) (<= x 3004)) (= y V)) (implies (and (>= x 3006) (<= x 3006)) (= y I)) (implies (and (>= x 3009) (<= x 3009)) (= y X)) (implies (and (>= x 3011) (<= x 3011)) (= y I)) (implies (and (>= x 3015) (<= x 3015)) (= y V)) (implies (and (>= x 3020) (<= x 3020)) (= y X)) (implies (and (>= x 3040) (<= x 3040)) (= y L)) (implies (and (>= x 3051) (<= x 3051)) (= y I)) (implies (and (>= x 3055) (<= x 3055)) (= y V)) (implies (and (>= x 3060) (<= x 3060)) (= y X)) (implies (and (>= x 3090) (<= x 3090)) (= y C)) (implies (and (>= x 3101) (<= x 3101)) (= y I)) (implies (and (>= x 3105) (<= x 3105)) (= y V)) (implies (and (>= x 3110) (<= x 3110)) (= y X)) (implies (and (>= x 3150) (<= x 3150)) (= y L)) (implies (and (>= x 3200) (<= x 3200)) (= y C)) (implies (and (>= x 3400) (<= x 3400)) (= y D)) (implies (and (>= x 3501) (<= x 3501)) (= y I)) (implies (and (>= x 3505) (<= x 3505)) (= y V)) (implies (and (>= x 3510) (<= x 3510)) (= y X)) (implies (and (>= x 3550) (<= x 3550)) (= y L)) (implies (and (>= x 3600) (<= x 3600)) (= y C)) (implies (and (>= x 3900) (<= x 3900)) (= y M)))
)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(declare-const e Int)
(declare-const f Int)
(declare-const g Int)
(declare-const h Int)
(declare-const i Int)
(declare-const j Int)
(assert (ran b))
(assert (cran c))
(assert (ran d))
(assert (ran e))
(assert (ran f))
(assert (ran g))
(assert (ran h))
(assert (ran i))
(assert (ran j))
(declare-const m11 Rom)
(declare-const m12 Rom)
(declare-const m13 Rom)
(declare-const m14 Rom)
(declare-const m15 Rom)
(declare-const m21 Rom)
(declare-const m22 Rom)
(declare-const m23 Rom)
(declare-const m24 Rom)
(declare-const m25 Rom)
(declare-const m31 Rom)
(declare-const m32 Rom)
(declare-const m33 Rom)
(declare-const m34 Rom)
(declare-const m35 Rom)
(declare-const m41 Rom)
(declare-const m42 Rom)
(declare-const m43 Rom)
(declare-const m44 Rom)
(declare-const m45 Rom)
(declare-const m51 Rom)
(declare-const m52 Rom)
(declare-const m53 Rom)
(declare-const m54 Rom)
(declare-const m55 Rom)
(assert (rom1 e m11))
(assert (rom2 e m21))
(assert (rom3 e m31))
(assert (rom4 e m41))
(assert (rom5 e m51))
(assert (rom1 d m12))
(assert (rom2 d m22))
(assert (rom3 d m32))
(assert (rom4 d m42))
(assert (rom5 d m52))
(assert (rom1 c m13))
(assert (rom2 c m23))
(assert (rom3 c m33))
(assert (rom4 c m43))
(assert (rom5 c m53))
(assert (rom1 b m14))
(assert (rom2 b m24))
(assert (rom3 b m34))
(assert (rom4 b m44))
(assert (rom5 b m54))
(assert (rom1 f m11))
(assert (rom2 f m12))
(assert (rom3 f m13))
(assert (rom4 f m14))
(assert (rom5 f m15))
(assert (rom1 g m21))
(assert (rom2 g m22))
(assert (rom3 g m23))
(assert (rom4 g m24))
(assert (rom5 g m25))
(assert (rom1 h m31))
(assert (rom2 h m32))
(assert (rom3 h m33))
(assert (rom4 h m34))
(assert (rom5 h m35))
(assert (rom1 i m41))
(assert (rom2 i m42))
(assert (rom3 i m43))
(assert (rom4 i m44))
(assert (rom5 i m45))
(assert (rom1 j m51))
(assert (rom2 j m52))
(assert (rom3 j m53))
(assert (rom4 j m54))
(assert (rom5 j m55))
; Eisen:
; F oneven
(declare-const x Int)
(assert (= (+ x x 1) f))
; D = F
(assert (= d f))
; C is een priemgetal
; staat boven
; B + E = G + H
(assert (= (+ b e) (+ g h)))
; J is een deler van E
(declare-const y Int)
(assert (= e (* j y)))
; C - D + I = C + I + I
(assert (= (+ c -500 i) (+ 100 1 1)))
; D is groter dan G
(assert (> d g))
; Oplossen
(check-sat)
(get-value (m15))
(get-value (m25))
(get-value (m35))
(get-value (m45))
(get-value (m55))
(get-value (b))
(get-value (c))
(get-value (d))
(get-value (e))
(get-value (f))
(get-value (g))
(get-value (h))
(get-value (i))
(get-value (j))
; Check uniciteit van de oplossing
(push 1)
(assert (not (= m15 V)))
(check-sat)
(get-value (m15))
(pop)
(push 1)
(assert (not (= m25 I)))
(check-sat)
(get-value (m25))
(pop)
(push 1)
(assert (not (= m35 C)))
(check-sat)
(get-value (m35))
(pop)
(push 1)
(assert (not (= m45 I)))
(check-sat)
(get-value (m45))
(pop)
(push 1)
(assert (not (= m55 I)))
(check-sat)
(get-value (m55))
(pop)