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