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