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