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