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