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