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
|
|
69 -63 57 0
|
|
24 72 -123 0
|
|
-78 28 -114 0
|
|
-76 -93 -56 0
|
|
46 -60 4 0
|
|
-8 -46 79 0
|
|
-80 123 117 0
|
|
67 108 -38 0
|
|
-48 -5 60 0
|
|
-73 -38 -103 0
|
|
93 83 -125 0
|
|
-92 101 -96 0
|
|
92 119 108 0
|
|
96 -97 41 0
|
|
74 -23 71 0
|
|
7 -66 -103 0
|
|
-104 78 99 0
|
|
74 2 -20 0
|
|
92 102 -41 0
|
|
-41 81 -13 0
|
|
-6 14 52 0
|
|
-107 -124 116 0
|
|
106 -21 27 0
|
|
-70 44 10 0
|
|
-100 -92 -97 0
|
|
98 -83 118 0
|
|
62 48 -10 0
|
|
-77 -109 103 0
|
|
11 53 98 0
|
|
37 -12 -115 0
|
|
-112 -96 -24 0
|
|
-116 -56 13 0
|
|
82 58 -123 0
|
|
-112 -47 -35 0
|
|
-107 -104 -84 0
|
|
38 -99 52 0
|
|
27 -68 -101 0
|
|
54 -24 15 0
|
|
-33 69 98 0
|
|
-14 -10 19 0
|
|
-54 -19 103 0
|
|
27 107 -122 0
|
|
-85 74 88 0
|
|
-25 -33 113 0
|
|
38 -113 26 0
|
|
60 -14 -26 0
|
|
-92 20 -88 0
|
|
-28 -106 57 0
|
|
35 -105 -90 0
|
|
-38 -14 52 0
|
|
-70 4 25 0
|
|
76 -8 38 0
|
|
-20 -124 -41 0
|
|
-9 23 -100 0
|
|
-36 83 91 0
|
|
-98 91 -39 0
|
|
15 11 87 0
|
|
112 68 56 0
|
|
-23 -28 -67 0
|
|
74 -36 -69 0
|
|
-75 -95 -55 0
|
|
67 107 1 0
|
|
86 21 118 0
|
|
61 -71 39 0
|
|
114 17 -74 0
|
|
-22 -5 40 0
|
|
-67 -59 113 0
|
|
-117 -48 -42 0
|
|
120 125 -35 0
|
|
72 116 119 0
|
|
91 69 55 0
|
|
-12 87 -106 0
|
|
21 20 114 0
|
|
27 124 52 0
|
|
38 -104 -44 0
|
|
80 -89 35 0
|
|
56 -105 16 0
|
|
-103 125 -64 0
|
|
-19 88 -65 0
|
|
124 -61 -75 0
|
|
8 47 36 0
|
|
-97 111 -109 0
|
|
-31 -124 86 0
|
|
-36 108 109 0
|
|
73 -52 67 0
|
|
95 102 79 0
|
|
-8 -115 120 0
|
|
78 -7 -14 0
|
|
61 -12 85 0
|
|
-52 -60 65 0
|
|
-27 51 9 0
|
|
-115 63 -16 0
|
|
124 7 -123 0
|
|
-115 106 -110 0
|
|
88 -77 -31 0
|
|
-60 -96 -38 0
|
|
-95 65 -29 0
|
|
-102 47 89 0
|
|
73 -49 114 0
|
|
29 -87 90 0
|
|
-47 -5 84 0
|
|
-84 -19 79 0
|
|
45 114 125 0
|
|
93 -97 121 0
|
|
-53 56 100 0
|
|
-34 -91 -13 0
|
|
-42 -38 111 0
|
|
31 26 -40 0
|
|
38 13 58 0
|
|
43 -89 84 0
|
|
26 -110 92 0
|
|
-5 18 -84 0
|
|
-41 -44 91 0
|
|
-43 112 23 0
|
|
-3 -63 -23 0
|
|
88 105 84 0
|
|
101 22 -78 0
|
|
-124 52 -10 0
|
|
-99 49 -70 0
|
|
-55 -27 77 0
|
|
76 -86 -9 0
|
|
105 125 -20 0
|
|
-37 -62 -119 0
|
|
-99 118 -22 0
|
|
-23 44 -12 0
|
|
25 -107 79 0
|
|
-101 92 -57 0
|
|
-105 42 -4 0
|
|
-50 -15 -65 0
|
|
-57 -7 125 0
|
|
62 6 -12 0
|
|
72 13 -90 0
|
|
-70 -112 12 0
|
|
-21 -10 68 0
|
|
41 -13 59 0
|
|
-70 17 -45 0
|
|
80 -104 -96 0
|
|
14 -52 90 0
|
|
78 -20 60 0
|
|
72 21 -28 0
|
|
-44 -5 1 0
|
|
46 -41 -11 0
|
|
-119 -99 44 0
|
|
-8 -75 63 0
|
|
-83 42 -63 0
|
|
-95 91 -2 0
|
|
3 -99 -4 0
|
|
5 -108 62 0
|
|
91 73 -9 0
|
|
71 -98 -20 0
|
|
5 53 -32 0
|
|
-95 25 60 0
|
|
-62 -43 -31 0
|
|
-57 44 65 0
|
|
31 -32 64 0
|
|
-43 -37 49 0
|
|
90 -57 116 0
|
|
45 -11 -50 0
|
|
67 -25 -46 0
|
|
-57 -116 27 0
|
|
12 -24 -68 0
|
|
-78 54 -121 0
|
|
121 -101 -111 0
|
|
-25 -53 -117 0
|
|
34 -11 66 0
|
|
92 117 70 0
|
|
-99 -5 86 0
|
|
70 -69 -117 0
|
|
23 -13 -30 0
|
|
90 117 -120 0
|
|
77 20 92 0
|
|
54 -28 -24 0
|
|
31 -67 40 0
|
|
124 19 -41 0
|
|
12 123 116 0
|
|
-107 105 -62 0
|
|
-92 -55 18 0
|
|
87 -100 -80 0
|
|
-30 119 96 0
|
|
68 33 1 0
|
|
101 -21 9 0
|
|
28 61 65 0
|
|
58 13 -109 0
|
|
90 -44 -98 0
|
|
-64 -56 -27 0
|
|
-94 89 87 0
|
|
113 -28 116 0
|
|
62 6 -54 0
|
|
-23 108 -111 0
|
|
114 106 29 0
|
|
82 -13 -105 0
|
|
-98 103 -8 0
|
|
5 92 -85 0
|
|
-125 34 86 0
|
|
-84 18 108 0
|
|
-3 114 41 0
|
|
-87 -4 8 0
|
|
49 97 4 0
|
|
-112 29 -48 0
|
|
75 -97 94 0
|
|
-84 -85 115 0
|
|
30 -28 -25 0
|
|
-75 46 -88 0
|
|
94 -42 20 0
|
|
93 -63 -4 0
|
|
63 -78 -47 0
|
|
-74 106 16 0
|
|
91 92 -58 0
|
|
-45 14 28 0
|
|
-97 123 -78 0
|
|
-62 121 -24 0
|
|
-96 -122 -81 0
|
|
122 -60 -65 0
|
|
-41 -33 125 0
|
|
85 69 -26 0
|
|
109 -106 80 0
|
|
-108 59 -124 0
|
|
-37 -42 29 0
|
|
-87 -12 50 0
|
|
114 -40 90 0
|
|
99 -61 -115 0
|
|
56 -51 12 0
|
|
23 25 -97 0
|
|
-67 88 78 0
|
|
-13 37 73 0
|
|
-111 -25 85 0
|
|
-52 8 -78 0
|
|
-119 84 -92 0
|
|
-32 -76 -55 0
|
|
-18 79 -14 0
|
|
-114 42 90 0
|
|
101 68 -50 0
|
|
-121 -125 -69 0
|
|
-55 -122 -28 0
|
|
-87 -123 -48 0
|
|
41 76 21 0
|
|
-47 124 -104 0
|
|
82 47 -110 0
|
|
103 63 71 0
|
|
99 -9 48 0
|
|
125 25 -86 0
|
|
56 77 108 0
|
|
20 5 -81 0
|
|
78 7 -28 0
|
|
-74 110 -83 0
|
|
-6 5 -91 0
|
|
75 -81 -71 0
|
|
91 9 122 0
|
|
11 -91 33 0
|
|
-113 62 29 0
|
|
-11 63 -39 0
|
|
95 104 19 0
|
|
33 1 17 0
|
|
-56 -58 -120 0
|
|
8 83 -44 0
|
|
-69 38 -39 0
|
|
46 -108 -64 0
|
|
-56 81 -89 0
|
|
-16 60 -113 0
|
|
112 -14 -22 0
|
|
-52 -27 -73 0
|
|
-48 -15 57 0
|
|
-2 50 -93 0
|
|
-103 111 73 0
|
|
-69 2 55 0
|
|
56 68 71 0
|
|
122 55 54 0
|
|
57 -2 -73 0
|
|
109 -67 -56 0
|
|
91 1 -28 0
|
|
-111 -84 17 0
|
|
110 21 -38 0
|
|
-24 -80 -119 0
|
|
-53 62 33 0
|
|
-42 -61 -33 0
|
|
-83 35 120 0
|
|
-56 21 35 0
|
|
64 66 -122 0
|
|
-35 105 -11 0
|
|
-72 -97 -7 0
|
|
-83 -27 -118 0
|
|
3 -28 15 0
|
|
-80 -60 122 0
|
|
25 -26 -29 0
|
|
-107 40 -57 0
|
|
-71 102 -27 0
|
|
-57 26 71 0
|
|
-49 -83 124 0
|
|
24 -101 77 0
|
|
41 108 -93 0
|
|
99 104 -119 0
|
|
94 89 18 0
|
|
42 -107 -123 0
|
|
88 -4 -48 0
|
|
76 103 -98 0
|
|
12 105 -78 0
|
|
122 110 73 0
|
|
55 -65 -112 0
|
|
125 -68 96 0
|
|
37 -59 12 0
|
|
110 -114 122 0
|
|
-47 115 123 0
|
|
-125 -58 -87 0
|
|
78 109 -10 0
|
|
-82 -68 51 0
|
|
-110 -62 16 0
|
|
-120 45 123 0
|
|
-13 38 59 0
|
|
41 102 28 0
|
|
-42 -107 -125 0
|
|
119 60 13 0
|
|
18 35 -55 0
|
|
-16 40 6 0
|
|
119 -54 7 0
|
|
-78 -20 -13 0
|
|
28 -105 22 0
|
|
-51 7 -97 0
|
|
-74 38 -80 0
|
|
-105 -104 116 0
|
|
78 -102 -35 0
|
|
-57 67 -18 0
|
|
24 -62 52 0
|
|
77 -120 87 0
|
|
15 -87 -116 0
|
|
27 -39 49 0
|
|
-57 -125 78 0
|
|
-30 -120 70 0
|
|
-5 -76 22 0
|
|
-103 121 90 0
|
|
-41 -27 91 0
|
|
100 -20 33 0
|
|
60 -124 -125 0
|
|
31 84 73 0
|
|
56 -28 50 0
|
|
72 37 78 0
|
|
-70 100 59 0
|
|
-107 -87 -26 0
|
|
104 121 -63 0
|
|
105 -103 15 0
|
|
81 -69 47 0
|
|
73 50 22 0
|
|
33 -9 -10 0
|
|
-38 92 95 0
|
|
-87 123 -119 0
|
|
112 108 61 0
|
|
-79 -88 -91 0
|
|
24 2 -1 0
|
|
-8 -97 -81 0
|
|
-119 34 -96 0
|
|
104 122 -107 0
|
|
80 -108 85 0
|
|
37 107 -55 0
|
|
-27 -22 86 0
|
|
81 -118 -65 0
|
|
50 -84 -71 0
|
|
-28 -77 83 0
|
|
-41 -33 22 0
|
|
83 -97 59 0
|
|
75 -35 50 0
|
|
89 11 -113 0
|
|
-9 69 61 0
|
|
7 -96 89 0
|
|
-65 -23 -6 0
|
|
-55 15 -119 0
|
|
-9 118 90 0
|
|
106 36 74 0
|
|
98 9 100 0
|
|
-96 -102 62 0
|
|
60 30 17 0
|
|
-8 17 -38 0
|
|
102 118 -100 0
|
|
54 -6 109 0
|
|
68 37 -122 0
|
|
6 73 1 0
|
|
-69 -8 26 0
|
|
46 82 -31 0
|
|
-121 -60 70 0
|
|
-1 31 49 0
|
|
-94 -40 8 0
|
|
103 -7 -17 0
|
|
-40 33 -77 0
|
|
-9 49 -18 0
|
|
89 30 11 0
|
|
-73 -121 85 0
|
|
-89 -66 29 0
|
|
102 108 -49 0
|
|
12 61 26 0
|
|
10 -102 -85 0
|
|
65 61 -107 0
|
|
-47 -106 -11 0
|
|
92 -63 -62 0
|
|
118 2 49 0
|
|
74 41 39 0
|
|
-19 125 -89 0
|
|
-70 71 85 0
|
|
-35 113 -108 0
|
|
85 120 101 0
|
|
-71 -86 -46 0
|
|
-11 12 106 0
|
|
79 82 -76 0
|
|
-85 72 -84 0
|
|
41 3 -81 0
|
|
-22 -81 54 0
|
|
48 76 -59 0
|
|
-34 4 -27 0
|
|
80 -1 11 0
|
|
-124 -108 -56 0
|
|
-47 -20 -23 0
|
|
-22 10 -38 0
|
|
26 72 90 0
|
|
117 10 -7 0
|
|
-56 47 58 0
|
|
-54 48 76 0
|
|
-38 45 -47 0
|
|
37 -26 -32 0
|
|
8 -70 97 0
|
|
89 -2 -67 0
|
|
77 -42 115 0
|
|
-64 -30 58 0
|
|
-70 16 83 0
|
|
62 24 105 0
|
|
-52 2 53 0
|
|
61 -99 -83 0
|
|
-63 64 -104 0
|
|
52 -118 -98 0
|
|
45 30 13 0
|
|
76 -114 -53 0
|
|
44 -43 49 0
|
|
76 30 112 0
|
|
-12 -75 -27 0
|
|
-97 4 -23 0
|
|
-35 -104 74 0
|
|
-37 26 -98 0
|
|
-8 102 -94 0
|
|
28 42 67 0
|
|
-48 -122 29 0
|
|
-31 -16 36 0
|
|
34 -14 -43 0
|
|
71 -106 -46 0
|
|
-30 3 118 0
|
|
122 105 -15 0
|
|
-83 82 -12 0
|
|
11 -95 -3 0
|
|
121 -46 82 0
|
|
-117 -114 -59 0
|
|
3 -82 96 0
|
|
13 64 103 0
|
|
13 -67 -7 0
|
|
116 -27 72 0
|
|
24 100 61 0
|
|
11 -16 21 0
|
|
-41 -61 19 0
|
|
-78 60 62 0
|
|
83 -44 71 0
|
|
-31 -98 92 0
|
|
117 -105 -38 0
|
|
-60 38 99 0
|
|
76 89 91 0
|
|
1 61 80 0
|
|
60 -109 40 0
|
|
-44 -81 -110 0
|
|
36 34 124 0
|
|
38 108 117 0
|
|
-14 26 -70 0
|
|
103 116 64 0
|
|
22 60 -109 0
|
|
-92 52 116 0
|
|
-118 -99 5 0
|
|
-119 -116 -57 0
|
|
-18 -61 -102 0
|
|
-110 -99 -53 0
|
|
51 72 121 0
|
|
-63 30 31 0
|
|
99 -8 -125 0
|
|
-17 88 -18 0
|
|
111 -29 69 0
|
|
-108 -46 120 0
|
|
-35 -25 -60 0
|
|
-74 -66 82 0
|
|
30 -112 115 0
|
|
-17 91 62 0
|
|
8 -112 -104 0
|
|
-33 -124 90 0
|
|
-42 -12 -123 0
|
|
25 113 80 0
|
|
-47 51 25 0
|
|
41 19 -15 0
|
|
85 54 102 0
|
|
-107 64 52 0
|
|
73 -86 123 0
|
|
-87 20 -84 0
|
|
15 44 113 0
|
|
-7 -22 -62 0
|
|
-24 53 -22 0
|
|
-85 105 43 0
|
|
-115 -93 35 0
|
|
42 -93 81 0
|
|
-37 -4 -40 0
|
|
-57 -10 -39 0
|
|
-35 -43 50 0
|
|
92 115 -24 0
|
|
-39 103 -70 0
|
|
12 44 69 0
|
|
-38 74 65 0
|
|
-22 61 -67 0
|
|
2 -104 -56 0
|
|
-1 19 -95 0
|
|
-11 -25 21 0
|
|
-10 -114 112 0
|
|
98 86 -73 0
|
|
106 32 64 0
|
|
-29 57 -63 0
|
|
-100 13 121 0
|
|
103 -39 19 0
|
|
-25 -63 -105 0
|
|
-45 1 4 0
|
|
-110 114 -108 0
|
|
-4 -34 -77 0
|
|
-74 -123 4 0
|
|
-25 38 -14 0
|
|
-9 -7 81 0
|
|
74 51 113 0
|
|
-13 45 81 0
|
|
-74 -88 37 0
|
|
-111 -113 49 0
|
|
77 85 -61 0
|
|
36 123 -50 0
|
|
70 65 10 0
|
|
-65 103 -112 0
|
|
113 40 62 0
|
|
91 116 96 0
|
|
-25 -59 -17 0
|
|
40 26 9 0
|
|
73 -116 -15 0
|
|
-9 -79 108 0
|
|
82 -80 11 0
|
|
-73 -6 93 0
|
|
33 120 -74 0
|