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