-
Notifications
You must be signed in to change notification settings - Fork 0
/
MyCSP.smt
175 lines (151 loc) · 12 KB
/
MyCSP.smt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
(set-logic QF_UF)
(declare-const b111 Bool)
(declare-const b121 Bool)
(declare-const b131 Bool)
(declare-const b141 Bool)
(declare-const b211 Bool)
(declare-const b221 Bool)
(declare-const b231 Bool)
(declare-const b241 Bool)
(declare-const b311 Bool)
(declare-const b321 Bool)
(declare-const b331 Bool)
(declare-const b341 Bool)
(declare-const b411 Bool)
(declare-const b421 Bool)
(declare-const b431 Bool)
(declare-const b441 Bool)
(declare-const b112 Bool)
(declare-const b122 Bool)
(declare-const b132 Bool)
(declare-const b142 Bool)
(declare-const b212 Bool)
(declare-const b222 Bool)
(declare-const b232 Bool)
(declare-const b242 Bool)
(declare-const b312 Bool)
(declare-const b322 Bool)
(declare-const b332 Bool)
(declare-const b342 Bool)
(declare-const b412 Bool)
(declare-const b422 Bool)
(declare-const b432 Bool)
(declare-const b442 Bool)
(declare-const b113 Bool)
(declare-const b123 Bool)
(declare-const b133 Bool)
(declare-const b143 Bool)
(declare-const b213 Bool)
(declare-const b223 Bool)
(declare-const b233 Bool)
(declare-const b243 Bool)
(declare-const b313 Bool)
(declare-const b323 Bool)
(declare-const b333 Bool)
(declare-const b343 Bool)
(declare-const b413 Bool)
(declare-const b423 Bool)
(declare-const b433 Bool)
(declare-const b443 Bool)
(declare-const b114 Bool)
(declare-const b124 Bool)
(declare-const b134 Bool)
(declare-const b144 Bool)
(declare-const b214 Bool)
(declare-const b224 Bool)
(declare-const b234 Bool)
(declare-const b244 Bool)
(declare-const b314 Bool)
(declare-const b324 Bool)
(declare-const b334 Bool)
(declare-const b344 Bool)
(declare-const b414 Bool)
(declare-const b424 Bool)
(declare-const b434 Bool)
(declare-const b444 Bool)
(assert (not (or(and b121 b111)(and b131 b111)(and b141 b111)(and b211 b111)(and b311 b111)(and b411 b111))))
(assert (not (or(and b122 b112)(and b132 b112)(and b142 b112)(and b212 b112)(and b312 b112)(and b412 b112))))
(assert (not (or(and b123 b113)(and b133 b113)(and b143 b113)(and b213 b113)(and b313 b113)(and b413 b113))))
(assert (not (or(and b124 b114)(and b134 b114)(and b144 b114)(and b214 b114)(and b314 b114)(and b414 b114))))
(assert (not (or(and b111 b121)(and b131 b121)(and b141 b121)(and b221 b121)(and b321 b121)(and b421 b121))))
(assert (not (or(and b112 b122)(and b132 b122)(and b142 b122)(and b222 b122)(and b322 b122)(and b422 b122))))
(assert (not (or(and b113 b123)(and b133 b123)(and b143 b123)(and b223 b123)(and b323 b123)(and b423 b123))))
(assert (not (or(and b114 b124)(and b134 b124)(and b144 b124)(and b224 b124)(and b324 b124)(and b424 b124))))
(assert (not (or(and b111 b131)(and b121 b131)(and b141 b131)(and b231 b131)(and b331 b131)(and b431 b131))))
(assert (not (or(and b112 b132)(and b122 b132)(and b142 b132)(and b232 b132)(and b332 b132)(and b432 b132))))
(assert (not (or(and b113 b133)(and b123 b133)(and b143 b133)(and b233 b133)(and b333 b133)(and b433 b133))))
(assert (not (or(and b114 b134)(and b124 b134)(and b144 b134)(and b234 b134)(and b334 b134)(and b434 b134))))
(assert (not (or(and b121 b141)(and b131 b141)(and b111 b141)(and b241 b141)(and b341 b141)(and b441 b141))))
(assert (not (or(and b122 b142)(and b132 b142)(and b112 b142)(and b242 b142)(and b342 b142)(and b442 b142))))
(assert (not (or(and b123 b143)(and b133 b143)(and b113 b143)(and b243 b143)(and b343 b143)(and b443 b143))))
(assert (not (or(and b124 b144)(and b134 b144)(and b114 b144)(and b244 b144)(and b344 b144)(and b444 b144))))
(assert (not (or(and b221 b211)(and b231 b211)(and b241 b211)(and b111 b211)(and b311 b211)(and b411 b211))))
(assert (not (or(and b222 b212)(and b232 b212)(and b242 b212)(and b212 b212)(and b312 b212)(and b412 b212))))
(assert (not (or(and b223 b213)(and b233 b213)(and b243 b213)(and b213 b213)(and b313 b213)(and b413 b213))))
(assert (not (or(and b224 b214)(and b234 b214)(and b244 b214)(and b214 b214)(and b314 b214)(and b414 b214))))
(assert (not (or(and b221 b211)(and b231 b221)(and b241 b221)(and b121 b221)(and b321 b221)(and b421 b221))))
(assert (not (or(and b222 b212)(and b232 b222)(and b242 b222)(and b122 b222)(and b322 b222)(and b422 b222))))
(assert (not (or(and b223 b213)(and b233 b223)(and b243 b223)(and b123 b223)(and b323 b223)(and b423 b223))))
(assert (not (or(and b224 b214)(and b234 b224)(and b244 b224)(and b124 b224)(and b324 b224)(and b424 b224))))
(assert (not (or(and b231 b211)(and b231 b221)(and b241 b231)(and b131 b231)(and b331 b231)(and b431 b231))))
(assert (not (or(and b232 b212)(and b232 b222)(and b242 b232)(and b132 b232)(and b332 b232)(and b432 b232))))
(assert (not (or(and b233 b213)(and b233 b223)(and b243 b233)(and b133 b233)(and b333 b233)(and b433 b233))))
(assert (not (or(and b234 b214)(and b234 b224)(and b244 b234)(and b134 b234)(and b334 b234)(and b434 b234))))
(assert (not (or(and b241 b211)(and b241 b221)(and b241 b231)(and b141 b241)(and b341 b241)(and b441 b241))))
(assert (not (or(and b242 b212)(and b242 b222)(and b242 b232)(and b142 b242)(and b342 b242)(and b442 b242))))
(assert (not (or(and b243 b213)(and b243 b223)(and b243 b233)(and b143 b243)(and b343 b243)(and b443 b243))))
(assert (not (or(and b244 b214)(and b244 b224)(and b244 b234)(and b144 b244)(and b344 b244)(and b444 b244))))
(assert (not (or(and b321 b311)(and b331 b311)(and b341 b311)(and b311 b211)(and b311 b111)(and b411 b311))))
(assert (not (or(and b322 b312)(and b332 b312)(and b342 b312)(and b312 b112)(and b312 b112)(and b412 b312))))
(assert (not (or(and b323 b313)(and b333 b313)(and b343 b313)(and b313 b113)(and b313 b113)(and b413 b313))))
(assert (not (or(and b324 b314)(and b334 b314)(and b344 b314)(and b314 b114)(and b314 b114)(and b414 b314))))
(assert (not (or(and b321 b311)(and b331 b321)(and b341 b321)(and b321 b221)(and b321 b121)(and b421 b321))))
(assert (not (or(and b322 b312)(and b332 b322)(and b342 b322)(and b322 b222)(and b322 b122)(and b422 b322))))
(assert (not (or(and b323 b313)(and b333 b323)(and b343 b323)(and b323 b223)(and b323 b123)(and b423 b323))))
(assert (not (or(and b324 b314)(and b334 b324)(and b344 b324)(and b324 b224)(and b324 b124)(and b424 b324))))
(assert (not (or(and b331 b311)(and b331 b321)(and b341 b331)(and b331 b231)(and b331 b131)(and b431 b331))))
(assert (not (or(and b332 b312)(and b332 b322)(and b342 b332)(and b332 b232)(and b332 b132)(and b432 b332))))
(assert (not (or(and b333 b313)(and b333 b323)(and b343 b333)(and b333 b233)(and b333 b133)(and b433 b333))))
(assert (not (or(and b334 b314)(and b334 b324)(and b344 b334)(and b334 b234)(and b334 b134)(and b434 b334))))
(assert (not (or(and b341 b311)(and b341 b321)(and b341 b331)(and b341 b241)(and b341 b141)(and b441 b341))))
(assert (not (or(and b342 b312)(and b342 b322)(and b342 b332)(and b342 b242)(and b342 b142)(and b442 b342))))
(assert (not (or(and b343 b313)(and b343 b323)(and b343 b333)(and b343 b243)(and b343 b143)(and b443 b343))))
(assert (not (or(and b344 b314)(and b344 b324)(and b344 b334)(and b344 b244)(and b344 b144)(and b444 b344))))
(assert (not (or(and b421 b411)(and b431 b411)(and b441 b411)(and b411 b311)(and b411 b111)(and b411 b211))))
(assert (not (or(and b422 b412)(and b432 b412)(and b442 b412)(and b412 b312)(and b412 b112)(and b412 b212))))
(assert (not (or(and b423 b413)(and b433 b413)(and b443 b413)(and b413 b313)(and b413 b113)(and b413 b213))))
(assert (not (or(and b424 b414)(and b434 b414)(and b444 b414)(and b414 b314)(and b414 b114)(and b414 b214))))
(assert (not (or(and b421 b411)(and b431 b421)(and b441 b421)(and b421 b321)(and b421 b121)(and b421 b221))))
(assert (not (or(and b422 b412)(and b432 b422)(and b442 b422)(and b422 b322)(and b422 b122)(and b422 b222))))
(assert (not (or(and b423 b413)(and b433 b423)(and b443 b423)(and b423 b323)(and b423 b123)(and b423 b223))))
(assert (not (or(and b424 b414)(and b434 b424)(and b444 b424)(and b424 b324)(and b424 b124)(and b424 b224))))
(assert (not (or(and b431 b411)(and b431 b421)(and b441 b431)(and b431 b331)(and b431 b131)(and b431 b231))))
(assert (not (or(and b432 b412)(and b432 b422)(and b442 b432)(and b432 b332)(and b432 b132)(and b432 b232))))
(assert (not (or(and b433 b413)(and b433 b423)(and b443 b433)(and b433 b333)(and b433 b133)(and b433 b233))))
(assert (not (or(and b434 b414)(and b434 b424)(and b444 b434)(and b434 b334)(and b434 b134)(and b434 b234))))
(assert (not (or(and b441 b411)(and b441 b421)(and b441 b431)(and b441 b341)(and b431 b141)(and b431 b241))))
(assert (not (or(and b442 b412)(and b442 b422)(and b442 b432)(and b442 b342)(and b432 b142)(and b432 b242))))
(assert (not (or(and b443 b413)(and b443 b423)(and b443 b433)(and b443 b343)(and b433 b143)(and b433 b243))))
(assert (not (or(and b444 b414)(and b444 b424)(and b444 b434)(and b444 b344)(and b434 b144)(and b434 b244))))
(assert (and (or b111 b121 b131 b141) (or b211 b221 b231 b241) (or b311 b321 b331 b341) (or b411 b421 b431 b441)))
(assert (and (or b112 b122 b132 b142) (or b212 b222 b232 b242) (or b312 b322 b332 b342) (or b412 b422 b432 b442)))
(assert (and (or b113 b123 b133 b143) (or b213 b223 b233 b243) (or b313 b323 b333 b343) (or b413 b423 b433 b443)))
(assert (and (or b114 b124 b134 b144) (or b214 b224 b234 b244) (or b314 b324 b334 b344) (or b414 b424 b434 b444)))
(assert (or (and b111 (not b112) (not b113) (not b114)) (and b112 (not b111) (not b113) (not b114)) (and b113 (not b112) (not b111) (not b114)) (and b114 (not b112) (not b113) (not b111))))
(assert (or (and b121 (not b122) (not b123) (not b124)) (and b122 (not b121) (not b123) (not b124)) (and b123 (not b122) (not b121) (not b124)) (and b124 (not b122) (not b123) (not b121))))
(assert (or (and b131 (not b132) (not b133) (not b124)) (and b132 (not b131) (not b133) (not b134)) (and b133 (not b132) (not b131) (not b134)) (and b134 (not b132) (not b133) (not b131))))
(assert (or (and b141 (not b142) (not b143) (not b124)) (and b142 (not b141) (not b143) (not b144)) (and b143 (not b142) (not b141) (not b144)) (and b144 (not b142) (not b143) (not b141))))
(assert (or (and b211 (not b212) (not b213) (not b214)) (and b212 (not b211) (not b213) (not b214)) (and b213 (not b212) (not b211) (not b214)) (and b214 (not b212) (not b213) (not b211))))
(assert (or (and b221 (not b222) (not b223) (not b214)) (and b222 (not b221) (not b223) (not b224)) (and b223 (not b222) (not b221) (not b224)) (and b224 (not b222) (not b223) (not b221))))
(assert (or (and b231 (not b232) (not b233) (not b214)) (and b232 (not b231) (not b233) (not b234)) (and b233 (not b232) (not b231) (not b234)) (and b234 (not b232) (not b233) (not b231))))
(assert (or (and b241 (not b242) (not b243) (not b214)) (and b242 (not b241) (not b243) (not b244)) (and b243 (not b242) (not b241) (not b244)) (and b244 (not b242) (not b243) (not b241))))
(assert (or (and b311 (not b312) (not b313) (not b314)) (and b312 (not b311) (not b313) (not b314)) (and b313 (not b312) (not b311) (not b314)) (and b314 (not b312) (not b313) (not b311))))
(assert (or (and b321 (not b312) (not b323) (not b324)) (and b322 (not b321) (not b323) (not b324)) (and b323 (not b322) (not b321) (not b324)) (and b324 (not b322) (not b323) (not b321))))
(assert (or (and b331 (not b312) (not b333) (not b334)) (and b342 (not b331) (not b333) (not b334)) (and b333 (not b332) (not b331) (not b334)) (and b344 (not b332) (not b333) (not b331))))
(assert (or (and b341 (not b312) (not b343) (not b344)) (and b342 (not b341) (not b343) (not b344)) (and b343 (not b342) (not b341) (not b344)) (and b344 (not b342) (not b343) (not b341))))
(assert (or (and b411 (not b412) (not b413) (not b414)) (and b412 (not b411) (not b413) (not b414)) (and b413 (not b412) (not b411) (not b414)) (and b414 (not b412) (not b413) (not b411))))
(assert (or (and b421 (not b422) (not b423) (not b424)) (and b422 (not b421) (not b423) (not b424)) (and b423 (not b422) (not b421) (not b424)) (and b424 (not b422) (not b423) (not b421))))
(assert (or (and b431 (not b432) (not b433) (not b434)) (and b432 (not b431) (not b433) (not b434)) (and b433 (not b432) (not b431) (not b434)) (and b434 (not b432) (not b433) (not b431))))
(assert (or (and b441 (not b442) (not b443) (not b444)) (and b442 (not b441) (not b443) (not b444)) (and b443 (not b442) (not b441) (not b444)) (and b444 (not b442) (not b443) (not b441))))
(check-sat)
(get-model)