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