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