sidekick/tests/uuf150/uuf150-054.cnf

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 150  645 
 104 -68 144 0
81 -101 -71 0
23 -146 6 0
-128 126 -101 0
-85 -113 115 0
104 45 67 0
99 138 -148 0
-136 -60 95 0
-149 59 18 0
47 -143 -1 0
85 -96 22 0
69 -61 -47 0
-16 66 144 0
3 57 133 0
59 52 33 0
37 -148 -120 0
117 -69 144 0
-97 -1 140 0
-16 -113 -104 0
39 -42 10 0
97 139 71 0
-149 14 -138 0
66 -123 -56 0
-79 46 56 0
115 71 -24 0
133 11 -16 0
48 -70 73 0
106 -69 -17 0
114 -61 145 0
33 -102 -95 0
2 121 127 0
102 -67 103 0
-70 63 -117 0
36 -9 31 0
-87 -97 -149 0
143 56 -91 0
-112 -141 -76 0
-56 -10 89 0
28 119 46 0
-113 -109 138 0
76 -94 128 0
139 65 -43 0
-37 -106 -150 0
13 125 50 0
-99 -146 -32 0
-10 32 75 0
-40 -37 -93 0
73 -137 99 0
5 125 20 0
127 132 48 0
140 79 -36 0
92 105 119 0
-27 110 56 0
20 -37 143 0
-92 67 -7 0
144 -64 4 0
-112 -70 24 0
150 -130 21 0
74 124 89 0
-92 -105 95 0
24 -88 83 0
-96 78 -130 0
31 8 63 0
103 136 140 0
70 -143 108 0
-34 -114 -140 0
26 87 35 0
89 -86 -50 0
17 -90 -98 0
-10 51 -142 0
20 99 46 0
-115 -91 124 0
-42 34 -116 0
53 51 41 0
-150 68 -71 0
-74 54 -84 0
-7 27 89 0
-9 67 -68 0
-76 61 3 0
137 62 127 0
-43 -127 -65 0
125 -103 3 0
97 91 -96 0
-115 -140 14 0
27 -93 136 0
-14 43 -15 0
55 145 -63 0
86 4 -32 0
-132 -141 148 0
-125 39 -59 0
142 -81 112 0
124 94 -135 0
-117 4 65 0
-132 -3 55 0
-52 75 -39 0
57 -45 -7 0
89 -88 51 0
-52 -85 -56 0
-31 64 78 0
-87 95 103 0
52 -110 50 0
15 -66 102 0
117 41 -5 0
98 -37 150 0
53 59 137 0
12 -86 -150 0
75 9 42 0
-97 40 -71 0
38 9 -114 0
80 -87 145 0
-106 104 -114 0
-82 -90 115 0
4 63 -78 0
-1 -51 148 0
50 -17 118 0
73 -38 13 0
-142 74 -116 0
145 -51 144 0
61 -125 -58 0
90 139 -11 0
-116 -105 -131 0
-4 -133 -46 0
52 83 -144 0
-53 -66 93 0
-104 -63 20 0
58 85 -8 0
11 66 131 0
-149 -87 2 0
110 -34 71 0
-84 97 -108 0
7 120 11 0
-12 18 137 0
61 72 -108 0
-68 23 -123 0
-33 -9 -63 0
-66 -118 -94 0
-148 -143 118 0
-6 -45 113 0
53 23 -49 0
140 44 -132 0
-26 99 61 0
70 23 35 0
79 -13 63 0
-67 29 41 0
88 -43 -95 0
12 -121 -77 0
-114 10 -124 0
-17 125 -144 0
-97 83 148 0
-40 135 93 0
112 -66 -8 0
-140 -102 106 0
-94 115 -127 0
57 -141 -75 0
104 17 107 0
-83 -112 76 0
-37 -139 -15 0
-145 -46 -79 0
114 -40 -113 0
-10 -47 -107 0
127 -25 70 0
-116 -2 59 0
93 -139 57 0
-143 -75 79 0
45 -123 69 0
109 -66 36 0
98 84 -3 0
16 6 -136 0
112 -20 -21 0
-62 19 107 0
142 129 -111 0
28 -104 12 0
27 125 -80 0
-109 8 -126 0
113 -110 -118 0
114 -82 -116 0
3 136 77 0
89 43 11 0
-126 -13 -65 0
50 104 72 0
-5 136 93 0
93 -63 36 0
55 17 -94 0
122 -11 10 0
149 12 -106 0
81 34 114 0
-73 -97 87 0
-10 -20 31 0
-101 -56 77 0
112 91 -50 0
45 -91 -112 0
-31 -37 62 0
132 -5 -46 0
78 59 -36 0
-41 131 -69 0
-18 -92 -19 0
95 -130 19 0
-32 -79 -19 0
-58 18 35 0
-72 62 -34 0
-69 -19 -22 0
-70 -93 101 0
-103 131 127 0
-98 116 -84 0
36 -131 15 0
149 -39 35 0
-141 -46 126 0
-140 87 -54 0
-33 -5 -77 0
-70 -23 -116 0
-101 -89 -125 0
-18 99 -146 0
-67 -29 -66 0
81 -27 -128 0
-143 -62 -137 0
45 -96 -16 0
-119 -99 -73 0
94 -8 -142 0
-133 58 13 0
75 57 67 0
139 -60 -9 0
127 47 -38 0
12 -105 -136 0
138 96 -20 0
5 130 141 0
-134 30 -65 0
-82 10 39 0
-97 71 -4 0
45 61 -62 0
-147 -66 -97 0
143 -122 18 0
-49 45 -60 0
-136 110 -40 0
105 -87 -23 0
-134 -147 -150 0
-68 126 108 0
135 81 -116 0
14 -3 -89 0
16 -96 68 0
-122 95 64 0
108 93 23 0
-137 13 135 0
81 -71 -4 0
1 139 90 0
135 -148 146 0
-95 -76 -114 0
22 -127 4 0
8 9 -132 0
-6 -30 -95 0
-145 -82 -119 0
-11 74 12 0
-115 62 128 0
29 -76 -65 0
115 92 123 0
-30 31 -1 0
-84 32 -54 0
97 -121 7 0
131 -116 -150 0
-139 -90 29 0
30 27 -95 0
11 108 147 0
10 150 123 0
-91 -55 27 0
27 89 -92 0
119 -79 -117 0
28 120 99 0
-28 43 -2 0
-61 -149 -131 0
89 116 19 0
-119 139 -146 0
76 -79 -74 0
25 -131 150 0
-102 -41 -57 0
13 -66 -111 0
-99 -64 120 0
-48 -74 99 0
-79 -122 34 0
137 99 55 0
-39 43 98 0
-131 -22 -106 0
120 -14 -28 0
122 -64 -97 0
19 128 43 0
105 60 116 0
95 -40 62 0
5 110 41 0
-7 149 -89 0
-47 -22 -58 0
-12 -50 139 0
-18 -46 -89 0
-106 -100 37 0
-22 -140 64 0
-41 -139 89 0
27 90 84 0
64 85 80 0
-80 -120 -126 0
-31 -137 97 0
-12 -137 -28 0
134 -112 -45 0
102 41 47 0
57 -121 -29 0
-140 118 -131 0
125 74 -65 0
108 8 -111 0
114 27 127 0
-69 -115 -140 0
92 136 -45 0
149 47 30 0
62 7 -61 0
-109 -122 12 0
-104 -50 33 0
19 89 -15 0
20 9 134 0
102 133 39 0
148 113 -18 0
-78 -1 48 0
140 112 -133 0
91 -44 1 0
-107 44 55 0
42 54 22 0
-58 -140 70 0
-1 -89 -125 0
-126 -34 -43 0
-49 64 -29 0
12 101 138 0
103 68 -40 0
36 24 78 0
8 -133 54 0
35 -8 -75 0
-148 122 -85 0
36 -109 13 0
-63 17 60 0
10 -34 50 0
-73 118 -17 0
131 28 -99 0
10 -49 63 0
-58 35 -59 0
-34 118 -83 0
20 18 -108 0
148 -76 -33 0
-72 -137 -48 0
-1 145 -150 0
-1 -53 -52 0
-26 19 120 0
-68 -33 94 0
-86 -17 -20 0
74 -111 -123 0
8 79 45 0
-12 37 -63 0
-149 87 130 0
-126 -122 91 0
-124 -28 -12 0
-89 110 18 0
-27 30 -66 0
36 -10 23 0
89 78 -30 0
-81 -46 -12 0
31 81 -73 0
-77 90 -121 0
-78 -64 -140 0
9 17 -20 0
23 128 -138 0
148 -100 -60 0
-11 75 -63 0
-112 -144 -3 0
44 -102 -98 0
-5 13 121 0
121 -45 -140 0
4 -125 -62 0
6 68 122 0
90 -63 17 0
31 -130 19 0
42 -92 110 0
-19 127 49 0
58 49 -73 0
-94 147 -6 0
-117 64 -111 0
51 -108 -23 0
-84 -8 122 0
138 146 -63 0
3 -119 -117 0
-139 45 -64 0
30 -81 87 0
48 26 83 0
-34 146 16 0
67 58 -9 0
-33 54 132 0
76 -31 93 0
87 -131 59 0
39 -34 -62 0
-95 -46 -25 0
40 111 -144 0
-32 -133 -26 0
7 -82 -89 0
132 140 -122 0
10 -139 147 0
-124 131 -36 0
-112 33 76 0
97 -13 -3 0
-124 -61 -94 0
46 -114 126 0
117 -122 47 0
96 50 -80 0
-93 134 98 0
-50 -143 87 0
-131 133 3 0
23 -142 122 0
118 -91 -110 0
-132 55 -131 0
106 50 -142 0
-82 -23 -62 0
85 2 79 0
116 -38 -15 0
72 -66 32 0
52 -102 -81 0
123 75 -145 0
121 -94 124 0
-123 114 83 0
-114 110 -84 0
-26 -64 30 0
-79 -99 74 0
-84 51 21 0
-106 14 148 0
57 12 98 0
77 87 -57 0
112 -122 -28 0
-82 19 -35 0
17 107 -98 0
-29 106 10 0
3 -84 120 0
139 -79 135 0
1 -45 -87 0
120 12 -45 0
-66 55 51 0
-108 -34 -141 0
90 -82 -35 0
-142 -99 43 0
17 104 -51 0
7 86 131 0
-115 119 -46 0
-62 136 70 0
-94 -51 -116 0
25 146 54 0
-1 -64 10 0
143 86 140 0
-26 101 -21 0
-114 -141 -130 0
-29 -1 105 0
6 77 15 0
-50 132 25 0
114 123 82 0
-23 -9 -140 0
130 136 54 0
-67 138 142 0
-117 96 20 0
-52 147 14 0
-143 78 41 0
-81 9 12 0
50 137 -62 0
-79 35 -53 0
140 78 -81 0
-36 53 -64 0
-102 117 114 0
150 -8 99 0
118 -111 108 0
56 -65 -124 0
95 28 -23 0
-123 -29 -67 0
123 129 96 0
-127 136 -133 0
-127 108 34 0
-59 -111 -35 0
-47 103 -126 0
-52 -12 -83 0
20 -60 -87 0
121 120 -96 0
12 128 74 0
-143 106 8 0
73 -121 -58 0
107 -137 51 0
-31 -110 -14 0
89 125 -60 0
66 -14 -74 0
119 55 -113 0
17 -67 -59 0
-14 125 65 0
-102 -117 -15 0
-137 10 -4 0
-24 116 148 0
101 112 81 0
99 31 16 0
17 -110 -40 0
-112 69 -135 0
-86 -61 -102 0
98 -95 -109 0
-70 53 6 0
7 -82 123 0
21 75 123 0
-142 125 71 0
89 6 -10 0
23 103 -16 0
41 -44 -13 0
67 -111 -51 0
-49 107 -64 0
34 138 127 0
7 -58 -113 0
-104 -126 -44 0
-93 54 -143 0
-142 14 -145 0
143 -50 -93 0
42 -142 66 0
-18 52 -109 0
76 93 -34 0
-150 -26 105 0
110 129 66 0
6 -57 142 0
-137 -138 119 0
37 -48 -99 0
-12 -115 -10 0
133 -68 -125 0
49 125 45 0
-108 -33 -3 0
83 -15 -22 0
16 96 101 0
-21 -45 -126 0
134 142 -70 0
43 140 -148 0
20 149 140 0
-27 47 -21 0
36 -93 127 0
106 -70 -62 0
-140 141 -84 0
-112 -56 148 0
26 -123 -75 0
-128 -136 89 0
-24 -102 95 0
-29 -116 34 0
-111 64 126 0
138 -41 -44 0
-58 64 -130 0
-21 -41 77 0
9 -4 -19 0
-112 77 35 0
8 -23 90 0
46 -143 -89 0
-150 -10 -146 0
-130 134 -126 0
119 136 18 0
-53 -80 76 0
-18 27 -3 0
62 -51 -1 0
30 -108 -109 0
-96 -75 119 0
-17 -131 -120 0
-104 -141 128 0
-97 9 79 0
72 -97 -13 0
-13 47 -43 0
-22 -28 102 0
93 74 65 0
98 126 -21 0
-82 145 -34 0
-63 38 32 0
77 41 70 0
102 125 -114 0
28 142 119 0
136 99 35 0
4 107 -97 0
-78 139 6 0
37 -119 12 0
-143 13 47 0
2 46 14 0
96 -70 -14 0
7 33 -65 0
49 67 50 0
116 60 -46 0
-77 22 2 0
147 4 -137 0
86 53 124 0
-82 114 -69 0
15 140 45 0
17 80 -87 0
86 17 149 0
-13 -113 98 0
139 44 -126 0
-42 -39 -140 0
-1 -115 -71 0
-82 -69 -107 0
125 -3 95 0
84 127 -100 0
60 75 -12 0
-40 -12 75 0
50 -31 -126 0
-139 86 -119 0
-140 92 -84 0
63 -61 42 0
-34 -148 65 0
-15 8 44 0
107 -1 -91 0
-32 73 39 0
-81 -74 100 0
-25 -30 56 0
-102 -2 21 0
-150 99 -35 0
-38 54 41 0
116 100 -125 0
123 96 -2 0
42 -135 -141 0
-96 130 -81 0
-98 107 8 0
40 149 125 0
-136 37 141 0
-126 107 -10 0
99 -116 119 0
-133 43 145 0
-16 -70 -26 0
36 69 125 0
51 -32 147 0
49 -96 -131 0
56 -107 -119 0
-78 -112 68 0
42 138 -69 0
57 -65 6 0
69 24 98 0
-126 -96 -30 0
92 74 88 0
-9 -68 27 0
52 142 -106 0
60 113 -104 0
-79 -138 -90 0
84 23 9 0
-61 -41 103 0
-127 -20 29 0
-12 -136 36 0
109 71 -36 0
-134 -112 141 0
-27 -43 63 0
16 106 -50 0
117 50 -112 0
-49 123 24 0
52 -5 -14 0
-64 24 39 0
6 19 124 0
-32 29 61 0
-97 79 48 0