blob: 816bd39c34c7c93b32c5aab9c46415f1e27663d5 (
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
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
|
(set-logic QF_UF)
(declare-fun a1 () Bool)
(declare-fun a2 () Bool)
(declare-fun a3 () Bool)
(declare-fun a4 () Bool)
(declare-fun a5 () Bool)
(declare-fun a6 () Bool)
(declare-fun a7 () Bool)
(declare-fun a8 () Bool)
(declare-fun a9 () Bool)
(declare-fun a10 () Bool)
(declare-fun a11 () Bool)
(declare-fun a12 () Bool)
(declare-fun a13 () Bool)
(declare-fun a14 () Bool)
(declare-fun a15 () Bool)
(declare-fun a16 () Bool)
(declare-fun a17 () Bool)
(declare-fun a18 () Bool)
(declare-fun a19 () Bool)
(declare-fun a20 () Bool)
(assert (and
(or a1 a2 a3 a4)
(or a5 a6 a7 a8)
(or a9 a10 a11 a12)
(or a13 a14 a15 a16)
(or a17 a18 a19 a20)
(or (not a1) (not a2))
(or (not a1) (not a3))
(or (not a1) (not a4))
(or (not a2) (not a3))
(or (not a2) (not a4))
(or (not a3) (not a4))
(or (not a5) (not a6))
(or (not a5) (not a7))
(or (not a5) (not a8))
(or (not a6) (not a7))
(or (not a6) (not a8))
(or (not a7) (not a8))
(or (not a9) (not a10))
(or (not a9) (not a11))
(or (not a9) (not a12))
(or (not a10) (not a11))
(or (not a10) (not a12))
(or (not a11) (not a12))
(or (not a13) (not a14))
(or (not a13) (not a15))
(or (not a13) (not a16))
(or (not a14) (not a15))
(or (not a14) (not a16))
(or (not a15) (not a16))
(or (not a17) (not a18))
(or (not a17) (not a19))
(or (not a17) (not a20))
(or (not a18) (not a19))
(or (not a18) (not a20))
(or (not a19) (not a20))
(or (not a1) (not a5))
(or (not a1) (not a9))
(or (not a1) (not a13))
(or (not a1) (not a17))
(or (not a5) (not a9))
(or (not a5) (not a13))
(or (not a5) (not a17))
(or (not a9) (not a13))
(or (not a9) (not a17))
(or (not a13) (not a17))
(or (not a2) (not a6))
(or (not a2) (not a10))
(or (not a2) (not a14))
(or (not a2) (not a18))
(or (not a6) (not a10))
(or (not a6) (not a14))
(or (not a6) (not a18))
(or (not a10) (not a14))
(or (not a10) (not a18))
(or (not a14) (not a18))
(or (not a3) (not a7))
(or (not a3) (not a11))
(or (not a3) (not a15))
(or (not a3) (not a19))
(or (not a7) (not a11))
(or (not a7) (not a15))
(or (not a7) (not a19))
(or (not a11) (not a15))
(or (not a11) (not a19))
(or (not a15) (not a19))
(or (not a4) (not a8))
(or (not a4) (not a12))
(or (not a4) (not a16))
(or (not a4) (not a20))
(or (not a8) (not a12))
(or (not a8) (not a16))
(or (not a8) (not a20))
(or (not a12) (not a16))
(or (not a12) (not a20))
(or (not a16) (not a20))))
(check-sat)
(exit)
|
