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