mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
546 lines
6.9 KiB
INI
546 lines
6.9 KiB
INI
c This Formular is generated by mcnf
|
|
c
|
|
c horn? no
|
|
c forced? no
|
|
c mixed sat? no
|
|
c clause length = 3
|
|
c
|
|
p cnf 125 538
|
|
60 1 102 0
|
|
-88 -21 -116 0
|
|
88 -101 15 0
|
|
-96 -120 -68 0
|
|
-3 -109 -23 0
|
|
-42 98 -68 0
|
|
57 -27 62 0
|
|
7 -91 -71 0
|
|
-16 63 81 0
|
|
37 49 -28 0
|
|
-25 72 -98 0
|
|
-39 98 -5 0
|
|
-31 -22 84 0
|
|
63 83 90 0
|
|
-62 78 -60 0
|
|
90 -36 62 0
|
|
41 -49 43 0
|
|
45 86 121 0
|
|
-84 111 -112 0
|
|
38 -104 57 0
|
|
91 25 57 0
|
|
-66 -68 -57 0
|
|
21 2 -81 0
|
|
39 -107 -94 0
|
|
-23 -119 -99 0
|
|
100 -86 112 0
|
|
-39 54 81 0
|
|
90 -58 -40 0
|
|
-29 112 45 0
|
|
-117 -34 -120 0
|
|
53 -86 -75 0
|
|
54 -30 117 0
|
|
-48 88 86 0
|
|
-25 36 20 0
|
|
-70 -25 64 0
|
|
53 -43 11 0
|
|
65 11 31 0
|
|
85 67 -117 0
|
|
-79 -54 -35 0
|
|
-5 67 -92 0
|
|
119 57 -125 0
|
|
7 125 -93 0
|
|
67 15 -54 0
|
|
-57 -13 11 0
|
|
-33 116 -74 0
|
|
-82 53 -11 0
|
|
38 -64 -69 0
|
|
118 -43 -13 0
|
|
5 -32 -85 0
|
|
-23 29 -63 0
|
|
-50 -109 60 0
|
|
-103 46 -72 0
|
|
101 65 84 0
|
|
26 -72 116 0
|
|
63 -97 -125 0
|
|
84 109 46 0
|
|
-22 26 -73 0
|
|
-39 109 -34 0
|
|
28 -32 -20 0
|
|
-80 11 60 0
|
|
-76 3 -42 0
|
|
-23 43 -116 0
|
|
-65 50 -108 0
|
|
-48 -75 -20 0
|
|
-30 47 103 0
|
|
-22 -77 25 0
|
|
29 -95 -88 0
|
|
-18 -5 -22 0
|
|
114 -26 -18 0
|
|
-100 -123 32 0
|
|
-99 108 109 0
|
|
44 -76 -25 0
|
|
104 -112 -95 0
|
|
-70 -100 -99 0
|
|
-72 83 65 0
|
|
-10 9 8 0
|
|
-48 51 -5 0
|
|
37 36 -86 0
|
|
79 -106 48 0
|
|
119 -14 113 0
|
|
-83 -125 31 0
|
|
21 -41 88 0
|
|
-124 25 -56 0
|
|
-33 109 73 0
|
|
-110 -30 29 0
|
|
120 46 19 0
|
|
62 32 52 0
|
|
-45 55 -64 0
|
|
67 47 -78 0
|
|
29 -112 -18 0
|
|
-76 -78 27 0
|
|
106 -40 70 0
|
|
71 -109 -56 0
|
|
103 25 -117 0
|
|
43 -68 104 0
|
|
-42 76 -15 0
|
|
106 25 -32 0
|
|
-52 2 80 0
|
|
53 114 -63 0
|
|
36 87 45 0
|
|
-77 64 120 0
|
|
-84 112 -64 0
|
|
87 -89 121 0
|
|
78 123 121 0
|
|
116 -78 125 0
|
|
-80 44 -85 0
|
|
113 -94 -78 0
|
|
45 -46 79 0
|
|
48 39 -22 0
|
|
-81 -44 -16 0
|
|
102 -34 26 0
|
|
-26 95 -4 0
|
|
93 -65 -9 0
|
|
-70 -28 7 0
|
|
30 -25 104 0
|
|
27 82 -91 0
|
|
-87 43 42 0
|
|
54 113 -2 0
|
|
31 -104 -9 0
|
|
-97 99 -103 0
|
|
-8 -46 40 0
|
|
-45 59 -100 0
|
|
22 78 108 0
|
|
5 -44 -120 0
|
|
-91 53 38 0
|
|
-26 -11 -102 0
|
|
-122 -28 7 0
|
|
-90 10 -108 0
|
|
-89 37 -40 0
|
|
22 -15 49 0
|
|
-116 108 62 0
|
|
40 44 71 0
|
|
77 104 -69 0
|
|
-56 -15 13 0
|
|
91 120 77 0
|
|
65 46 -16 0
|
|
-45 -52 -106 0
|
|
-50 98 -118 0
|
|
40 38 107 0
|
|
-100 6 120 0
|
|
54 -106 -44 0
|
|
-99 44 -87 0
|
|
14 67 -53 0
|
|
-101 -90 -114 0
|
|
-125 -75 -5 0
|
|
-23 117 45 0
|
|
47 -20 -81 0
|
|
88 123 -39 0
|
|
-91 105 54 0
|
|
-78 61 103 0
|
|
-22 78 -32 0
|
|
103 -64 -96 0
|
|
-30 35 -78 0
|
|
-31 -15 -62 0
|
|
-113 46 -59 0
|
|
5 -24 -66 0
|
|
-113 -67 -22 0
|
|
-39 -29 3 0
|
|
73 -3 67 0
|
|
-6 75 -81 0
|
|
-53 -44 -107 0
|
|
-77 68 13 0
|
|
-67 65 41 0
|
|
-122 2 -15 0
|
|
98 -17 -50 0
|
|
11 -8 117 0
|
|
78 30 -75 0
|
|
118 120 2 0
|
|
-58 52 28 0
|
|
94 78 54 0
|
|
33 41 -25 0
|
|
87 120 -17 0
|
|
-123 -38 -68 0
|
|
13 33 -43 0
|
|
-45 122 -57 0
|
|
116 -51 6 0
|
|
3 -36 -42 0
|
|
92 -69 -124 0
|
|
-25 -81 5 0
|
|
-47 41 29 0
|
|
-69 4 97 0
|
|
121 22 82 0
|
|
-123 7 98 0
|
|
-95 65 -121 0
|
|
7 54 32 0
|
|
82 101 -49 0
|
|
99 -45 89 0
|
|
84 -79 10 0
|
|
-96 44 -114 0
|
|
-83 25 -50 0
|
|
-34 -18 -58 0
|
|
-25 -45 -26 0
|
|
116 -59 60 0
|
|
50 86 -53 0
|
|
-35 -10 96 0
|
|
-41 -33 -48 0
|
|
-79 14 38 0
|
|
85 -118 71 0
|
|
-28 -43 -21 0
|
|
-27 -115 -82 0
|
|
-29 -114 -112 0
|
|
-70 41 -115 0
|
|
-119 -104 -109 0
|
|
125 -26 -19 0
|
|
93 8 88 0
|
|
-4 -33 -25 0
|
|
-92 54 27 0
|
|
73 -29 25 0
|
|
32 -93 47 0
|
|
-24 81 35 0
|
|
23 -7 72 0
|
|
35 88 109 0
|
|
107 116 47 0
|
|
-28 79 -108 0
|
|
102 28 51 0
|
|
-50 -37 61 0
|
|
52 119 -20 0
|
|
-53 36 -55 0
|
|
-115 70 55 0
|
|
-67 121 -87 0
|
|
-46 57 -12 0
|
|
39 105 90 0
|
|
122 67 -55 0
|
|
-28 31 41 0
|
|
-16 69 54 0
|
|
-78 -106 117 0
|
|
60 1 23 0
|
|
-43 -57 104 0
|
|
-69 -10 50 0
|
|
-43 -107 120 0
|
|
32 -36 -35 0
|
|
-67 -60 123 0
|
|
-1 -113 -105 0
|
|
41 -104 -49 0
|
|
67 52 94 0
|
|
-69 46 58 0
|
|
-33 105 -52 0
|
|
-124 64 -96 0
|
|
102 -77 -45 0
|
|
-124 42 -93 0
|
|
-24 98 -47 0
|
|
23 122 28 0
|
|
-18 123 107 0
|
|
-97 -110 -92 0
|
|
-120 -2 123 0
|
|
-76 -105 22 0
|
|
99 117 -36 0
|
|
-11 30 -92 0
|
|
39 -121 -110 0
|
|
-88 -111 72 0
|
|
9 23 -7 0
|
|
-70 -118 -93 0
|
|
76 -4 9 0
|
|
43 35 28 0
|
|
97 -3 -5 0
|
|
-70 97 -98 0
|
|
53 72 -110 0
|
|
125 3 -107 0
|
|
-40 -87 13 0
|
|
-87 85 56 0
|
|
41 73 -115 0
|
|
-5 -77 -63 0
|
|
-93 -97 118 0
|
|
-52 -18 -124 0
|
|
118 47 -72 0
|
|
67 -53 22 0
|
|
-47 70 -122 0
|
|
-100 -27 66 0
|
|
4 -27 61 0
|
|
114 85 -68 0
|
|
10 74 -7 0
|
|
-76 52 -17 0
|
|
-42 -11 -102 0
|
|
-25 -105 -104 0
|
|
107 96 30 0
|
|
4 -41 -111 0
|
|
-82 -22 -42 0
|
|
49 -11 -88 0
|
|
-102 -18 44 0
|
|
26 85 121 0
|
|
-92 13 67 0
|
|
-67 -104 35 0
|
|
61 125 15 0
|
|
88 -1 25 0
|
|
32 107 -87 0
|
|
-53 -2 109 0
|
|
7 21 110 0
|
|
45 -65 -62 0
|
|
-66 50 87 0
|
|
92 -87 24 0
|
|
25 41 61 0
|
|
-14 -41 34 0
|
|
-60 2 -102 0
|
|
82 -1 114 0
|
|
-85 -58 -5 0
|
|
-42 11 -33 0
|
|
116 31 -108 0
|
|
62 -89 66 0
|
|
-103 -41 -2 0
|
|
9 43 25 0
|
|
7 66 22 0
|
|
-107 33 -70 0
|
|
-30 119 62 0
|
|
-96 -9 61 0
|
|
-65 -108 -61 0
|
|
-100 4 -26 0
|
|
-35 -24 101 0
|
|
78 -18 25 0
|
|
-35 83 66 0
|
|
114 -119 23 0
|
|
9 58 -22 0
|
|
-102 -88 -89 0
|
|
109 20 -94 0
|
|
65 68 -38 0
|
|
-45 -26 86 0
|
|
-86 -83 100 0
|
|
47 94 116 0
|
|
87 29 -77 0
|
|
12 -103 -52 0
|
|
-16 -27 -115 0
|
|
-19 55 22 0
|
|
21 -84 107 0
|
|
-68 -56 19 0
|
|
122 70 55 0
|
|
62 79 -9 0
|
|
56 102 -94 0
|
|
-69 -98 -88 0
|
|
22 -122 44 0
|
|
-44 104 81 0
|
|
117 -86 85 0
|
|
73 -54 -109 0
|
|
-22 -45 95 0
|
|
98 20 33 0
|
|
-28 -104 119 0
|
|
-115 -69 -104 0
|
|
-81 17 30 0
|
|
62 79 51 0
|
|
-68 35 69 0
|
|
-115 79 108 0
|
|
-1 -51 -4 0
|
|
81 89 -111 0
|
|
-82 98 -43 0
|
|
56 -70 36 0
|
|
20 75 -23 0
|
|
-4 62 85 0
|
|
64 16 120 0
|
|
-42 -118 112 0
|
|
-52 -36 -91 0
|
|
3 -86 36 0
|
|
-107 -92 108 0
|
|
-98 -14 -60 0
|
|
-107 -106 -88 0
|
|
-115 -117 105 0
|
|
-41 -83 -6 0
|
|
-123 89 60 0
|
|
-24 -3 -23 0
|
|
54 77 66 0
|
|
-85 -34 -123 0
|
|
-109 -29 34 0
|
|
82 -104 105 0
|
|
26 -108 -11 0
|
|
-9 120 -57 0
|
|
-80 95 -10 0
|
|
28 17 27 0
|
|
78 -87 -110 0
|
|
-65 4 -52 0
|
|
-57 61 -113 0
|
|
89 93 -98 0
|
|
68 18 121 0
|
|
82 -110 113 0
|
|
78 92 -108 0
|
|
-85 -80 -88 0
|
|
37 -53 54 0
|
|
-104 35 -73 0
|
|
-103 121 80 0
|
|
20 -86 9 0
|
|
-103 74 -106 0
|
|
-26 -59 -122 0
|
|
-10 47 124 0
|
|
52 -124 34 0
|
|
47 -108 -3 0
|
|
-82 88 -66 0
|
|
8 54 -21 0
|
|
-93 -17 10 0
|
|
4 25 -29 0
|
|
-79 77 -99 0
|
|
73 89 -46 0
|
|
-101 34 1 0
|
|
-84 -5 -26 0
|
|
124 100 24 0
|
|
-19 91 5 0
|
|
-76 120 100 0
|
|
-68 -108 -35 0
|
|
77 63 -103 0
|
|
30 22 124 0
|
|
-76 124 -56 0
|
|
18 40 42 0
|
|
81 30 79 0
|
|
-102 70 79 0
|
|
5 -46 -53 0
|
|
-13 -76 -36 0
|
|
-98 -35 20 0
|
|
-67 -111 16 0
|
|
67 63 18 0
|
|
74 -42 87 0
|
|
-106 -116 -16 0
|
|
43 -22 -12 0
|
|
95 -88 90 0
|
|
3 19 -23 0
|
|
-97 -98 -26 0
|
|
-79 66 56 0
|
|
-88 -53 63 0
|
|
49 -51 -4 0
|
|
18 115 102 0
|
|
105 -109 -5 0
|
|
71 36 20 0
|
|
-43 -92 83 0
|
|
21 114 -90 0
|
|
-108 20 -66 0
|
|
-117 39 61 0
|
|
-76 -114 53 0
|
|
-125 32 -24 0
|
|
-121 32 -79 0
|
|
-36 -37 100 0
|
|
-53 -113 -72 0
|
|
6 59 -104 0
|
|
115 -28 125 0
|
|
103 -105 -42 0
|
|
-12 -100 8 0
|
|
-19 -3 -116 0
|
|
82 121 33 0
|
|
28 43 -88 0
|
|
-38 -34 -53 0
|
|
49 -101 92 0
|
|
60 -105 44 0
|
|
25 -27 -30 0
|
|
-117 115 125 0
|
|
-27 54 89 0
|
|
72 -57 -30 0
|
|
-80 -48 96 0
|
|
33 122 68 0
|
|
20 -44 19 0
|
|
75 -26 -90 0
|
|
-92 -51 28 0
|
|
-112 43 62 0
|
|
-124 74 -31 0
|
|
-96 30 2 0
|
|
-25 124 26 0
|
|
-85 4 56 0
|
|
-2 -113 -63 0
|
|
97 68 52 0
|
|
-86 -104 91 0
|
|
-88 -117 13 0
|
|
118 65 54 0
|
|
68 -53 -41 0
|
|
108 -88 54 0
|
|
96 50 41 0
|
|
-76 -100 -1 0
|
|
-14 80 -46 0
|
|
121 -71 25 0
|
|
-22 -59 -102 0
|
|
12 -63 117 0
|
|
62 76 -104 0
|
|
-42 -53 21 0
|
|
-59 116 94 0
|
|
-97 -49 -102 0
|
|
16 -11 7 0
|
|
-11 125 -82 0
|
|
-55 -104 48 0
|
|
-98 -124 32 0
|
|
-110 53 -108 0
|
|
31 18 117 0
|
|
-44 36 -55 0
|
|
120 79 94 0
|
|
-83 -1 -32 0
|
|
48 52 41 0
|
|
11 -44 -60 0
|
|
-57 -125 119 0
|
|
-102 119 -97 0
|
|
104 -118 -1 0
|
|
123 30 118 0
|
|
81 -70 50 0
|
|
-98 -4 5 0
|
|
-109 91 122 0
|
|
-80 15 24 0
|
|
22 -35 15 0
|
|
16 -39 -69 0
|
|
-3 -115 -79 0
|
|
78 -70 -79 0
|
|
-113 120 8 0
|
|
-89 -41 49 0
|
|
-123 116 57 0
|
|
-16 -23 32 0
|
|
51 -70 79 0
|
|
-114 90 -54 0
|
|
10 -121 -112 0
|
|
75 97 -79 0
|
|
-48 55 -122 0
|
|
89 -75 58 0
|
|
102 67 125 0
|
|
-101 72 28 0
|
|
50 -79 99 0
|
|
-102 -8 -67 0
|
|
86 -51 -40 0
|
|
53 -70 -59 0
|
|
-84 75 -68 0
|
|
-114 -88 -26 0
|
|
99 67 -118 0
|
|
6 -1 45 0
|
|
-72 43 -95 0
|
|
-83 91 -33 0
|
|
58 91 -4 0
|
|
118 123 107 0
|
|
-38 37 67 0
|
|
-119 2 -82 0
|
|
-53 84 -64 0
|
|
-64 -86 -33 0
|
|
56 98 -86 0
|
|
98 -43 -34 0
|
|
78 -118 -92 0
|
|
-8 -51 71 0
|
|
-32 40 45 0
|
|
-29 -117 -94 0
|
|
-38 39 -125 0
|
|
-30 -31 56 0
|
|
71 -119 73 0
|
|
-29 -118 -66 0
|
|
82 119 -76 0
|
|
17 97 110 0
|
|
106 77 53 0
|
|
58 -87 -33 0
|
|
-32 -7 -112 0
|
|
57 -37 71 0
|
|
-79 -105 101 0
|
|
86 103 -100 0
|
|
-53 -71 77 0
|
|
-78 -109 61 0
|
|
-16 13 53 0
|