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