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