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