From a1a44c953a57b7cdf188cebdabcc898db51982a5 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Sun, 26 May 2019 15:28:45 +0200 Subject: [PATCH] Added the problems --- README.md | 5 +- main.smt | 70 +++++++++++++ opg22.smt | 208 +++++++++++++++++++++++++++++++++++++++ opgave4aivd.smt | 248 +++++++++++++++++++++++++++++++++++++++++++++++ superperm.smt | 59 +++++++++++ superperm2.proof | 37 +++++++ superperm2.smt | 135 ++++++++++++++++++++++++++ 7 files changed, 761 insertions(+), 1 deletion(-) create mode 100644 main.smt create mode 100644 opg22.smt create mode 100644 opgave4aivd.smt create mode 100644 superperm.smt create mode 100644 superperm2.proof create mode 100644 superperm2.smt diff --git a/README.md b/README.md index 1a54015..7af2cd4 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,6 @@ # smt-solving -Collections of smt problems \ No newline at end of file +Collections of smt problems. Some for AVID +kerstpuzzel. I have some for an A&D assignment. +And there is one for superpermutations. + diff --git a/main.smt b/main.smt new file mode 100644 index 0000000..576189e --- /dev/null +++ b/main.smt @@ -0,0 +1,70 @@ +(set-option :produce-proofs true) +(declare-datatypes () ((Box (mk-box (fst Real) (snd Real) (trd Real))))) + +; Valid interval = (1/2, 1) +(define-fun valint ((x Real)) Bool + (and (< 0.5 x) (< x 1))) +; Valid box +(define-fun valbox ((x Box)) Bool + (and (valint (fst x)) + (valint (snd x)) + (valint (trd x)))) + +(define-fun fits1 ((x1 Real) (x2 Real) (x3 Real) (y1 Real) (y2 Real) (y3 Real)) Bool + (and (< x1 y1) (< x2 y2) (< x3 y3))) +(define-fun fits2 ((x1 Real) (x2 Real) (x3 Real) (y1 Real) (y2 Real) (y3 Real)) Bool + (or + (fits1 x1 x2 x3 y1 y2 y3) + (fits1 x1 x2 x3 y1 y3 y2) + (fits1 x1 x2 x3 y2 y1 y3) + (fits1 x1 x2 x3 y2 y3 y1) + (fits1 x1 x2 x3 y3 y1 y2) + (fits1 x1 x2 x3 y3 y2 y1))) +; Box x fits inside box y +(define-fun fits ((x Box) (y Box)) Bool + (fits2 (fst x) (snd x) (trd x) (fst y) (snd y) (trd y))) +; x and y do not fit in each other +(define-fun nfits ((x Box) (y Box)) Bool + (and (not (fits x y)) (not (fits y x)))) + +; nodes +(declare-datatypes () ((Dom A1 A2 A4 A7 A8 A11 A13 A14))) +; edges +(declare-fun rel (Dom Dom) Bool) +; transitive +(assert (forall ((x Dom) (y Dom) (z Dom)) (implies (and (rel x y) (rel y z)) (rel x z)))) +; acyclic +(assert (forall ((x Dom) (y Dom)) (not (and (rel x y) (rel y x))))) + +(assert (rel A1 A7)) +(assert (rel A2 A7)) +(assert (rel A4 A7)) +(assert (not (rel A8 A7))) +(assert (rel A1 A11)) +(assert (rel A2 A11)) +(assert (not (rel A4 A11))) +(assert (rel A8 A11)) +(assert (rel A1 A13)) +(assert (not (rel A2 A13))) +(assert (rel A4 A13)) +(assert (rel A8 A13)) +(assert (not (rel A1 A14))) +(assert (rel A2 A14)) +(assert (rel A4 A14)) +(assert (rel A8 A14)) + +; check graph +(check-sat) +(push) + +; strong homomorphism to boxes +(declare-fun boxes (Dom) Box) +(assert (forall ((x Dom)) (valbox (boxes x)))) +(assert (forall ((x Dom) (y Dom)) (implies (rel x y) (fits (boxes x) (boxes y))))) +(assert (forall ((x Dom) (y Dom)) (implies (fits (boxes x) (boxes y)) (rel x y)))) + +; Compute boxes +(check-sat) +; (get-proof) +(pop) +(exit) diff --git a/opg22.smt b/opg22.smt new file mode 100644 index 0000000..d06de61 --- /dev/null +++ b/opg22.smt @@ -0,0 +1,208 @@ +; 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) diff --git a/opgave4aivd.smt b/opgave4aivd.smt new file mode 100644 index 0000000..45aa51a --- /dev/null +++ b/opgave4aivd.smt @@ -0,0 +1,248 @@ +(set-option :produce-proofs true) + +(define-fun chr ((x Int)) String + (ite (= x 26) "z" (ite (= x 25) "y" (ite (= x 24) "x" (ite (= x 23) "w" (ite (= x 22) "v" (ite (= x 21) "u" (ite (= x 20) "t" (ite (= x 19) "s" (ite (= x 18) "r" (ite (= x 17) "q" (ite (= x 16) "p" (ite (= x 15) "o" (ite (= x 14) "n" (ite (= x 13) "m" (ite (= x 12) "l" (ite (= x 11) "k" (ite (= x 10) "j" (ite (= x 9) "i" (ite (= x 8) "h" (ite (= x 7) "g" (ite (= x 6) "f" (ite (= x 5) "e" (ite (= x 4) "d" (ite (= x 3) "c" (ite (= x 2) "b" (ite (= x 1) "a" "-"))))))))))))))))))))))))))) + +(define-fun klinker ((x Int)) Bool + (or (= x 1) (= x 5) (= x 9) (= x 15) (= x 21) (= x 25))) + +(define-fun verboden ((x Int)) Bool + (or + (= x 25) + (= x 24) + )) + +(define-fun ran ((x Int)) Bool + (and (<= 0 x) (<= x 44))) + +; +; +; 3 +; _4_ 5 _10_ +; _0_ _1_ 2 6 7 _8_ 9 11 12 _13_ +; + +(declare-fun letter (Int) Int) +(define-fun drie ((x Int) (y Int) (z Int)) Bool + (= (letter x) (+ (letter y) (letter z)))) + +(assert (forall ((x Int)) (and (>= (letter x) 1) (<= (letter x) 26)))) +(assert (= (letter 0) 4)) +(assert (= (letter 1) 5)) +(assert (drie 3 4 5)) +(assert (= (letter 4) 13)) +(assert (drie 4 6 7)) +(assert (drie 5 7 8)) +(assert (= (letter 8) 4)) +(assert (= (letter 10) 23)) +(assert (drie 10 11 12)) +(assert (= (letter 13) 4)) +(assert (= (letter 14) 26)) +(assert (drie 15 16 17)) +(assert (= (letter 16) 5)) +(assert (= (letter 18) 5)) +(assert (= (letter 19) 14)) + +(assert (= (letter 21) 20)) +(assert (= (letter 24) 14)) +(assert (drie 21 22 23)) +(assert (drie 22 24 25)) +(assert (drie 23 25 26)) + +(assert (= (letter 27) 5)) +(assert (= (letter 28) 5)) +(assert (= (letter 29) 14)) + +(assert (= (letter 38) 4)) +(assert (drie 30 31 32)) +(assert (drie 31 33 34)) +(assert (drie 32 34 35)) +(assert (drie 33 36 37)) +(assert (drie 34 37 38)) +(assert (drie 35 38 39)) + +(assert (= (letter 44) 6)) +(assert (drie 42 43 44)) + +(define-fun rk ((x Int)) Bool + (and (ran x) (klinker (letter x)))) + +(assert (exists ((a1 Int) (a2 Int) (a3 Int) (a4 Int) (a5 Int) (a6 Int) (a7 Int)) + (and + (distinct a1 a2 a3 a4 a5 a6 a7) + (rk a1) (rk a2) (rk a3) (rk a4) (rk a5) (rk a6) (rk a7) + ))) + +; nergens een 'x','y'... +(assert (forall ((a Int)) (not (verboden (letter a))))) + +; (a,1),(b,2),(c,3),(d,4),(e,5),(f,6),(g,7),(h,8),(i,9), +; (j,10),(k,11),(l,12),(m,13),(n,14),(o,15),(p,16),(q,17), +; (r,18),(s,19),(t,20),(u,21),(v,22),(w,23),(x,24),(y,25),(z,26) + + +; '...mih...' kan niet +(assert (forall ((a Int)) + (not (and (= (letter (+ a 0)) 13) + (= (letter (+ a 1)) 9) + (= (letter (+ a 2)) 8) + )))) + +; '...zmm...' kan niet +(assert (forall ((a Int)) + (not (and (= (letter (+ a 0)) 26) + (= (letter (+ a 1)) 13) + (= (letter (+ a 2)) 13) + )))) + +; '...dzz...' kan niet +(assert (forall ((a Int)) + (not (and (= (letter (+ a 0)) 4) + (= (letter (+ a 1)) 26) + (= (letter (+ a 2)) 26) + )))) + +; '...tpd...' kan niet +(assert (forall ((a Int)) + (not (and (= (letter (+ a 0)) 20) + (= (letter (+ a 1)) 16) + (= (letter (+ a 2)) 4) + )))) + +; '...nzl...' kan niet +(assert (forall ((a Int)) + (not (and (= (letter (+ a 0)) 14) + (= (letter (+ a 1)) 26) + (= (letter (+ a 2)) 12) + )))) + +; '...ggb...' kan niet +(assert (forall ((a Int)) + (not (and (= (letter (+ a 0)) 7) + (= (letter (+ a 1)) 7) + (= (letter (+ a 2)) 2) + )))) + +; '...cff...' kan niet +(assert (forall ((a Int)) + (not (and (= (letter (+ a 0)) 3) + (= (letter (+ a 1)) 6) + (= (letter (+ a 2)) 6) + )))) + +; '...bcd...' kan niet +(assert (forall ((a Int)) + (not (and (= (letter (+ a 0)) 2) + (= (letter (+ a 1)) 3) + (= (letter (+ a 2)) 4) + )))) + +; nzn +(assert (forall ((a Int)) + (not (and (= (letter (+ a 0)) 14) + (= (letter (+ a 1)) 26) + (= (letter (+ a 2)) 14) + )))) + +; nwh +(assert (forall ((a Int)) + (not (and (= (letter (+ a 0)) 14) + (= (letter (+ a 1)) 23) + (= (letter (+ a 2)) 8) + )))) + +; nwm +(assert (forall ((a Int)) + (not (and (= (letter (+ a 0)) 14) + (= (letter (+ a 1)) 23) + (= (letter (+ a 2)) 13) + )))) + +; nwk +(assert (forall ((a Int)) + (not (and (= (letter (+ a 0)) 14) + (= (letter (+ a 1)) 23) + (= (letter (+ a 2)) 11) + )))) + +; rhj +(assert (forall ((a Int)) + (not (and (= (letter (+ a 0)) 18) + (= (letter (+ a 1)) 8) + (= (letter (+ a 2)) 10) + )))) + +; zpj +(assert (forall ((a Int)) + (not (and (= (letter (+ a 0)) 26) + (= (letter (+ a 1)) 16) + (= (letter (+ a 2)) 10) + )))) + +; qgj +(assert (forall ((a Int)) + (not (and (= (letter (+ a 0)) 17) + (= (letter (+ a 1)) 7) + (= (letter (+ a 2)) 10) + )))) + +; '...umhi...' kan niet +(assert (forall ((a Int)) + (not (and (= (letter (+ a 0)) 21) + (= (letter (+ a 1)) 13) + (= (letter (+ a 2)) 8) + (= (letter (+ a 3)) 9) + )))) + +(assert (= (letter 11) 9)) ; w_i_nd + +(assert (<= (letter 37) 2)) ; a of b. + +(assert (= (letter 43) 1)) ; g_a_f. + +(check-sat) +(get-value ((chr (letter 0)))) +(get-value ((chr (letter 1)))) +(get-value ((chr (letter 2)))) +(get-value ((chr (letter 3)))) +(get-value ((chr (letter 4)))) +(get-value ((chr (letter 5)))) +(get-value ((chr (letter 6)))) +(get-value ((chr (letter 7)))) +(get-value ((chr (letter 8)))) +(get-value ((chr (letter 9)))) +(get-value ((chr (letter 10)))) +(get-value ((chr (letter 11)))) +(get-value ((chr (letter 12)))) +(get-value ((chr (letter 13)))) +(get-value ((chr (letter 14)))) +(get-value ((chr (letter 15)))) +(get-value ((chr (letter 16)))) +(get-value ((chr (letter 17)))) +(get-value ((chr (letter 18)))) +(get-value ((chr (letter 19)))) +(get-value ((chr (letter 20)))) +(get-value ((chr (letter 21)))) +(get-value ((chr (letter 22)))) +(get-value ((chr (letter 23)))) +(get-value ((chr (letter 24)))) +(get-value ((chr (letter 25)))) +(get-value ((chr (letter 26)))) +(get-value ((chr (letter 27)))) +(get-value ((chr (letter 28)))) +(get-value ((chr (letter 29)))) +(get-value ((chr (letter 30)))) +(get-value ((chr (letter 31)))) +(get-value ((chr (letter 32)))) +(get-value ((chr (letter 33)))) +(get-value ((chr (letter 34)))) +(get-value ((chr (letter 35)))) +(get-value ((chr (letter 36)))) +(get-value ((chr (letter 37)))) +(get-value ((chr (letter 38)))) +(get-value ((chr (letter 39)))) +(get-value ((chr (letter 40)))) +(get-value ((chr (letter 41)))) +(get-value ((chr (letter 42)))) +(get-value ((chr (letter 43)))) +(get-value ((chr (letter 44)))) diff --git a/superperm.smt b/superperm.smt new file mode 100644 index 0000000..32c2009 --- /dev/null +++ b/superperm.smt @@ -0,0 +1,59 @@ +;(set-option :produce-proofs true) + +(define-fun n () Int 4) ; number of symbols +(define-fun len () Int 33) ; length of string +(define-fun len2 () Int 29) + +(define-fun ran ((x Int)) Bool + (and (<= 0 x) (< x len))) + +(define-fun ran2 ((x Int)) Bool + (and (<= 0 x) (<= x len2))) + +(declare-fun perm (Int) Int) +(assert (forall ((x Int)) + (and (>= (perm x) 1) (<= (perm x) n)))) + +(define-fun subWord ((a0 Int) (a1 Int) (a2 Int) (a3 Int)) Bool + (exists ((x Int)) + (and (ran2 x) + (= (perm (+ x 0)) a0) + (= (perm (+ x 1)) a1) + (= (perm (+ x 2)) a2) + (= (perm (+ x 3)) a3) ))) + +;(assert (forall ((x Int)) (not (= (perm x) (perm (+ x 1)))) )) +;(assert (forall ((x Int)) (not (= (perm x) (perm (+ x 2)))) )) + +(assert (= 1 (perm 0))) +(assert (= 2 (perm 1))) +(assert (= 3 (perm 2))) +(assert (= 4 (perm 3))) + +;(assert (subWord 1 2 3 4 5)) +(assert (subWord 1 2 3 4)) +(assert (subWord 2 1 3 4)) +(assert (subWord 3 2 1 4)) +(assert (subWord 2 3 1 4)) +(assert (subWord 3 1 2 4)) +(assert (subWord 1 3 2 4)) +(assert (subWord 4 3 2 1)) +(assert (subWord 3 4 2 1)) +(assert (subWord 3 2 4 1)) +(assert (subWord 4 2 3 1)) +(assert (subWord 2 4 3 1)) +(assert (subWord 2 3 4 1)) +(assert (subWord 4 1 2 3)) +(assert (subWord 1 4 2 3)) +(assert (subWord 1 2 4 3)) +(assert (subWord 4 2 1 3)) +(assert (subWord 2 4 1 3)) +(assert (subWord 2 1 4 3)) +(assert (subWord 4 1 3 2)) +(assert (subWord 1 4 3 2)) +(assert (subWord 1 3 4 2)) +(assert (subWord 4 3 1 2)) +(assert (subWord 3 4 1 2)) +(assert (subWord 3 1 4 2)) + +(check-sat) diff --git a/superperm2.proof b/superperm2.proof new file mode 100644 index 0000000..c73833c --- /dev/null +++ b/superperm2.proof @@ -0,0 +1,37 @@ +unknown +(error "line 135 column 11: proof is not available") +(:added-eqs 103686431 + :arith-add-rows 345 + :arith-assert-diseq 75045628 + :arith-assert-lower 61627173 + :arith-assert-upper 63603655 + :arith-bound-prop 2163 + :arith-conflicts 205 + :arith-eq-adapter 15320 + :arith-fixed-eqs 556790 + :arith-offset-eqs 56410 + :arith-pivots 2351 + :bv-bit2core 52377850 + :bv-conflicts 36500 + :bv-dynamic-eqs 18457182 + :bv->core-eq 18457182 + :conflicts 86074 + :decisions 60974940 + :del-clause 3076236 + :final-checks 402793 + :max-memory 67.43 + :memory 67.26 + :minimized-lits 12979 + :mk-bool-var 129261498 + :mk-clause 3148986 + :num-allocs 5465284107.00 + :num-checks 1 + :propagations 169737856 + :restarts 341 + :rlimit-count 1494080384 + :seq-add-axiom 88311 + :seq-branch 321201 + :seq-fixed-length 81592 + :seq-num-reductions 63534116 + :time 6184.33 + :total-time 6137.96) diff --git a/superperm2.smt b/superperm2.smt new file mode 100644 index 0000000..5843f95 --- /dev/null +++ b/superperm2.smt @@ -0,0 +1,135 @@ +(set-option :produce-proofs true) + +; Some string +(declare-const perm String) + +; of this length +(assert (= (str.len perm) 152)) + +; with these substrings... +(assert (str.prefixof "12345" perm)) +(assert (str.contains perm "21345")) +(assert (str.contains perm "32145")) +(assert (str.contains perm "23145")) +(assert (str.contains perm "31245")) +(assert (str.contains perm "13245")) +(assert (str.contains perm "43215")) +(assert (str.contains perm "34215")) +(assert (str.contains perm "32415")) +(assert (str.contains perm "42315")) +(assert (str.contains perm "24315")) +(assert (str.contains perm "23415")) +(assert (str.contains perm "41235")) +(assert (str.contains perm "14235")) +(assert (str.contains perm "12435")) +(assert (str.contains perm "42135")) +(assert (str.contains perm "24135")) +(assert (str.contains perm "21435")) +(assert (str.contains perm "41325")) +(assert (str.contains perm "14325")) +(assert (str.contains perm "13425")) +(assert (str.contains perm "43125")) +(assert (str.contains perm "34125")) +(assert (str.contains perm "31425")) +(assert (str.contains perm "54321")) +(assert (str.contains perm "45321")) +(assert (str.contains perm "43521")) +(assert (str.contains perm "43251")) +(assert (str.contains perm "53421")) +(assert (str.contains perm "35421")) +(assert (str.contains perm "34521")) +(assert (str.contains perm "34251")) +(assert (str.contains perm "52341")) +(assert (str.contains perm "25341")) +(assert (str.contains perm "23541")) +(assert (str.contains perm "23451")) +(assert (str.contains perm "53241")) +(assert (str.contains perm "35241")) +(assert (str.contains perm "32541")) +(assert (str.contains perm "32451")) +(assert (str.contains perm "52431")) +(assert (str.contains perm "25431")) +(assert (str.contains perm "24531")) +(assert (str.contains perm "24351")) +(assert (str.contains perm "54231")) +(assert (str.contains perm "45231")) +(assert (str.contains perm "42531")) +(assert (str.contains perm "42351")) +(assert (str.contains perm "51234")) +(assert (str.contains perm "15234")) +(assert (str.contains perm "12534")) +(assert (str.contains perm "12354")) +(assert (str.contains perm "52134")) +(assert (str.contains perm "25134")) +(assert (str.contains perm "21534")) +(assert (str.contains perm "21354")) +(assert (str.contains perm "52314")) +(assert (str.contains perm "25314")) +(assert (str.contains perm "23514")) +(assert (str.contains perm "23154")) +(assert (str.contains perm "51324")) +(assert (str.contains perm "15324")) +(assert (str.contains perm "13524")) +(assert (str.contains perm "13254")) +(assert (str.contains perm "53124")) +(assert (str.contains perm "35124")) +(assert (str.contains perm "31524")) +(assert (str.contains perm "31254")) +(assert (str.contains perm "53214")) +(assert (str.contains perm "35214")) +(assert (str.contains perm "32514")) +(assert (str.contains perm "32154")) +(assert (str.contains perm "51432")) +(assert (str.contains perm "15432")) +(assert (str.contains perm "14532")) +(assert (str.contains perm "14352")) +(assert (str.contains perm "54132")) +(assert (str.contains perm "45132")) +(assert (str.contains perm "41532")) +(assert (str.contains perm "41352")) +(assert (str.contains perm "54312")) +(assert (str.contains perm "45312")) +(assert (str.contains perm "43512")) +(assert (str.contains perm "43152")) +(assert (str.contains perm "51342")) +(assert (str.contains perm "15342")) +(assert (str.contains perm "13542")) +(assert (str.contains perm "13452")) +(assert (str.contains perm "53142")) +(assert (str.contains perm "35142")) +(assert (str.contains perm "31542")) +(assert (str.contains perm "31452")) +(assert (str.contains perm "53412")) +(assert (str.contains perm "35412")) +(assert (str.contains perm "34512")) +(assert (str.contains perm "34152")) +(assert (str.contains perm "51423")) +(assert (str.contains perm "15423")) +(assert (str.contains perm "14523")) +(assert (str.contains perm "14253")) +(assert (str.contains perm "54123")) +(assert (str.contains perm "45123")) +(assert (str.contains perm "41523")) +(assert (str.contains perm "41253")) +(assert (str.contains perm "54213")) +(assert (str.contains perm "45213")) +(assert (str.contains perm "42513")) +(assert (str.contains perm "42153")) +(assert (str.contains perm "51243")) +(assert (str.contains perm "15243")) +(assert (str.contains perm "12543")) +(assert (str.contains perm "12453")) +(assert (str.contains perm "52143")) +(assert (str.contains perm "25143")) +(assert (str.contains perm "21543")) +(assert (str.contains perm "21453")) +(assert (str.contains perm "52413")) +(assert (str.contains perm "25413")) +(assert (str.contains perm "24513")) +(assert (str.contains perm "24153")) + +; Does it exist? +(check-sat) + +;(get-model) +(get-proof)