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