mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
438 lines
5.3 KiB
INI
438 lines
5.3 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 100 430
|
|
-84 -51 82 0
|
|
85 8 72 0
|
|
64 31 -58 0
|
|
5 -13 -8 0
|
|
-72 -91 36 0
|
|
-1 63 -68 0
|
|
-95 29 61 0
|
|
-12 99 -34 0
|
|
35 20 -70 0
|
|
-42 5 47 0
|
|
-95 -2 88 0
|
|
-15 79 -61 0
|
|
78 57 95 0
|
|
69 61 -31 0
|
|
94 45 -68 0
|
|
-66 -16 -70 0
|
|
84 -92 -33 0
|
|
41 -44 -33 0
|
|
-47 -23 18 0
|
|
40 -54 -65 0
|
|
76 59 -2 0
|
|
99 96 71 0
|
|
7 81 80 0
|
|
98 62 57 0
|
|
-35 -78 -71 0
|
|
-85 59 24 0
|
|
66 3 -30 0
|
|
-73 -40 -50 0
|
|
87 -77 -28 0
|
|
61 26 43 0
|
|
96 -10 -85 0
|
|
-54 -62 91 0
|
|
54 71 64 0
|
|
-68 -10 19 0
|
|
60 13 -36 0
|
|
28 -40 -70 0
|
|
-2 -13 27 0
|
|
-16 -50 96 0
|
|
21 -28 40 0
|
|
-76 94 85 0
|
|
6 78 -14 0
|
|
20 50 6 0
|
|
27 96 6 0
|
|
-69 -72 66 0
|
|
59 -46 99 0
|
|
-41 -60 57 0
|
|
-78 -45 -42 0
|
|
16 86 99 0
|
|
47 -2 -15 0
|
|
27 -44 -12 0
|
|
68 -21 54 0
|
|
59 57 -94 0
|
|
-73 -62 71 0
|
|
13 28 -6 0
|
|
94 -66 35 0
|
|
-100 -58 34 0
|
|
-2 41 70 0
|
|
-81 -13 -77 0
|
|
-55 96 86 0
|
|
-51 16 -91 0
|
|
99 -20 40 0
|
|
45 -75 61 0
|
|
29 51 -14 0
|
|
63 56 91 0
|
|
-74 -66 29 0
|
|
-46 -49 70 0
|
|
-6 25 -17 0
|
|
-68 38 -81 0
|
|
-36 94 -68 0
|
|
57 75 -9 0
|
|
-67 -73 -27 0
|
|
57 79 -86 0
|
|
-90 -86 11 0
|
|
47 -94 -44 0
|
|
94 -34 -27 0
|
|
-60 -21 -24 0
|
|
-56 -28 42 0
|
|
40 59 -25 0
|
|
-57 -10 -18 0
|
|
-64 -20 97 0
|
|
25 -94 72 0
|
|
67 93 -5 0
|
|
22 -83 -36 0
|
|
21 49 62 0
|
|
9 82 68 0
|
|
54 -72 -35 0
|
|
-75 -50 93 0
|
|
-58 80 18 0
|
|
46 -48 -59 0
|
|
55 95 60 0
|
|
-63 -55 -79 0
|
|
-97 55 -11 0
|
|
24 -92 -49 0
|
|
51 31 22 0
|
|
88 92 3 0
|
|
54 -76 58 0
|
|
93 -70 92 0
|
|
72 82 18 0
|
|
95 -74 -33 0
|
|
24 71 -62 0
|
|
-29 71 52 0
|
|
23 -95 -94 0
|
|
-40 -71 -34 0
|
|
-59 85 31 0
|
|
62 -25 85 0
|
|
99 -79 -74 0
|
|
-74 87 -71 0
|
|
-19 -41 40 0
|
|
9 56 15 0
|
|
53 8 -40 0
|
|
39 -29 69 0
|
|
-88 51 20 0
|
|
-28 -36 -61 0
|
|
96 -12 10 0
|
|
87 -66 -65 0
|
|
-63 25 -23 0
|
|
63 -53 -75 0
|
|
48 -7 55 0
|
|
10 90 -24 0
|
|
45 11 47 0
|
|
-64 -97 -67 0
|
|
41 -33 -22 0
|
|
-9 1 -99 0
|
|
-75 25 82 0
|
|
79 -90 17 0
|
|
68 63 46 0
|
|
2 89 50 0
|
|
15 -13 4 0
|
|
-6 51 -44 0
|
|
93 -27 -77 0
|
|
59 -19 -38 0
|
|
-22 -55 -74 0
|
|
-73 93 -90 0
|
|
95 -11 -17 0
|
|
26 -90 92 0
|
|
77 -57 63 0
|
|
-99 -83 69 0
|
|
51 26 38 0
|
|
7 97 54 0
|
|
-88 -60 40 0
|
|
-22 -38 -95 0
|
|
-99 51 -38 0
|
|
-13 74 16 0
|
|
94 20 15 0
|
|
97 29 -8 0
|
|
-74 29 -6 0
|
|
-23 -11 8 0
|
|
-52 90 4 0
|
|
-85 -33 -36 0
|
|
-48 75 7 0
|
|
23 -84 -42 0
|
|
-87 74 65 0
|
|
24 -86 -31 0
|
|
-43 38 -3 0
|
|
56 -83 -62 0
|
|
-61 -50 -17 0
|
|
-76 74 -35 0
|
|
92 93 -6 0
|
|
62 83 -78 0
|
|
-96 2 -14 0
|
|
32 -99 29 0
|
|
-19 64 3 0
|
|
29 24 3 0
|
|
-10 4 31 0
|
|
-45 -38 -50 0
|
|
-39 -27 -88 0
|
|
-96 95 -39 0
|
|
8 77 95 0
|
|
-58 20 -41 0
|
|
-36 51 21 0
|
|
-74 47 43 0
|
|
-36 10 -13 0
|
|
46 15 37 0
|
|
77 -82 -66 0
|
|
100 -5 22 0
|
|
-37 63 -78 0
|
|
98 58 1 0
|
|
71 78 23 0
|
|
54 95 -28 0
|
|
91 12 -100 0
|
|
43 70 -52 0
|
|
12 -47 -32 0
|
|
20 27 -42 0
|
|
88 87 -54 0
|
|
11 96 78 0
|
|
-100 -51 80 0
|
|
-24 -82 74 0
|
|
-20 -14 -57 0
|
|
-20 -44 -77 0
|
|
39 -69 -78 0
|
|
26 79 36 0
|
|
33 53 -88 0
|
|
-37 -28 -96 0
|
|
-84 -8 -95 0
|
|
42 19 22 0
|
|
4 -61 80 0
|
|
45 98 -62 0
|
|
14 41 -98 0
|
|
-61 -18 -93 0
|
|
7 18 92 0
|
|
29 -39 -87 0
|
|
-17 -22 -51 0
|
|
48 -67 96 0
|
|
30 -36 47 0
|
|
-94 98 -41 0
|
|
-12 -55 -16 0
|
|
51 -79 -14 0
|
|
-56 4 34 0
|
|
81 -77 46 0
|
|
-50 -92 -33 0
|
|
-67 -89 -13 0
|
|
-75 38 54 0
|
|
-56 94 -13 0
|
|
100 -25 38 0
|
|
81 -1 28 0
|
|
-72 58 -93 0
|
|
59 15 -17 0
|
|
22 60 -50 0
|
|
96 -48 -18 0
|
|
-69 -73 -70 0
|
|
-100 59 -18 0
|
|
-72 2 -73 0
|
|
-44 -36 -35 0
|
|
87 -66 31 0
|
|
73 -67 -96 0
|
|
2 -62 -41 0
|
|
77 25 -85 0
|
|
-26 57 35 0
|
|
-44 36 -71 0
|
|
-97 -12 -36 0
|
|
76 -55 60 0
|
|
-99 52 -38 0
|
|
83 -26 -8 0
|
|
-21 29 92 0
|
|
-60 -100 -43 0
|
|
-94 -68 51 0
|
|
66 -83 -77 0
|
|
-54 -48 -3 0
|
|
17 -85 18 0
|
|
-40 36 21 0
|
|
78 -25 -81 0
|
|
53 44 47 0
|
|
6 -100 61 0
|
|
97 -77 -10 0
|
|
-35 25 -21 0
|
|
68 84 -77 0
|
|
-13 -65 98 0
|
|
71 99 44 0
|
|
-56 4 -81 0
|
|
-50 52 -91 0
|
|
-22 74 -80 0
|
|
-53 -34 56 0
|
|
95 -64 -47 0
|
|
43 51 -57 0
|
|
-90 64 26 0
|
|
-77 -55 5 0
|
|
48 -6 -61 0
|
|
-51 17 -98 0
|
|
-32 -62 -8 0
|
|
44 -40 8 0
|
|
-100 -28 -44 0
|
|
4 86 -31 0
|
|
-58 -93 1 0
|
|
6 -14 74 0
|
|
96 12 -90 0
|
|
-42 -35 -90 0
|
|
-55 95 -57 0
|
|
-68 58 -92 0
|
|
-80 18 -87 0
|
|
-4 27 66 0
|
|
56 -72 35 0
|
|
-16 -11 20 0
|
|
-71 64 -77 0
|
|
35 -11 8 0
|
|
76 -68 -66 0
|
|
-41 -17 67 0
|
|
1 78 34 0
|
|
40 -21 92 0
|
|
6 17 -34 0
|
|
51 -14 65 0
|
|
-12 -95 42 0
|
|
1 -71 82 0
|
|
-63 30 52 0
|
|
-77 -51 11 0
|
|
15 -2 -73 0
|
|
43 51 40 0
|
|
-21 -91 -24 0
|
|
-17 -11 6 0
|
|
-48 -7 -90 0
|
|
66 84 80 0
|
|
-37 -57 86 0
|
|
19 -98 -96 0
|
|
97 70 87 0
|
|
42 89 49 0
|
|
-10 -13 2 0
|
|
24 -88 -74 0
|
|
14 82 49 0
|
|
-87 21 71 0
|
|
-15 -66 100 0
|
|
-82 -7 59 0
|
|
-100 19 -97 0
|
|
-24 -42 -72 0
|
|
38 86 -43 0
|
|
-25 -75 -53 0
|
|
-70 -78 -57 0
|
|
53 91 64 0
|
|
49 60 65 0
|
|
93 -48 16 0
|
|
88 -82 -99 0
|
|
-39 48 -96 0
|
|
-45 11 25 0
|
|
19 -89 13 0
|
|
-32 47 -58 0
|
|
-55 -85 -81 0
|
|
33 -94 98 0
|
|
90 -30 -29 0
|
|
-63 -18 46 0
|
|
-18 -89 -91 0
|
|
57 9 79 0
|
|
-88 -36 27 0
|
|
4 -53 41 0
|
|
90 29 57 0
|
|
-80 -22 -2 0
|
|
64 -53 -65 0
|
|
76 -78 -4 0
|
|
-13 -68 -20 0
|
|
93 89 16 0
|
|
-62 -4 41 0
|
|
-19 -38 -90 0
|
|
-52 -55 59 0
|
|
23 70 -89 0
|
|
29 -16 77 0
|
|
64 -26 -4 0
|
|
41 -7 -15 0
|
|
-11 -42 49 0
|
|
-91 -19 -75 0
|
|
68 89 -13 0
|
|
45 97 -2 0
|
|
26 -41 -97 0
|
|
-34 -83 28 0
|
|
87 42 -62 0
|
|
88 92 71 0
|
|
76 21 49 0
|
|
-50 61 35 0
|
|
22 -15 -50 0
|
|
-90 7 16 0
|
|
-10 15 9 0
|
|
-27 22 -53 0
|
|
13 -95 -34 0
|
|
69 5 81 0
|
|
92 98 -53 0
|
|
25 59 94 0
|
|
66 65 61 0
|
|
92 -51 -1 0
|
|
-92 -67 -89 0
|
|
-19 -77 95 0
|
|
50 8 2 0
|
|
82 6 4 0
|
|
48 15 -93 0
|
|
33 32 58 0
|
|
19 -22 20 0
|
|
-58 -42 -12 0
|
|
99 65 -58 0
|
|
44 54 97 0
|
|
-28 -36 -68 0
|
|
28 -77 -93 0
|
|
-51 48 27 0
|
|
-14 5 -75 0
|
|
53 -51 35 0
|
|
-85 -15 73 0
|
|
24 -28 -7 0
|
|
2 -26 -45 0
|
|
38 -2 -56 0
|
|
93 -25 14 0
|
|
65 57 16 0
|
|
-68 32 42 0
|
|
72 -49 43 0
|
|
67 14 32 0
|
|
-85 20 -28 0
|
|
99 12 -57 0
|
|
-30 -17 97 0
|
|
88 -64 -94 0
|
|
-60 -46 84 0
|
|
94 -53 -29 0
|
|
-21 -50 87 0
|
|
43 -94 53 0
|
|
-84 -53 -7 0
|
|
46 42 -32 0
|
|
-40 26 52 0
|
|
44 68 52 0
|
|
66 88 -9 0
|
|
-62 -10 26 0
|
|
-54 -33 -49 0
|
|
84 -1 -6 0
|
|
-38 12 -21 0
|
|
6 8 -53 0
|
|
87 -86 -89 0
|
|
-20 -7 -8 0
|
|
-48 76 70 0
|
|
6 50 -51 0
|
|
91 -44 100 0
|
|
23 -45 -10 0
|
|
-87 76 -71 0
|
|
64 91 38 0
|
|
72 -49 99 0
|
|
14 66 81 0
|
|
37 32 83 0
|
|
-10 31 -15 0
|
|
-42 88 -48 0
|
|
29 93 40 0
|
|
64 28 -80 0
|
|
-83 77 -20 0
|
|
4 34 94 0
|
|
77 55 6 0
|
|
-16 -64 19 0
|
|
69 -55 -60 0
|
|
-37 81 -77 0
|
|
20 -50 34 0
|
|
31 -45 2 0
|
|
-63 84 -99 0
|
|
-14 -8 44 0
|
|
73 92 -23 0
|
|
-50 -67 -18 0
|
|
29 10 -31 0
|
|
-66 -9 83 0
|
|
-54 -4 -29 0
|
|
-39 -50 75 0
|
|
29 48 -89 0
|
|
-33 -59 77 0
|
|
62 53 31 0
|