blob: df1867c634d597cffe9ae70434d4b9a8050b6424 (
plain)
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
|
(set-logic QF_UFLIAFS)
(set-info :status sat)
(declare-sort E 0)
(declare-fun A1 () (Set E))
(declare-fun A2 () (Set E))
(declare-fun A3 () (Set E))
(declare-fun A4 () (Set E))
(declare-fun A5 () (Set E))
(declare-fun A6 () (Set E))
(declare-fun A7 () (Set E))
(declare-fun A8 () (Set E))
(declare-fun A9 () (Set E))
(declare-fun A10 () (Set E))
(declare-fun A11 () (Set E))
(declare-fun A12 () (Set E))
(declare-fun A13 () (Set E))
(declare-fun A14 () (Set E))
(declare-fun A15 () (Set E))
(declare-fun A16 () (Set E))
(declare-fun A17 () (Set E))
(declare-fun A18 () (Set E))
(declare-fun A19 () (Set E))
(declare-fun A20 () (Set E))
(assert (and
(= (card A1) 1)
(= (card A2) 1)
(= (card A3) 1)
(= (card A4) 1)
(= (card A5) 1)
(= (card A6) 1)
(= (card A7) 1)
(= (card A8) 1)
(= (card A9) 1)
(= (card A10) 1)
(= (card A11) 1)
(= (card A12) 1)
(= (card A13) 1)
(= (card A14) 1)
(= (card A15) 1)
(= (card A16) 1)
(= (card A17) 1)
(= (card A18) 1)
(= (card A19) 1)
(= (card A20) 1)
))
(assert (= 20 (+ (card A1) (card A2) (card A3) (card A4) (card A5) (card A6) (card A7) (card A8) (card A9) (card A10) (card A11) (card A12) (card A13) (card A14) (card A15) (card A16) (card A17) (card A18) (card A19) (card A20))))
(check-sat)
|
