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