mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
653 lines
8.5 KiB
INI
653 lines
8.5 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 150 645
|
|
28 -128 -147 0
|
|
-99 115 -25 0
|
|
122 -74 149 0
|
|
72 -29 -132 0
|
|
-95 -138 -132 0
|
|
-110 139 87 0
|
|
-101 122 38 0
|
|
-94 40 127 0
|
|
-113 -126 82 0
|
|
42 -89 -30 0
|
|
132 -40 130 0
|
|
141 97 124 0
|
|
82 -15 -81 0
|
|
112 70 -109 0
|
|
-85 -55 -41 0
|
|
-105 -59 10 0
|
|
87 -118 103 0
|
|
101 -78 -39 0
|
|
-14 -97 -66 0
|
|
-75 74 134 0
|
|
-86 -143 -121 0
|
|
102 13 65 0
|
|
-79 23 -138 0
|
|
113 67 70 0
|
|
-107 -114 133 0
|
|
-2 -15 -13 0
|
|
-69 -63 102 0
|
|
44 45 -47 0
|
|
5 124 16 0
|
|
-133 109 -19 0
|
|
-135 51 112 0
|
|
86 92 -135 0
|
|
-62 -118 146 0
|
|
57 -3 -131 0
|
|
-127 59 -91 0
|
|
92 8 40 0
|
|
-126 -90 -4 0
|
|
61 -39 45 0
|
|
63 -52 -47 0
|
|
-26 -100 32 0
|
|
-105 -37 63 0
|
|
56 66 -7 0
|
|
136 -87 23 0
|
|
-75 -56 70 0
|
|
-93 -125 -144 0
|
|
-29 45 125 0
|
|
8 94 129 0
|
|
149 139 -91 0
|
|
-40 93 -138 0
|
|
-3 -6 61 0
|
|
85 -9 -45 0
|
|
-122 -108 26 0
|
|
105 -122 17 0
|
|
-127 -33 129 0
|
|
-52 -145 48 0
|
|
112 -75 -36 0
|
|
-89 104 93 0
|
|
143 9 37 0
|
|
44 -30 62 0
|
|
-64 46 47 0
|
|
137 -119 -112 0
|
|
-7 63 -48 0
|
|
14 20 111 0
|
|
-79 -72 44 0
|
|
-43 -7 -84 0
|
|
-127 -104 59 0
|
|
-31 -133 -97 0
|
|
-30 -96 143 0
|
|
3 75 93 0
|
|
84 107 42 0
|
|
107 -22 -112 0
|
|
-49 140 70 0
|
|
-118 -97 -96 0
|
|
131 -89 -15 0
|
|
109 -67 -36 0
|
|
-9 40 104 0
|
|
-58 -103 -52 0
|
|
127 65 73 0
|
|
-6 89 -28 0
|
|
37 139 143 0
|
|
46 111 -28 0
|
|
73 117 -142 0
|
|
-26 129 25 0
|
|
-111 -10 114 0
|
|
-95 125 -24 0
|
|
11 57 55 0
|
|
-127 145 -37 0
|
|
-78 70 -79 0
|
|
-128 92 -91 0
|
|
-61 5 -149 0
|
|
7 -73 149 0
|
|
-21 139 104 0
|
|
67 -102 132 0
|
|
-146 96 7 0
|
|
61 -122 41 0
|
|
3 126 -130 0
|
|
68 40 -113 0
|
|
75 -95 96 0
|
|
-122 109 10 0
|
|
14 106 43 0
|
|
-112 17 137 0
|
|
65 -86 46 0
|
|
-21 -32 -19 0
|
|
30 60 -91 0
|
|
110 -51 -91 0
|
|
14 67 -122 0
|
|
6 -72 74 0
|
|
-126 -119 62 0
|
|
127 114 -60 0
|
|
-53 -113 -147 0
|
|
98 -129 19 0
|
|
-59 135 98 0
|
|
13 12 -15 0
|
|
-75 132 64 0
|
|
-81 -101 -29 0
|
|
29 -42 -123 0
|
|
74 20 -87 0
|
|
-68 -15 -135 0
|
|
-32 -14 121 0
|
|
11 79 120 0
|
|
33 -35 105 0
|
|
107 6 -85 0
|
|
-16 96 101 0
|
|
-140 60 54 0
|
|
-130 16 -131 0
|
|
-13 -87 -21 0
|
|
-33 -48 -109 0
|
|
54 -106 -82 0
|
|
-45 95 19 0
|
|
-1 -34 -39 0
|
|
-117 -146 -29 0
|
|
90 -146 -17 0
|
|
-34 18 63 0
|
|
-74 66 113 0
|
|
116 -14 51 0
|
|
-96 -111 -30 0
|
|
-94 -37 -139 0
|
|
-67 -119 -130 0
|
|
-6 56 -110 0
|
|
63 -83 27 0
|
|
-12 -38 -89 0
|
|
79 -23 70 0
|
|
-106 75 -140 0
|
|
83 -13 -35 0
|
|
19 -24 -37 0
|
|
105 -101 -1 0
|
|
125 15 -8 0
|
|
65 -9 40 0
|
|
33 26 60 0
|
|
20 -86 -44 0
|
|
19 -86 84 0
|
|
5 -103 -34 0
|
|
127 -61 94 0
|
|
63 -146 -122 0
|
|
-82 67 36 0
|
|
6 -133 -101 0
|
|
30 64 -3 0
|
|
20 -121 33 0
|
|
98 -79 -132 0
|
|
-62 73 -29 0
|
|
115 -66 58 0
|
|
36 121 -81 0
|
|
127 32 111 0
|
|
79 -16 -124 0
|
|
23 -147 -36 0
|
|
126 -58 -11 0
|
|
-51 9 -72 0
|
|
-122 24 117 0
|
|
-127 112 -49 0
|
|
-64 -45 130 0
|
|
46 -72 -131 0
|
|
-7 -5 113 0
|
|
-13 108 34 0
|
|
12 -18 29 0
|
|
43 -31 96 0
|
|
-95 -27 113 0
|
|
-29 89 71 0
|
|
1 30 14 0
|
|
-100 -19 71 0
|
|
-29 -122 69 0
|
|
-15 89 76 0
|
|
43 -97 114 0
|
|
35 -143 -33 0
|
|
-19 7 147 0
|
|
69 114 149 0
|
|
2 -89 140 0
|
|
-58 43 146 0
|
|
126 -148 -47 0
|
|
63 -16 139 0
|
|
-83 -33 147 0
|
|
-94 -96 98 0
|
|
-117 -19 -87 0
|
|
127 -86 -90 0
|
|
-5 -42 103 0
|
|
27 -33 99 0
|
|
-32 -58 -139 0
|
|
-23 108 -118 0
|
|
-51 46 -13 0
|
|
77 73 -35 0
|
|
96 -93 -18 0
|
|
-87 -147 39 0
|
|
-25 -149 138 0
|
|
-70 -8 103 0
|
|
-76 -75 94 0
|
|
-95 -50 102 0
|
|
-93 -30 63 0
|
|
-12 -131 -36 0
|
|
57 -43 -1 0
|
|
-31 51 74 0
|
|
-133 105 77 0
|
|
150 -9 50 0
|
|
-100 2 -136 0
|
|
-128 58 -2 0
|
|
128 98 28 0
|
|
78 -53 144 0
|
|
25 136 69 0
|
|
80 -147 60 0
|
|
23 -109 118 0
|
|
1 -65 132 0
|
|
67 43 -106 0
|
|
119 -71 -78 0
|
|
95 -74 -121 0
|
|
65 11 -61 0
|
|
67 35 62 0
|
|
102 129 -69 0
|
|
-149 8 35 0
|
|
50 -140 -103 0
|
|
122 -58 -101 0
|
|
-30 6 -20 0
|
|
118 6 -61 0
|
|
2 -60 -106 0
|
|
66 36 -140 0
|
|
108 28 -41 0
|
|
44 89 136 0
|
|
144 149 -46 0
|
|
-3 36 17 0
|
|
-108 138 -38 0
|
|
-80 113 121 0
|
|
-99 -65 -119 0
|
|
125 121 147 0
|
|
-127 -27 -68 0
|
|
146 93 -127 0
|
|
-126 -119 -95 0
|
|
-126 -37 31 0
|
|
-93 -95 128 0
|
|
121 -91 29 0
|
|
27 -79 -106 0
|
|
-135 87 113 0
|
|
-46 -7 86 0
|
|
83 -43 -1 0
|
|
-63 -103 -55 0
|
|
104 17 67 0
|
|
54 -4 -114 0
|
|
65 129 -3 0
|
|
57 138 -146 0
|
|
-23 110 80 0
|
|
-65 5 -85 0
|
|
-8 -117 109 0
|
|
-116 47 20 0
|
|
71 105 -62 0
|
|
-43 -34 -69 0
|
|
-41 25 124 0
|
|
80 -13 -4 0
|
|
-80 100 -33 0
|
|
-23 138 35 0
|
|
-43 96 81 0
|
|
80 -109 66 0
|
|
-91 14 84 0
|
|
-81 -131 -17 0
|
|
-44 103 -71 0
|
|
125 79 -70 0
|
|
96 120 -12 0
|
|
114 -43 -17 0
|
|
-139 76 100 0
|
|
145 -107 -104 0
|
|
-48 -72 -146 0
|
|
48 -81 -78 0
|
|
143 -67 -1 0
|
|
94 113 20 0
|
|
77 -59 -131 0
|
|
-107 -30 46 0
|
|
85 -30 88 0
|
|
-120 -82 -108 0
|
|
-65 -35 -45 0
|
|
-108 5 -18 0
|
|
-63 -141 29 0
|
|
115 27 -39 0
|
|
92 -9 60 0
|
|
132 -43 -36 0
|
|
135 84 118 0
|
|
3 85 -143 0
|
|
-41 7 112 0
|
|
-58 150 -10 0
|
|
119 31 30 0
|
|
-118 41 -90 0
|
|
-87 -46 80 0
|
|
118 95 -125 0
|
|
105 3 -134 0
|
|
40 -82 2 0
|
|
-11 29 96 0
|
|
-33 118 103 0
|
|
-125 11 -136 0
|
|
75 -13 141 0
|
|
30 125 -124 0
|
|
-38 -29 140 0
|
|
-40 -7 29 0
|
|
34 93 -83 0
|
|
-7 117 -4 0
|
|
39 -55 -62 0
|
|
-124 -122 -108 0
|
|
25 -145 88 0
|
|
125 21 149 0
|
|
49 46 8 0
|
|
140 -82 87 0
|
|
-130 68 -143 0
|
|
-19 -56 -92 0
|
|
12 -84 -99 0
|
|
52 -40 -34 0
|
|
91 -82 -8 0
|
|
48 112 19 0
|
|
-137 68 106 0
|
|
-7 36 -147 0
|
|
-94 97 -28 0
|
|
54 -97 51 0
|
|
12 21 144 0
|
|
81 -47 -110 0
|
|
-99 -132 18 0
|
|
-84 31 11 0
|
|
-81 -61 -112 0
|
|
13 134 106 0
|
|
49 -95 63 0
|
|
140 79 -19 0
|
|
-71 108 -137 0
|
|
97 -148 55 0
|
|
-144 -141 10 0
|
|
115 45 -118 0
|
|
-65 42 26 0
|
|
40 121 7 0
|
|
20 148 73 0
|
|
-100 -49 41 0
|
|
-133 -112 -83 0
|
|
47 -53 -26 0
|
|
-122 25 -46 0
|
|
-53 -70 -94 0
|
|
26 93 48 0
|
|
104 -34 -7 0
|
|
20 -30 47 0
|
|
122 74 -57 0
|
|
113 -105 27 0
|
|
-56 105 112 0
|
|
148 126 46 0
|
|
149 -32 59 0
|
|
-78 49 -83 0
|
|
-91 -28 89 0
|
|
-136 -139 -123 0
|
|
110 -90 -120 0
|
|
-35 -92 -12 0
|
|
103 64 137 0
|
|
-20 -139 79 0
|
|
-126 92 -2 0
|
|
93 148 -34 0
|
|
43 -38 69 0
|
|
-144 -83 120 0
|
|
-32 -137 -6 0
|
|
-123 71 -53 0
|
|
-68 112 -89 0
|
|
-78 -67 -130 0
|
|
52 -115 43 0
|
|
38 -127 -147 0
|
|
4 60 12 0
|
|
-147 102 142 0
|
|
28 -131 82 0
|
|
118 28 -18 0
|
|
21 -86 89 0
|
|
-108 132 -85 0
|
|
-149 -35 -70 0
|
|
-5 147 -103 0
|
|
140 -122 107 0
|
|
119 2 91 0
|
|
82 -127 -51 0
|
|
135 -94 -123 0
|
|
-27 88 -89 0
|
|
58 14 64 0
|
|
-19 140 47 0
|
|
-28 -129 -42 0
|
|
-16 129 80 0
|
|
80 59 -101 0
|
|
111 -96 139 0
|
|
-69 -128 149 0
|
|
30 114 24 0
|
|
-57 56 146 0
|
|
-149 -124 -87 0
|
|
74 -102 70 0
|
|
72 44 -7 0
|
|
-116 -38 -56 0
|
|
6 16 2 0
|
|
-30 -1 19 0
|
|
92 -23 -113 0
|
|
41 -7 -131 0
|
|
139 43 -27 0
|
|
-140 38 1 0
|
|
37 69 -3 0
|
|
67 -127 125 0
|
|
-116 28 -67 0
|
|
-86 -63 37 0
|
|
-97 -105 -98 0
|
|
124 -62 102 0
|
|
-96 74 -28 0
|
|
90 -5 -37 0
|
|
77 -35 84 0
|
|
129 57 -128 0
|
|
41 112 -29 0
|
|
-16 134 110 0
|
|
-80 -135 52 0
|
|
88 -75 84 0
|
|
51 86 -92 0
|
|
-104 43 133 0
|
|
-127 147 25 0
|
|
46 26 123 0
|
|
-100 98 -106 0
|
|
20 -141 -84 0
|
|
-2 -35 30 0
|
|
48 -124 -39 0
|
|
-144 -136 -105 0
|
|
-139 97 -76 0
|
|
86 -87 -121 0
|
|
-95 -135 -149 0
|
|
16 -17 119 0
|
|
-134 82 44 0
|
|
-66 -37 139 0
|
|
-122 -67 -141 0
|
|
56 31 -109 0
|
|
49 21 94 0
|
|
-75 -58 114 0
|
|
-10 61 48 0
|
|
53 -24 96 0
|
|
-18 -22 63 0
|
|
-54 -125 88 0
|
|
-30 66 69 0
|
|
4 45 125 0
|
|
81 -96 51 0
|
|
-58 -6 -37 0
|
|
-38 37 -87 0
|
|
136 63 144 0
|
|
-119 -60 -73 0
|
|
121 42 60 0
|
|
36 -126 54 0
|
|
-35 -133 -73 0
|
|
48 -93 19 0
|
|
-69 115 -133 0
|
|
106 28 135 0
|
|
-63 84 -28 0
|
|
-3 41 106 0
|
|
31 -59 5 0
|
|
-123 18 116 0
|
|
49 -114 -52 0
|
|
-86 41 33 0
|
|
85 -11 -79 0
|
|
-103 117 -148 0
|
|
107 -139 -115 0
|
|
-96 143 87 0
|
|
-96 111 -106 0
|
|
-18 9 124 0
|
|
35 -1 25 0
|
|
-129 -64 -28 0
|
|
67 -81 -114 0
|
|
67 24 101 0
|
|
-136 -20 -32 0
|
|
17 150 81 0
|
|
-81 -11 -101 0
|
|
81 20 -17 0
|
|
-33 -89 -118 0
|
|
7 97 -139 0
|
|
119 -71 -103 0
|
|
87 43 -145 0
|
|
-123 -82 -118 0
|
|
83 -9 79 0
|
|
20 149 137 0
|
|
111 6 112 0
|
|
47 142 -117 0
|
|
-140 -1 50 0
|
|
98 -72 35 0
|
|
67 -142 25 0
|
|
93 110 -67 0
|
|
-128 -70 -114 0
|
|
-62 100 -142 0
|
|
138 5 53 0
|
|
47 -97 16 0
|
|
133 -92 -125 0
|
|
-22 123 66 0
|
|
-126 -128 127 0
|
|
99 -77 39 0
|
|
26 145 16 0
|
|
57 -48 -107 0
|
|
-28 -118 -75 0
|
|
-120 78 118 0
|
|
130 -144 -133 0
|
|
-87 20 -75 0
|
|
117 -118 -37 0
|
|
-25 -26 102 0
|
|
89 88 132 0
|
|
-114 14 21 0
|
|
-27 118 -35 0
|
|
-91 -36 64 0
|
|
112 -133 87 0
|
|
-116 -20 143 0
|
|
-124 -40 41 0
|
|
9 -13 -40 0
|
|
140 55 -146 0
|
|
115 143 86 0
|
|
-106 -21 -36 0
|
|
125 -91 -1 0
|
|
-87 -94 -150 0
|
|
-86 126 18 0
|
|
-35 144 -43 0
|
|
136 -150 -119 0
|
|
-133 -72 -27 0
|
|
-121 -23 54 0
|
|
-85 84 17 0
|
|
2 49 -39 0
|
|
-143 5 82 0
|
|
47 -9 100 0
|
|
-34 -114 57 0
|
|
-128 -19 139 0
|
|
-40 123 52 0
|
|
-10 -9 -74 0
|
|
119 -15 -109 0
|
|
103 122 -64 0
|
|
64 37 -16 0
|
|
-56 -70 -109 0
|
|
-27 -7 -133 0
|
|
51 -66 117 0
|
|
109 -86 -26 0
|
|
20 8 122 0
|
|
-22 116 72 0
|
|
-105 100 76 0
|
|
40 -101 89 0
|
|
-61 -67 -7 0
|
|
-21 109 -142 0
|
|
-17 135 -65 0
|
|
101 7 -60 0
|
|
-77 -7 -22 0
|
|
-143 -32 99 0
|
|
-100 80 7 0
|
|
-84 -90 10 0
|
|
133 37 -74 0
|
|
-126 -1 -137 0
|
|
89 77 -133 0
|
|
-87 105 -33 0
|
|
-119 -129 -46 0
|
|
-45 110 -18 0
|
|
-98 -128 93 0
|
|
35 -64 -103 0
|
|
121 -37 -63 0
|
|
109 -98 86 0
|
|
136 -121 23 0
|
|
96 -35 -3 0
|
|
64 3 -40 0
|
|
124 -141 28 0
|
|
-143 -102 105 0
|
|
141 -93 -1 0
|
|
38 -41 -123 0
|
|
17 142 -94 0
|
|
47 132 -104 0
|
|
80 -10 49 0
|
|
65 -80 97 0
|
|
-3 130 83 0
|
|
66 -36 3 0
|
|
-124 139 141 0
|
|
24 142 -18 0
|
|
77 91 -36 0
|
|
-66 -7 -108 0
|
|
10 48 -13 0
|
|
22 -31 93 0
|
|
21 132 146 0
|
|
144 132 -112 0
|
|
-7 71 -123 0
|
|
-92 -78 3 0
|
|
60 -111 91 0
|
|
6 143 -31 0
|
|
-23 24 67 0
|
|
100 60 142 0
|
|
27 117 -137 0
|
|
90 -130 36 0
|
|
-80 -138 1 0
|
|
-46 -12 -54 0
|
|
34 94 17 0
|
|
84 42 -8 0
|
|
146 10 58 0
|
|
39 -120 27 0
|
|
-70 -125 27 0
|
|
-80 -120 -115 0
|
|
-138 -79 -22 0
|
|
-73 145 -103 0
|
|
20 -65 112 0
|
|
-63 -23 -16 0
|
|
-111 76 72 0
|
|
-56 11 -145 0
|
|
-19 79 137 0
|
|
114 -79 77 0
|
|
-116 -39 53 0
|
|
83 89 -123 0
|
|
72 -69 6 0
|
|
58 -15 -89 0
|
|
-58 99 76 0
|
|
14 -139 90 0
|
|
-114 53 6 0
|
|
-81 128 -88 0
|
|
-97 -102 36 0
|
|
53 31 109 0
|
|
-50 42 100 0
|
|
79 -63 23 0
|
|
96 -98 129 0
|
|
129 -93 -9 0
|
|
46 141 121 0
|
|
-14 78 -65 0
|
|
130 -122 -139 0
|
|
43 -82 57 0
|
|
-84 -91 -140 0
|
|
32 150 -69 0
|
|
-26 -17 23 0
|
|
16 -110 37 0
|
|
113 5 104 0
|
|
66 110 -8 0
|
|
133 -83 -111 0
|
|
146 109 -132 0
|
|
-84 64 72 0
|
|
-143 31 38 0
|
|
13 115 23 0
|
|
-132 2 -6 0
|
|
57 49 -48 0
|
|
149 -1 -11 0
|
|
-103 114 109 0
|
|
-53 -72 -121 0
|
|
149 74 142 0
|
|
-93 73 -141 0
|
|
109 -10 98 0
|
|
-131 94 -134 0
|
|
-24 75 -111 0
|
|
-98 -90 -93 0
|
|
44 -28 -80 0
|
|
122 -96 -100 0
|
|
-94 -105 24 0
|
|
68 99 -101 0
|
|
130 -145 57 0
|