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