sidekick/tests/ssa/ssa0432-003.cnf

c FILE:  ssa0432-003.cnf
c
c SOURCE: Allen Van Gelder (avg@cs.ucsd.edu) and Yumi Tsuji
c        (tsuji@cse.ucsc.edu) 
c
c Nemesis formula in 6CNF in accordance with DIMACS CNF format:
c    Filename: MCNC/c432/c432.tdl
c    Formula number 3
c    1265 variables (range: 2 - 1266)
c    1027 clauses
c
c p cnf 1266 1027
p cnf 435 1027
435	0
174	0
-175	0
173	0
-39	-433	0
37	-433	0
39	-434	0
-37	-434	0
-434	432	0
-433	432	0
-79	-37	0
-67	-37	0
-68	38	0
-68	-79	0
-79	-39	0
-69	-39	0
-76	-67	0
-71	-67	0
-74	-67	0
-138	-67	0
-72	68	0
-72	-138	0
-72	-74	0
-72	-76	0
-76	-69	0
-73	-69	0
-74	-69	0
-138	-69	0
75	-138	0
-75	138	0
75	-139	0
-75	139	0
75	-147	0
-75	147	0
-311	-75	0
-307	-75	0
312	307	0
-312	-307	0
15	-315	0
-15	315	0
15	-316	0
-15	316	0
53	-93	0
-53	93	0
53	-94	0
-53	94	0
53	-98	0
-53	98	0
53	-102	0
-53	102	0
53	-105	0
-53	105	0
53	-119	0
-53	119	0
53	-121	0
-53	121	0
53	-124	0
-53	124	0
53	-129	0
-53	129	0
53	-169	0
-53	169	0
53	-207	0
-53	207	0
53	-221	0
-53	221	0
53	-244	0
-53	244	0
53	-250	0
-53	250	0
53	-304	0
-53	304	0
53	-314	0
-53	314	0
53	-330	0
-53	330	0
53	-343	0
-53	343	0
53	-345	0
-53	345	0
53	-360	0
-53	360	0
53	-378	0
-53	378	0
60	53	0
263	53	0
176	53	0
182	53	0
188	182	0
-188	-182	0
104	-187	0
-104	187	0
104	-188	0
-104	188	0
-196	-104	0
-191	-104	0
-193	-104	0
184	-192	0
-184	192	0
184	-193	0
-184	193	0
184	-200	0
-184	200	0
184	-203	0
-184	203	0
34	184	0
-34	-184	0
12	-190	0
-12	190	0
12	-191	0
-12	191	0
189	-196	0
-189	196	0
189	-197	0
-189	197	0
-271	-422	0
195	-422	0
271	-423	0
-195	-423	0
-423	189	0
-422	189	0
42	-80	0
-42	80	0
42	-81	0
-42	81	0
42	-84	0
-42	84	0
42	-101	0
-42	101	0
42	-112	0
-42	112	0
42	-166	0
-42	166	0
42	-195	0
-42	195	0
42	-218	0
-42	218	0
42	-241	0
-42	241	0
42	-259	0
-42	259	0
42	-291	0
-42	291	0
42	-303	0
-42	303	0
42	-313	0
-42	313	0
42	-323	0
-42	323	0
42	-344	0
-42	344	0
42	-349	0
-42	349	0
42	-357	0
-42	357	0
42	-385	0
-42	385	0
42	-404	0
-42	404	0
286	42	0
267	42	0
43	42	0
278	42	0
347	278	0
-347	-278	0
279	-347	0
-279	347	0
279	-348	0
-279	348	0
-369	-279	0
-370	-279	0
281	-284	0
-281	284	0
281	-285	0
-281	285	0
281	-301	0
-281	301	0
281	-370	0
-281	370	0
26	281	0
-26	-281	0
7	-368	0
-7	368	0
7	-369	0
-7	369	0
-110	-43	0
-46	-43	0
41	-45	0
-41	45	0
41	-46	0
-41	46	0
-219	-41	0
-211	-41	0
204	-211	0
-204	211	0
204	-212	0
-204	212	0
214	204	0
-214	-204	0
32	-214	0
-32	214	0
32	-215	0
-32	215	0
32	-228	0
-32	228	0
5	-219	0
-5	219	0
5	-220	0
-5	220	0
44	-110	0
-44	110	0
44	-111	0
-44	111	0
-358	-44	0
-355	-44	0
350	-353	0
-350	353	0
350	-354	0
-350	354	0
350	-355	0
-350	355	0
350	-367	0
-350	367	0
9	350	0
-9	-350	0
21	-358	0
-21	358	0
21	-359	0
-21	359	0
-270	-267	0
-268	-267	0
-272	-267	0
194	-271	0
-194	271	0
194	-272	0
-194	272	0
-202	-194	0
-203	-194	0
25	-201	0
-25	201	0
25	-202	0
-25	202	0
331	268	0
324	268	0
332	268	0
402	332	0
-402	-332	0
391	-402	0
-391	402	0
391	-403	0
-391	403	0
-400	-391	0
-401	-391	0
392	-397	0
-392	397	0
392	-398	0
-392	398	0
392	-401	0
-392	401	0
392	-409	0
-392	409	0
19	392	0
-19	-392	0
17	-399	0
-17	399	0
17	-400	0
-17	400	0
326	324	0
-326	-324	0
322	-325	0
-322	325	0
322	-326	0
-322	326	0
-389	-322	0
-390	-322	0
235	-386	0
-235	386	0
235	-387	0
-235	387	0
235	-390	0
-235	390	0
383	235	0
-383	-235	0
35	-382	0
-35	382	0
35	-383	0
-35	383	0
30	-388	0
-30	388	0
30	-389	0
-30	389	0
334	331	0
-334	-331	0
83	-333	0
-83	333	0
83	-334	0
-83	334	0
-320	-83	0
-321	-83	0
86	-91	0
-86	91	0
86	-92	0
-86	92	0
86	-158	0
-86	158	0
86	-321	0
-86	321	0
28	86	0
-28	-86	0
4	-317	0
-4	317	0
4	-320	0
-4	320	0
237	-269	0
-237	269	0
237	-270	0
-237	270	0
-242	-237	0
-239	-237	0
232	-238	0
-232	238	0
232	-239	0
-232	239	0
253	232	0
-253	-232	0
6	-253	0
-6	253	0
6	-254	0
-6	254	0
6	-258	0
-6	258	0
10	-242	0
-10	242	0
10	-243	0
-10	243	0
289	286	0
-289	-286	0
287	-289	0
-287	289	0
287	-290	0
-287	290	0
-372	-287	0
-373	-287	0
292	-295	0
-292	295	0
292	-296	0
-292	296	0
292	-311	0
-292	311	0
292	-373	0
-292	373	0
27	292	0
-27	-292	0
11	-371	0
-11	371	0
11	-372	0
-11	372	0
-180	-176	0
-328	-176	0
-276	-176	0
178	-276	0
-178	276	0
178	-277	0
-178	277	0
178	-342	0
-178	342	0
-405	-178	0
-396	-178	0
-398	-178	0
18	-395	0
-18	395	0
18	-396	0
-18	396	0
394	-405	0
-394	405	0
394	-406	0
-394	406	0
-403	-410	0
404	-410	0
403	-411	0
-404	-411	0
-411	394	0
-410	394	0
177	-328	0
-177	328	0
177	-329	0
-177	329	0
-337	-177	0
-376	-177	0
-386	-177	0
22	-376	0
-22	376	0
22	-377	0
-22	377	0
234	-337	0
-234	337	0
234	-338	0
-234	338	0
-325	-416	0
323	-416	0
325	-417	0
-323	-417	0
-417	234	0
-416	234	0
85	-179	0
-85	179	0
85	-180	0
-85	180	0
-89	-85	0
-172	-85	0
-91	-85	0
23	-172	0
-23	172	0
23	-173	0
-23	173	0
82	-89	0
-82	89	0
82	-90	0
-82	90	0
-333	-428	0
84	-428	0
333	-429	0
-84	-429	0
-429	82	0
-428	82	0
181	-263	0
-181	263	0
181	-264	0
-181	264	0
248	181	0
-248	-181	0
233	-248	0
-233	248	0
233	-249	0
-233	249	0
-261	-233	0
-245	-233	0
-238	-233	0
33	-245	0
-33	245	0
33	-246	0
-33	246	0
236	-261	0
-236	261	0
236	-262	0
-236	262	0
-269	-420	0
259	-420	0
269	-421	0
-259	-421	0
-421	236	0
-420	236	0
-65	-60	0
-122	-60	0
-117	-60	0
-127	-60	0
63	-127	0
-63	127	0
63	-128	0
-63	128	0
63	-206	0
-63	206	0
-210	-63	0
-222	-63	0
-212	-63	0
29	-222	0
-29	222	0
29	-223	0
-29	223	0
40	-209	0
-40	209	0
40	-210	0
-40	210	0
-45	-430	0
80	-430	0
45	-431	0
-80	-431	0
-431	40	0
-430	40	0
62	-117	0
-62	117	0
62	-118	0
-62	118	0
62	-120	0
-62	120	0
-283	-62	0
-305	-62	0
-285	-62	0
31	-305	0
-31	305	0
31	-306	0
-31	306	0
280	-282	0
-280	282	0
280	-283	0
-280	283	0
-348	-412	0
349	-412	0
348	-413	0
-349	-413	0
-413	280	0
-412	280	0
61	-122	0
-61	122	0
61	-123	0
-61	123	0
-351	-61	0
-361	-61	0
-353	-61	0
20	-361	0
-20	361	0
20	-362	0
-20	362	0
109	-351	0
-109	351	0
109	-352	0
-109	352	0
-111	-424	0
112	-424	0
111	-425	0
-112	-425	0
-425	109	0
-424	109	0
52	-64	0
-52	64	0
52	-65	0
-52	65	0
-293	-52	0
-315	-52	0
-295	-52	0
288	-293	0
-288	293	0
288	-294	0
-288	294	0
-290	-418	0
291	-418	0
290	-419	0
-291	-419	0
-419	288	0
-418	288	0
2	-309	0
-2	309	0
2	-310	0
-2	310	0
58	-185	0
-58	185	0
58	-186	0
-58	186	0
58	-231	0
-58	231	0
58	-298	0
-58	298	0
58	-308	0
-58	308	0
58	-364	0
-58	364	0
58	-375	0
-58	375	0
58	-393	0
-58	393	0
49	58	0
59	58	0
54	58	0
-57	-54	0
-209	-57	0
-208	-57	0
226	208	0
215	208	0
213	-226	0
-213	226	0
213	-227	0
-213	227	0
14	213	0
-14	-213	0
126	125	0
-126	-125	0
-128	-126	0
-129	-126	0
206	205	0
207	205	0
-352	-56	0
-365	-56	0
-354	-56	0
8	-365	0
-8	365	0
8	-366	0
-8	366	0
-95	-59	0
-87	-59	0
-96	-59	0
336	96	0
346	336	0
-406	-346	0
-408	-346	0
-409	-346	0
3	-407	0
-3	407	0
3	-408	0
-3	408	0
-342	-341	0
-343	-341	0
-274	-273	0
-275	-273	0
78	-265	0
-78	265	0
78	-266	0
-78	266	0
78	-275	0
-78	275	0
98	78	0
-98	-78	0
277	274	0
-277	-274	0
379	335	0
382	335	0
381	379	0
-381	-379	0
1	-380	0
-1	380	0
1	-381	0
-1	381	0
-329	-414	0
330	-414	0
329	-415	0
-330	-415	0
-415	327	0
-414	327	0
-88	-87	0
-90	-87	0
-156	-87	0
-92	-87	0
16	-156	0
-16	156	0
16	-157	0
-16	157	0
-179	-426	0
94	-426	0
179	-427	0
-94	-427	0
-427	88	0
-426	88	0
106	95	0
-106	-95	0
-108	-106	0
-262	-108	0
-255	-108	0
257	255	0
258	255	0
251	-256	0
-251	256	0
251	-257	0
-251	257	0
13	251	0
-13	-251	0
264	260	0
266	260	0
249	247	0
250	247	0
-197	-107	0
-199	-107	0
-200	-107	0
36	-198	0
-36	198	0
36	-199	0
-36	199	0
-47	-49	0
48	47	0
-48	-47	0
115	48	0
-282	-115	0
-299	-115	0
-284	-115	0
24	-299	0
-24	299	0
24	-300	0
-24	300	0
-120	-114	0
-121	-114	0
116	113	0
-116	-113	0
118	116	0
119	116	0
-294	-51	0
-309	-51	0
-296	-51	0
229	74	0
230	74	0
66	-132	0
-66	132	0
66	-133	0
-66	133	0
66	-135	0
-66	135	0
66	-230	0
-66	230	0
216	66	0
-216	-66	0
-356	-216	0
363	356	0
-363	-356	0
-367	-363	0
131	-136	0
-131	136	0
131	-137	0
-131	137	0
131	-140	0
-131	140	0
131	-148	0
-131	148	0
131	-229	0
-131	229	0
302	131	0
297	131	0
-301	-297	0
146	71	0
141	71	0
149	71	0
-142	72	0
-142	149	0
-142	146	0
146	73	0
143	73	0
149	73	0
144	-149	0
-144	149	0
144	-150	0
-144	150	0
152	144	0
-152	-144	0
134	-151	0
-134	151	0
134	-152	0
-134	152	0
-240	-134	0
254	240	0
97	-224	0
-97	224	0
97	-225	0
-97	225	0
97	-252	0
-97	252	0
231	97	0
-231	-97	0
-163	-141	0
-160	142	0
-160	153	0
-154	-163	0
-160	-163	0
-163	-143	0
99	-162	0
-99	162	0
99	-163	0
-99	163	0
-100	-99	0
183	100	0
-183	-100	0
-192	-183	0
-158	-153	0
-174	160	0
-174	169	0
-318	166	0
-167	317	0
130	-145	0
-130	145	0
130	-146	0
-130	146	0
228	130	0
217	130	0
70	-76	0
-70	76	0
70	-77	0
-70	77	0
-339	-70	0
340	339	0
-340	-339	0
-397	-340	0
-384	-79	0
-387	-79	0
374	384	0
-374	-384	0
-432	435	0
-435	432	0
433	39	-37	0
434	-39	37	0
-432	434	433	0
37	79	67	0
-38	37	39	0
-38	-37	-39	0
39	79	69	0
-68	67	69	0
-68	-67	-69	0
-310	-308	-75	0
-371	-313	-312	0
-316	-314	-312	0
314	313	312	0
316	313	312	0
314	371	312	0
316	371	312	0
422	271	-195	0
423	-271	195	0
-189	423	422	0
279	369	370	0
43	110	46	0
41	219	211	0
44	358	355	0
194	202	203	0
391	400	401	0
322	389	390	0
83	320	321	0
237	242	239	0
287	372	373	0
410	403	-404	0
411	-403	404	0
-394	411	410	0
416	325	-323	0
417	-325	323	0
-234	417	416	0
428	333	-84	0
429	-333	84	0
-82	429	428	0
420	269	-259	0
421	-269	259	0
-236	421	420	0
430	45	-80	0
431	-45	80	0
-40	431	430	0
412	348	-349	0
413	-348	349	0
-280	413	412	0
424	111	-112	0
425	-111	112	0
-109	425	424	0
418	290	-291	0
419	-290	291	0
-288	419	418	0
-56	-55	-54	0
57	55	54	0
57	56	54	0
-125	-205	-57	0
-208	-226	-215	0
126	128	129	0
-205	-206	-207	0
124	123	55	0
-124	-123	55	0
-124	123	-55	0
124	-123	-55	0
-336	-327	-96	0
-336	-338	-96	0
-336	-335	-96	0
341	273	336	0
-346	-273	-336	0
-346	-341	-336	0
341	342	343	0
273	274	275	0
-335	-379	-382	0
414	329	-330	0
415	-329	330	0
-327	415	414	0
426	179	-94	0
427	-179	94	0
-88	427	426	0
-107	-103	-106	0
108	103	106	0
108	107	106	0
-260	-247	-108	0
-255	-257	-258	0
-260	-264	-266	0
-247	-249	-250	0
105	187	103	0
-105	-187	103	0
-105	187	-103	0
105	-187	-103	0
-51	-50	-49	0
47	50	49	0
47	51	49	0
114	113	48	0
-115	-113	-48	0
-115	-114	-48	0
114	120	121	0
-116	-118	-119	0
93	64	50	0
-93	-64	50	0
-93	64	-50	0
93	-64	-50	0
-74	-229	-230	0
-359	-357	-216	0
-362	-360	-216	0
-366	-364	-363	0
367	364	363	0
367	366	363	0
-131	-302	-297	0
-300	-298	-297	0
301	298	297	0
301	300	297	0
-368	-303	-302	0
-306	-304	-302	0
304	303	302	0
306	303	302	0
304	368	302	0
306	368	302	0
-72	71	73	0
-72	-71	-73	0
-243	-241	-134	0
-246	-244	-134	0
256	252	240	0
-254	-252	-240	0
-254	-256	-240	0
-153	-159	-141	0
163	159	141	0
163	153	141	0
-154	-155	161	0
-154	-153	159	0
-154	159	161	0
-142	141	143	0
-142	-141	-143	0
-153	-161	-143	0
163	161	143	0
163	153	143	0
-201	-101	-99	0
-190	-102	-99	0
-198	-186	-183	0
192	186	183	0
192	198	183	0
-157	-185	-153	0
158	185	153	0
158	157	153	0
-317	-166	-159	0
-173	-169	-159	0
169	166	159	0
173	166	159	0
169	317	159	0
173	317	159	0
-170	-171	175	0
-170	-169	173	0
-170	173	175	0
-174	-317	-166	0
-170	-317	-166	0
-160	159	161	0
-160	-159	-161	0
-317	-166	-161	0
-175	-169	-161	0
169	166	161	0
175	166	161	0
169	317	161	0
175	317	161	0
227	225	130	0
-220	-218	-217	0
-223	-221	-217	0
221	218	217	0
223	218	217	0
221	220	217	0
223	220	217	0
-399	-344	-70	0
-395	-345	-70	0
-407	-393	-340	0
397	393	340	0
397	407	340	0
-385	-388	-79	0
-375	-380	-374	0
-378	-377	-374	0
377	380	374	0
378	380	374	0
377	375	374	0
378	375	374	0
307	311	308	75	0
307	311	310	75	0
104	196	191	193	0
267	270	268	272	0
-268	-331	-324	-332	0
176	180	328	276	0
178	405	396	398	0
177	337	376	386	0
85	89	172	91	0
233	261	245	238	0
63	210	222	212	0
62	283	305	285	0
61	351	361	353	0
52	293	315	295	0
-58	-49	-59	-54	0
208	209	205	57	0
208	209	125	57	0
56	352	365	354	0
59	95	87	96	0
335	338	327	96	0
346	406	408	409	0
255	262	247	108	0
255	262	260	108	0
107	197	199	200	0
115	282	299	284	0
51	294	309	296	0
356	360	357	216	0
356	362	357	216	0
356	360	359	216	0
356	362	359	216	0
-71	-146	-141	-149	0
-73	-146	-143	-149	0
240	244	241	134	0
240	246	241	134	0
240	244	243	134	0
240	246	243	134	0
-164	-153	-165	-159	0
-164	-153	-163	-161	0
-164	-153	-159	-161	0
100	102	101	99	0
100	190	101	99	0
100	102	201	99	0
100	190	201	99	0
-318	-169	-319	-173	0
-318	-169	-317	-175	0
-318	-169	-173	-175	0
-167	-169	-168	-173	0
-167	-169	-166	-175	0
-167	-169	-173	-175	0
-217	-228	-225	-130	0
-217	-228	-227	-130	0
339	345	344	70	0
339	395	344	70	0
339	345	399	70	0
339	395	399	70	0
387	384	388	79	0
387	384	385	79	0
67	76	71	74	138	0
69	76	73	74	138	0
-53	-60	-263	-176	-182	0
-42	-286	-267	-43	-278	0
60	65	122	117	127	0
87	88	90	156	92	0
c :status unsat