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