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