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