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