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