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