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