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