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