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