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