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