1(define p3::bool)
2(define p4::bool)
3(define p5::bool)
4(define p6::bool)
5(define p7::bool)
6(define p8::bool)
7(define p9::bool)
8(define p10::bool)
9(define p11::bool)
10(define p12::bool)
11(define p13::bool)
12(define p14::bool)
13(define p15::bool)
14(define p16::bool)
15(define p17::bool)
16(define p18::bool)
17(define p19::bool)
18(define p20::bool)
19(define p21::bool)
20(define p22::bool)
21
22
23(define p23::bool)
24(define p24::bool)
25(define p25::bool)
26(define p26::bool)
27(define p27::bool)
28(define p28::bool)
29(define p29::bool)
30(define p30::bool)
31(define p31::bool)
32(define p32::bool)
33(define p33::bool)
34(define p34::bool)
35(define p35::bool)
36(define p36::bool)
37(define p37::bool)
38(define p38::bool)
39(define p39::bool)
40(define p40::bool)
41(define p41::bool)
42(define p42::bool)
43
44
45(define p44::bool)
46(define p45::bool)
47(define p46::bool)
48(define p47::bool)
49(define p48::bool)
50(define p49::bool)
51(define p50::bool)
52(define p51::bool)
53(define p52::bool)
54(define p53::bool)
55(define p54::bool)
56(define p55::bool)
57(define p56::bool)
58(define p57::bool)
59(define p58::bool)
60(define p59::bool)
61(define p60::bool)
62(define p61::bool)
63(define p62::bool)
64(define p63::bool)
65
66
67(define p64::bool)
68(define p65::bool)
69(define p66::bool)
70(define p67::bool)
71(define p68::bool)
72(define p69::bool)
73(define p70::bool)
74(define p71::bool)
75(define p72::bool)
76(define p73::bool)
77(define p74::bool)
78(define p75::bool)
79(define p76::bool)
80(define p77::bool)
81(define p78::bool)
82(define p79::bool)
83(define p80::bool)
84(define p81::bool)
85(define p82::bool)
86(define p83::bool)
87(define p84::bool)
88(define p85::bool)
89(define p86::bool)
90(define p87::bool)
91(define p88::bool)
92(define p89::bool)
93(define p90::bool)
94(define p91::bool)
95(define p92::bool)
96(define p93::bool)
97(define p94::bool)
98(define p95::bool)
99(define p96::bool)
100(define p97::bool)
101(define p98::bool)
102(define p99::bool)
103(define p100::bool)
104(define p101::bool)
105(define p102::bool)
106(define p103::bool)
107(define p104::bool)
108(define p105::bool)
109(define p106::bool)
110(define p107::bool)
111(define p108::bool)
112(define p109::bool)
113(define p110::bool)
114(define p111::bool)
115(define p112::bool)
116(define p113::bool)
117(define p114::bool)
118(define p115::bool)
119(define p116::bool)
120(define p117::bool)
121(define p118::bool)
122(define p119::bool)
123(define p120::bool)
124(define p121::bool)
125(define p122::bool)
126(define p123::bool)
127(define p124::bool)
128(define p125::bool)
129(define p126::bool)
130(define p127::bool)
131(define p128::bool)
132(define p129::bool)
133(define p130::bool)
134(define p131::bool)
135(define p132::bool)
136(define p133::bool)
137(define p134::bool)
138(define p135::bool)
139(define p136::bool)
140(define p137::bool)
141(define p138::bool)
142(define p139::bool)
143(define p140::bool)
144(define p141::bool)
145(define p142::bool)
146(define p143::bool)
147(define p144::bool)
148(define p145::bool)
149(define p146::bool)
150(define p147::bool)
151(define p148::bool)
152(define p149::bool)
153(define p150::bool)
154(define p151::bool)
155(define p152::bool)
156(define p153::bool)
157(define p154::bool)
158(define p155::bool)
159(define p156::bool)
160(define p157::bool)
161(define p158::bool)
162(define p159::bool)
163(define p160::bool)
164(define p161::bool)
165(define p162::bool)
166(define p163::bool)
167(define p164::bool)
168(define p165::bool)
169(define p166::bool)
170(define p167::bool)
171(define p168::bool)
172(define p169::bool)
173(define p170::bool)
174(define p171::bool)
175(define p172::bool)
176(define p173::bool)
177(define p174::bool)
178(define p175::bool)
179(define p176::bool)
180(define p177::bool)
181(define p178::bool)
182(define p179::bool)
183(define p180::bool)
184(define p181::bool)
185(define p182::bool)
186(define p183::bool)
187(define p184::bool)
188(define p185::bool)
189(define p186::bool)
190(define p187::bool)
191(define p188::bool)
192(define p189::bool)
193(define p190::bool)
194(define p191::bool)
195(define p192::bool)
196(define p193::bool)
197(define p194::bool)
198(define p195::bool)
199(define p196::bool)
200(define p197::bool)
201(define p198::bool)
202(define p199::bool)
203(define p200::bool)
204(define p201::bool)
205(define p202::bool)
206(define p203::bool)
207(define p204::bool)
208(define p205::bool)
209(define p206::bool)
210(define p207::bool)
211(define p208::bool)
212(define p209::bool)
213(define p210::bool)
214(define p211::bool)
215(define p212::bool)
216(define p213::bool)
217(define p214::bool)
218(define p215::bool)
219(define p216::bool)
220(define p217::bool)
221(define p218::bool)
222(define p219::bool)
223(define p220::bool)
224(define p221::bool)
225(define p222::bool)
226(define p223::bool)
227(define p224::bool)
228(define p225::bool)
229(define p226::bool)
230(define p227::bool)
231(define p228::bool)
232(define p229::bool)
233(define p230::bool)
234(define p231::bool)
235(define p232::bool)
236(define p233::bool)
237(define p234::bool)
238(define p235::bool)
239(define p236::bool)
240(define p237::bool)
241(define p238::bool)
242(define p239::bool)
243(define p240::bool)
244(define p241::bool)
245(define p242::bool)
246(define p243::bool)
247(define p244::bool)
248(define p245::bool)
249(define p246::bool)
250(define p247::bool)
251(define p248::bool)
252(define p249::bool)
253(define p250::bool)
254(define p251::bool)
255(define p252::bool)
256(define p253::bool)
257(define p254::bool)
258(define p255::bool)
259(define p256::bool)
260(define p257::bool)
261(define p258::bool)
262(define p259::bool)
263(define p260::bool)
264(define p261::bool)
265(define p262::bool)
266(define p263::bool)
267(define p264::bool)
268(define p265::bool)
269(define p266::bool)
270(define p267::bool)
271(define p268::bool)
272(define p269::bool)
273(define p270::bool)
274(define p271::bool)
275(define p272::bool)
276(define p273::bool)
277(define p274::bool)
278(define p275::bool)
279(define p276::bool)
280(define p277::bool)
281(define p278::bool)
282(define p279::bool)
283(define p280::bool)
284(define p281::bool)
285(define p282::bool)
286(define p283::bool)
287(define p284::bool)
288(define p285::bool)
289(define p286::bool)
290(define p287::bool)
291(define p288::bool)
292(define p289::bool)
293(define p290::bool)
294(define p291::bool)
295(define p292::bool)
296(define p293::bool)
297(define p294::bool)
298(define p295::bool)
299
300(assert (= p64 (= (not p3) p44)))
301(assert (= p65 (or (not p3) (not p44))))
302(assert (= p66 (= (not p4) p45)))
303(assert (= p67 (= (not p65) (not p66))))
304(assert (= p68 (or (not p45) p65)))
305(assert (= p69 (or (not p4) p65)))
306(assert (= p70 (or (not p4) (not p45))))
307(assert (= p71 (or (not p68) (not p69) (not p70))))
308(assert (= p72 (= (not p5) p46)))
309(assert (= p73 (= p71 (not p72))))
310(assert (= p74 (or (not p46) (not p71))))
311(assert (= p75 (or (not p5) (not p71))))
312(assert (= p76 (or (not p5) (not p46))))
313(assert (= p77 (or (not p74) (not p75) (not p76))))
314(assert (= p78 (= (not p6) p47)))
315(assert (= p79 (= p77 (not p78))))
316(assert (= p80 (or (not p47) (not p77))))
317(assert (= p81 (or (not p6) (not p77))))
318(assert (= p82 (or (not p6) (not p47))))
319(assert (= p83 (or (not p80) (not p81) (not p82))))
320(assert (= p84 (= (not p7) p48)))
321(assert (= p85 (= p83 (not p84))))
322(assert (= p86 (or (not p48) (not p83))))
323(assert (= p87 (or (not p7) (not p83))))
324(assert (= p88 (or (not p7) (not p48))))
325(assert (= p89 (or (not p86) (not p87) (not p88))))
326(assert (= p90 (= (not p8) p49)))
327(assert (= p91 (= p89 (not p90))))
328(assert (= p92 (or (not p49) (not p89))))
329(assert (= p93 (or (not p8) (not p89))))
330(assert (= p94 (or (not p8) (not p49))))
331(assert (= p95 (or (not p92) (not p93) (not p94))))
332(assert (= p96 (= (not p9) p50)))
333(assert (= p97 (= p95 (not p96))))
334(assert (= p98 (or (not p50) (not p95))))
335(assert (= p99 (or (not p9) (not p95))))
336(assert (= p100 (or (not p9) (not p50))))
337(assert (= p101 (or (not p98) (not p99) (not p100))))
338(assert (= p102 (= (not p10) p51)))
339(assert (= p103 (= p101 (not p102))))
340(assert (= p104 (or (not p51) (not p101))))
341(assert (= p105 (or (not p10) (not p101))))
342(assert (= p106 (or (not p10) (not p51))))
343(assert (= p107 (or (not p104) (not p105) (not p106))))
344(assert (= p108 (= (not p11) p52)))
345(assert (= p109 (= p107 (not p108))))
346(assert (= p110 (or (not p52) (not p107))))
347(assert (= p111 (or (not p11) (not p107))))
348(assert (= p112 (or (not p11) (not p52))))
349(assert (= p113 (or (not p110) (not p111) (not p112))))
350(assert (= p114 (= (not p12) p53)))
351(assert (= p115 (= p113 (not p114))))
352(assert (= p116 (or (not p53) (not p113))))
353(assert (= p117 (or (not p12) (not p113))))
354(assert (= p118 (or (not p12) (not p53))))
355(assert (= p119 (or (not p116) (not p117) (not p118))))
356(assert (= p120 (= (not p13) p54)))
357(assert (= p121 (= p119 (not p120))))
358(assert (= p122 (or (not p54) (not p119))))
359(assert (= p123 (or (not p13) (not p119))))
360(assert (= p124 (or (not p13) (not p54))))
361(assert (= p125 (or (not p122) (not p123) (not p124))))
362(assert (= p126 (= (not p14) p55)))
363(assert (= p127 (= p125 (not p126))))
364(assert (= p128 (or (not p55) (not p125))))
365(assert (= p129 (or (not p14) (not p125))))
366(assert (= p130 (or (not p14) (not p55))))
367(assert (= p131 (or (not p128) (not p129) (not p130))))
368(assert (= p132 (= (not p15) p56)))
369(assert (= p133 (= p131 (not p132))))
370(assert (= p134 (or (not p56) (not p131))))
371(assert (= p135 (or (not p15) (not p131))))
372(assert (= p136 (or (not p15) (not p56))))
373(assert (= p137 (or (not p134) (not p135) (not p136))))
374(assert (= p138 (= (not p16) p57)))
375(assert (= p139 (= p137 (not p138))))
376(assert (= p140 (or (not p57) (not p137))))
377(assert (= p141 (or (not p16) (not p137))))
378(assert (= p142 (or (not p16) (not p57))))
379(assert (= p143 (or (not p140) (not p141) (not p142))))
380(assert (= p144 (= (not p17) p58)))
381(assert (= p145 (= p143 (not p144))))
382(assert (= p146 (or (not p58) (not p143))))
383(assert (= p147 (or (not p17) (not p143))))
384(assert (= p148 (or (not p17) (not p58))))
385(assert (= p149 (or (not p146) (not p147) (not p148))))
386(assert (= p150 (= (not p18) p59)))
387(assert (= p151 (= p149 (not p150))))
388(assert (= p152 (or (not p59) (not p149))))
389(assert (= p153 (or (not p18) (not p149))))
390(assert (= p154 (or (not p18) (not p59))))
391(assert (= p155 (or (not p152) (not p153) (not p154))))
392(assert (= p156 (= (not p19) p60)))
393(assert (= p157 (= p155 (not p156))))
394(assert (= p158 (or (not p60) (not p155))))
395(assert (= p159 (or (not p19) (not p155))))
396(assert (= p160 (or (not p19) (not p60))))
397(assert (= p161 (or (not p158) (not p159) (not p160))))
398(assert (= p162 (= (not p20) p61)))
399(assert (= p163 (= p161 (not p162))))
400(assert (= p164 (or (not p61) (not p161))))
401(assert (= p165 (or (not p20) (not p161))))
402(assert (= p166 (or (not p20) (not p61))))
403(assert (= p167 (or (not p164) (not p165) (not p166))))
404(assert (= p168 (= (not p21) p62)))
405(assert (= p169 (= p167 (not p168))))
406(assert (= p170 (or (not p62) (not p167))))
407(assert (= p171 (or (not p21) (not p167))))
408(assert (= p172 (or (not p21) (not p62))))
409(assert (= p173 (or (not p170) (not p171) (not p172))))
410(assert (= p174 (= (not p22) p63)))
411(assert (= p175 (= p173 (not p174))))
412(assert (= p176 (or (not p63) (not p173))))
413(assert (= p177 (or (not p22) (not p173))))
414(assert (= p178 (or (not p22) (not p63))))
415(assert (= p179 (or (not p176) (not p177) (not p178))))
416(assert (= p180 (= (not p23) p44)))
417(assert (= p181 (or (not p23) (not p44))))
418(assert (= p182 (= (not p24) p45)))
419(assert (= p183 (= (not p181) (not p182))))
420(assert (= p184 (or (not p45) p181)))
421(assert (= p185 (or (not p24) p181)))
422(assert (= p186 (or (not p24) (not p45))))
423(assert (= p187 (or (not p184) (not p185) (not p186))))
424(assert (= p188 (= (not p25) p46)))
425(assert (= p189 (= p187 (not p188))))
426(assert (= p190 (or (not p46) (not p187))))
427(assert (= p191 (or (not p25) (not p187))))
428(assert (= p192 (or (not p25) (not p46))))
429(assert (= p193 (or (not p190) (not p191) (not p192))))
430(assert (= p194 (= (not p26) p47)))
431(assert (= p195 (= p193 (not p194))))
432(assert (= p196 (or (not p47) (not p193))))
433(assert (= p197 (or (not p26) (not p193))))
434(assert (= p198 (or (not p26) (not p47))))
435(assert (= p199 (or (not p196) (not p197) (not p198))))
436(assert (= p200 (= (not p27) p48)))
437(assert (= p201 (= p199 (not p200))))
438(assert (= p202 (or (not p48) (not p199))))
439(assert (= p203 (or (not p27) (not p199))))
440(assert (= p204 (or (not p27) (not p48))))
441(assert (= p205 (or (not p202) (not p203) (not p204))))
442(assert (= p206 (= (not p28) p49)))
443(assert (= p207 (= p205 (not p206))))
444(assert (= p208 (or (not p49) (not p205))))
445(assert (= p209 (or (not p28) (not p205))))
446(assert (= p210 (or (not p28) (not p49))))
447(assert (= p211 (or (not p208) (not p209) (not p210))))
448(assert (= p212 (= (not p29) p50)))
449(assert (= p213 (= p211 (not p212))))
450(assert (= p214 (or (not p50) (not p211))))
451(assert (= p215 (or (not p29) (not p211))))
452(assert (= p216 (or (not p29) (not p50))))
453(assert (= p217 (or (not p214) (not p215) (not p216))))
454(assert (= p218 (= (not p30) p51)))
455(assert (= p219 (= p217 (not p218))))
456(assert (= p220 (or (not p51) (not p217))))
457(assert (= p221 (or (not p30) (not p217))))
458(assert (= p222 (or (not p30) (not p51))))
459(assert (= p223 (or (not p220) (not p221) (not p222))))
460(assert (= p224 (= (not p31) p52)))
461(assert (= p225 (= p223 (not p224))))
462(assert (= p226 (or (not p52) (not p223))))
463(assert (= p227 (or (not p31) (not p223))))
464(assert (= p228 (or (not p31) (not p52))))
465(assert (= p229 (or (not p226) (not p227) (not p228))))
466(assert (= p230 (= (not p32) p53)))
467(assert (= p231 (= p229 (not p230))))
468(assert (= p232 (or (not p53) (not p229))))
469(assert (= p233 (or (not p32) (not p229))))
470(assert (= p234 (or (not p32) (not p53))))
471(assert (= p235 (or (not p232) (not p233) (not p234))))
472(assert (= p236 (= (not p33) p54)))
473(assert (= p237 (= p235 (not p236))))
474(assert (= p238 (or (not p54) (not p235))))
475(assert (= p239 (or (not p33) (not p235))))
476(assert (= p240 (or (not p33) (not p54))))
477(assert (= p241 (or (not p238) (not p239) (not p240))))
478(assert (= p242 (= (not p34) p55)))
479(assert (= p243 (= p241 (not p242))))
480(assert (= p244 (or (not p55) (not p241))))
481(assert (= p245 (or (not p34) (not p241))))
482(assert (= p246 (or (not p34) (not p55))))
483(assert (= p247 (or (not p244) (not p245) (not p246))))
484(assert (= p248 (= (not p35) p56)))
485(assert (= p249 (= p247 (not p248))))
486(assert (= p250 (or (not p56) (not p247))))
487(assert (= p251 (or (not p35) (not p247))))
488(assert (= p252 (or (not p35) (not p56))))
489(assert (= p253 (or (not p250) (not p251) (not p252))))
490(assert (= p254 (= (not p36) p57)))
491(assert (= p255 (= p253 (not p254))))
492(assert (= p256 (or (not p57) (not p253))))
493(assert (= p257 (or (not p36) (not p253))))
494(assert (= p258 (or (not p36) (not p57))))
495(assert (= p259 (or (not p256) (not p257) (not p258))))
496(assert (= p260 (= (not p37) p58)))
497(assert (= p261 (= p259 (not p260))))
498(assert (= p262 (or (not p58) (not p259))))
499(assert (= p263 (or (not p37) (not p259))))
500(assert (= p264 (or (not p37) (not p58))))
501(assert (= p265 (or (not p262) (not p263) (not p264))))
502(assert (= p266 (= (not p38) p59)))
503(assert (= p267 (= p265 (not p266))))
504(assert (= p268 (or (not p59) (not p265))))
505(assert (= p269 (or (not p38) (not p265))))
506(assert (= p270 (or (not p38) (not p59))))
507(assert (= p271 (or (not p268) (not p269) (not p270))))
508(assert (= p272 (= (not p39) p60)))
509(assert (= p273 (= p271 (not p272))))
510(assert (= p274 (or (not p60) (not p271))))
511(assert (= p275 (or (not p39) (not p271))))
512(assert (= p276 (or (not p39) (not p60))))
513(assert (= p277 (or (not p274) (not p275) (not p276))))
514(assert (= p278 (= (not p40) p61)))
515(assert (= p279 (= p277 (not p278))))
516(assert (= p280 (or (not p61) (not p277))))
517(assert (= p281 (or (not p40) (not p277))))
518(assert (= p282 (or (not p40) (not p61))))
519(assert (= p283 (or (not p280) (not p281) (not p282))))
520(assert (= p284 (= (not p41) p62)))
521(assert (= p285 (= p283 (not p284))))
522(assert (= p286 (or (not p62) (not p283))))
523(assert (= p287 (or (not p41) (not p283))))
524(assert (= p288 (or (not p41) (not p62))))
525(assert (= p289 (or (not p286) (not p287) (not p288))))
526(assert (= p290 (= (not p42) p63)))
527(assert (= p291 (= p289 (not p290))))
528(assert (= p292 (or (not p63) (not p289))))
529(assert (= p293 (or (not p42) (not p289))))
530(assert (= p294 (or (not p42) (not p63))))
531(assert (= p295 (or (not p292) (not p293) (not p294))))
532
533(assert (or p3 p65))
534(assert (or p4 p70))
535(assert (or p4 p69))
536(assert (or p5 p76))
537(assert (or p5 p75))
538(assert (or p6 p82))
539(assert (or p6 p81))
540(assert (or p7 p88))
541(assert (or p7 p87))
542(assert (or p8 p94))
543(assert (or p8 p93))
544(assert (or p9 p100))
545(assert (or p9 p99))
546(assert (or p10 p106))
547(assert (or p10 p105))
548(assert (or p11 p112))
549(assert (or p11 p111))
550(assert (or p12 p118))
551(assert (or p12 p117))
552(assert (or p13 p124))
553(assert (or p13 p123))
554(assert (or p14 p130))
555(assert (or p14 p129))
556(assert (or p15 p136))
557(assert (or p15 p135))
558(assert (or p16 p142))
559(assert (or p16 p141))
560(assert (or p17 p148))
561(assert (or p17 p147))
562(assert (or p18 p154))
563(assert (or p18 p153))
564(assert (or p19 p160))
565(assert (or p19 p159))
566(assert (or p20 p166))
567(assert (or p20 p165))
568(assert (or p21 p172))
569(assert (or p21 p171))
570(assert (or p22 p178))
571(assert (or p22 p177))
572(assert (or p23 p181))
573(assert (or p24 p186))
574(assert (or p24 p185))
575(assert (or p25 p192))
576(assert (or p25 p191))
577(assert (or p26 p198))
578(assert (or p26 p197))
579(assert (or p27 p204))
580(assert (or p27 p203))
581(assert (or p28 p210))
582(assert (or p28 p209))
583(assert (or p29 p216))
584(assert (or p29 p215))
585(assert (or p30 p222))
586(assert (or p30 p221))
587(assert (or p31 p228))
588(assert (or p31 p227))
589(assert (or p32 p234))
590(assert (or p32 p233))
591(assert (or p33 p240))
592(assert (or p33 p239))
593(assert (or p34 p246))
594(assert (or p34 p245))
595(assert (or p35 p252))
596(assert (or p35 p251))
597(assert (or p36 p258))
598(assert (or p36 p257))
599(assert (or p37 p264))
600(assert (or p37 p263))
601(assert (or p38 p270))
602(assert (or p38 p269))
603(assert (or p39 p276))
604(assert (or p39 p275))
605(assert (or p40 p282))
606(assert (or p40 p281))
607(assert (or p41 p288))
608(assert (or p41 p287))
609(assert (or p42 p294))
610(assert (or p42 p293))
611(assert (or p44 p181))
612(assert (or p44 p65))
613(assert (or p45 p186))
614(assert (or p45 p184))
615(assert (or p45 p70))
616(assert (or p45 p68))
617(assert (or p46 p192))
618(assert (or p46 p190))
619(assert (or p46 p76))
620(assert (or p46 p74))
621(assert (or p47 p198))
622(assert (or p47 p196))
623(assert (or p47 p82))
624(assert (or p47 p80))
625(assert (or p48 p204))
626(assert (or p48 p202))
627(assert (or p48 p88))
628(assert (or p48 p86))
629(assert (or p49 p210))
630(assert (or p49 p208))
631(assert (or p49 p94))
632(assert (or p49 p92))
633(assert (or p50 p216))
634(assert (or p50 p214))
635(assert (or p50 p100))
636(assert (or p50 p98))
637(assert (or p51 p222))
638(assert (or p51 p220))
639(assert (or p51 p106))
640(assert (or p51 p104))
641(assert (or p52 p228))
642(assert (or p52 p226))
643(assert (or p52 p112))
644(assert (or p52 p110))
645(assert (or p53 p234))
646(assert (or p53 p232))
647(assert (or p53 p118))
648(assert (or p53 p116))
649(assert (or p54 p240))
650(assert (or p54 p238))
651(assert (or p54 p124))
652(assert (or p54 p122))
653(assert (or p55 p246))
654(assert (or p55 p244))
655(assert (or p55 p130))
656(assert (or p55 p128))
657(assert (or p56 p252))
658(assert (or p56 p250))
659(assert (or p56 p136))
660(assert (or p56 p134))
661(assert (or p57 p258))
662(assert (or p57 p256))
663(assert (or p57 p142))
664(assert (or p57 p140))
665(assert (or p58 p264))
666(assert (or p58 p262))
667(assert (or p58 p148))
668(assert (or p58 p146))
669(assert (or p59 p270))
670(assert (or p59 p268))
671(assert (or p59 p154))
672(assert (or p59 p152))
673(assert (or p60 p276))
674(assert (or p60 p274))
675(assert (or p60 p160))
676(assert (or p60 p158))
677(assert (or p61 p282))
678(assert (or p61 p280))
679(assert (or p61 p166))
680(assert (or p61 p164))
681(assert (or p62 p288))
682(assert (or p62 p286))
683(assert (or p62 p172))
684(assert (or p62 p170))
685(assert (or p63 p294))
686(assert (or p63 p292))
687(assert (or p63 p178))
688(assert (or p63 p176))
689(assert (or (not p65) p69))
690(assert (or (not p65) p68))
691(assert (or p68 p71))
692(assert (or p69 p71))
693(assert (or p70 p71))
694(assert (or p71 p75))
695(assert (or p71 p74))
696(assert (or p74 p77))
697(assert (or p75 p77))
698(assert (or p76 p77))
699(assert (or p77 p81))
700(assert (or p77 p80))
701(assert (or p80 p83))
702(assert (or p81 p83))
703(assert (or p82 p83))
704(assert (or p83 p87))
705(assert (or p83 p86))
706(assert (or p86 p89))
707(assert (or p87 p89))
708(assert (or p88 p89))
709(assert (or p89 p93))
710(assert (or p89 p92))
711(assert (or p92 p95))
712(assert (or p93 p95))
713(assert (or p94 p95))
714(assert (or p95 p99))
715(assert (or p95 p98))
716(assert (or p98 p101))
717(assert (or p99 p101))
718(assert (or p100 p101))
719(assert (or p101 p105))
720(assert (or p101 p104))
721(assert (or p104 p107))
722(assert (or p105 p107))
723(assert (or p106 p107))
724(assert (or p107 p111))
725(assert (or p107 p110))
726(assert (or p110 p113))
727(assert (or p111 p113))
728(assert (or p112 p113))
729(assert (or p113 p117))
730(assert (or p113 p116))
731(assert (or p116 p119))
732(assert (or p117 p119))
733(assert (or p118 p119))
734(assert (or p119 p123))
735(assert (or p119 p122))
736(assert (or p122 p125))
737(assert (or p123 p125))
738(assert (or p124 p125))
739(assert (or p125 p129))
740(assert (or p125 p128))
741(assert (or p128 p131))
742(assert (or p129 p131))
743(assert (or p130 p131))
744(assert (or p131 p135))
745(assert (or p131 p134))
746(assert (or p134 p137))
747(assert (or p135 p137))
748(assert (or p136 p137))
749(assert (or p137 p141))
750(assert (or p137 p140))
751(assert (or p140 p143))
752(assert (or p141 p143))
753(assert (or p142 p143))
754(assert (or p143 p147))
755(assert (or p143 p146))
756(assert (or p146 p149))
757(assert (or p147 p149))
758(assert (or p148 p149))
759(assert (or p149 p153))
760(assert (or p149 p152))
761(assert (or p152 p155))
762(assert (or p153 p155))
763(assert (or p154 p155))
764(assert (or p155 p159))
765(assert (or p155 p158))
766(assert (or p158 p161))
767(assert (or p159 p161))
768(assert (or p160 p161))
769(assert (or p161 p165))
770(assert (or p161 p164))
771(assert (or p164 p167))
772(assert (or p165 p167))
773(assert (or p166 p167))
774(assert (or p167 p171))
775(assert (or p167 p170))
776(assert (or p170 p173))
777(assert (or p171 p173))
778(assert (or p172 p173))
779(assert (or p173 p177))
780(assert (or p173 p176))
781(assert (or p176 p179))
782(assert (or p177 p179))
783(assert (or p178 p179))
784(assert (or (not p181) p185))
785(assert (or (not p181) p184))
786(assert (or p184 p187))
787(assert (or p185 p187))
788(assert (or p186 p187))
789(assert (or p187 p191))
790(assert (or p187 p190))
791(assert (or p190 p193))
792(assert (or p191 p193))
793(assert (or p192 p193))
794(assert (or p193 p197))
795(assert (or p193 p196))
796(assert (or p196 p199))
797(assert (or p197 p199))
798(assert (or p198 p199))
799(assert (or p199 p203))
800(assert (or p199 p202))
801(assert (or p202 p205))
802(assert (or p203 p205))
803(assert (or p204 p205))
804(assert (or p205 p209))
805(assert (or p205 p208))
806(assert (or p208 p211))
807(assert (or p209 p211))
808(assert (or p210 p211))
809(assert (or p211 p215))
810(assert (or p211 p214))
811(assert (or p214 p217))
812(assert (or p215 p217))
813(assert (or p216 p217))
814(assert (or p217 p221))
815(assert (or p217 p220))
816(assert (or p220 p223))
817(assert (or p221 p223))
818(assert (or p222 p223))
819(assert (or p223 p227))
820(assert (or p223 p226))
821(assert (or p226 p229))
822(assert (or p227 p229))
823(assert (or p228 p229))
824(assert (or p229 p233))
825(assert (or p229 p232))
826(assert (or p232 p235))
827(assert (or p233 p235))
828(assert (or p234 p235))
829(assert (or p235 p239))
830(assert (or p235 p238))
831(assert (or p238 p241))
832(assert (or p239 p241))
833(assert (or p240 p241))
834(assert (or p241 p245))
835(assert (or p241 p244))
836(assert (or p244 p247))
837(assert (or p245 p247))
838(assert (or p246 p247))
839(assert (or p247 p251))
840(assert (or p247 p250))
841(assert (or p250 p253))
842(assert (or p251 p253))
843(assert (or p252 p253))
844(assert (or p253 p257))
845(assert (or p253 p256))
846(assert (or p256 p259))
847(assert (or p257 p259))
848(assert (or p258 p259))
849(assert (or p259 p263))
850(assert (or p259 p262))
851(assert (or p262 p265))
852(assert (or p263 p265))
853(assert (or p264 p265))
854(assert (or p265 p269))
855(assert (or p265 p268))
856(assert (or p268 p271))
857(assert (or p269 p271))
858(assert (or p270 p271))
859(assert (or p271 p275))
860(assert (or p271 p274))
861(assert (or p274 p277))
862(assert (or p275 p277))
863(assert (or p276 p277))
864(assert (or p277 p281))
865(assert (or p277 p280))
866(assert (or p280 p283))
867(assert (or p281 p283))
868(assert (or p282 p283))
869(assert (or p283 p287))
870(assert (or p283 p286))
871(assert (or p286 p289))
872(assert (or p287 p289))
873(assert (or p288 p289))
874(assert (or p289 p293))
875(assert (or p289 p292))
876(assert (or p292 p295))
877(assert (or p293 p295))
878(assert (or p294 p295))
879(assert (or (not p3) (not p44) (not p64)))
880(assert (or p3 p44 (not p64)))
881(assert (or (not p3) p44 p64))
882(assert (or p3 (not p44) p64))
883(assert (or (not p3) (not p44) (not p65)))
884(assert (or (not p4) (not p45) (not p66)))
885(assert (or p4 p45 (not p66)))
886(assert (or (not p4) p45 p66))
887(assert (or p4 (not p45) p66))
888(assert (or (not p65) p66 (not p67)))
889(assert (or p65 (not p66) (not p67)))
890(assert (or (not p65) (not p66) p67))
891(assert (or p65 p66 p67))
892(assert (or (not p45) p65 (not p68)))
893(assert (or (not p4) p65 (not p69)))
894(assert (or (not p4) (not p45) (not p70)))
895(assert (or (not p68) (not p69) (not p70) (not p71)))
896(assert (or (not p5) (not p46) (not p72)))
897(assert (or p5 p46 (not p72)))
898(assert (or (not p5) p46 p72))
899(assert (or p5 (not p46) p72))
900(assert (or p71 p72 (not p73)))
901(assert (or (not p71) (not p72) (not p73)))
902(assert (or p71 (not p72) p73))
903(assert (or (not p71) p72 p73))
904(assert (or (not p46) (not p71) (not p74)))
905(assert (or (not p5) (not p71) (not p75)))
906(assert (or (not p5) (not p46) (not p76)))
907(assert (or (not p74) (not p75) (not p76) (not p77)))
908(assert (or (not p6) (not p47) (not p78)))
909(assert (or p6 p47 (not p78)))
910(assert (or (not p6) p47 p78))
911(assert (or p6 (not p47) p78))
912(assert (or p77 p78 (not p79)))
913(assert (or (not p77) (not p78) (not p79)))
914(assert (or p77 (not p78) p79))
915(assert (or (not p77) p78 p79))
916(assert (or (not p47) (not p77) (not p80)))
917(assert (or (not p6) (not p77) (not p81)))
918(assert (or (not p6) (not p47) (not p82)))
919(assert (or (not p80) (not p81) (not p82) (not p83)))
920(assert (or (not p7) (not p48) (not p84)))
921(assert (or p7 p48 (not p84)))
922(assert (or (not p7) p48 p84))
923(assert (or p7 (not p48) p84))
924(assert (or p83 p84 (not p85)))
925(assert (or (not p83) (not p84) (not p85)))
926(assert (or p83 (not p84) p85))
927(assert (or (not p83) p84 p85))
928(assert (or (not p48) (not p83) (not p86)))
929(assert (or (not p7) (not p83) (not p87)))
930(assert (or (not p7) (not p48) (not p88)))
931(assert (or (not p86) (not p87) (not p88) (not p89)))
932(assert (or (not p8) (not p49) (not p90)))
933(assert (or p8 p49 (not p90)))
934(assert (or (not p8) p49 p90))
935(assert (or p8 (not p49) p90))
936(assert (or p89 p90 (not p91)))
937(assert (or (not p89) (not p90) (not p91)))
938(assert (or p89 (not p90) p91))
939(assert (or (not p89) p90 p91))
940(assert (or (not p49) (not p89) (not p92)))
941(assert (or (not p8) (not p89) (not p93)))
942(assert (or (not p8) (not p49) (not p94)))
943(assert (or (not p92) (not p93) (not p94) (not p95)))
944(assert (or (not p9) (not p50) (not p96)))
945(assert (or p9 p50 (not p96)))
946(assert (or (not p9) p50 p96))
947(assert (or p9 (not p50) p96))
948(assert (or p95 p96 (not p97)))
949(assert (or (not p95) (not p96) (not p97)))
950(assert (or p95 (not p96) p97))
951(assert (or (not p95) p96 p97))
952(assert (or (not p50) (not p95) (not p98)))
953(assert (or (not p9) (not p95) (not p99)))
954(assert (or (not p9) (not p50) (not p100)))
955(assert (or (not p98) (not p99) (not p100) (not p101)))
956(assert (or (not p10) (not p51) (not p102)))
957(assert (or p10 p51 (not p102)))
958(assert (or (not p10) p51 p102))
959(assert (or p10 (not p51) p102))
960(assert (or p101 p102 (not p103)))
961(assert (or (not p101) (not p102) (not p103)))
962(assert (or p101 (not p102) p103))
963(assert (or (not p101) p102 p103))
964(assert (or (not p51) (not p101) (not p104)))
965(assert (or (not p10) (not p101) (not p105)))
966(assert (or (not p10) (not p51) (not p106)))
967(assert (or (not p104) (not p105) (not p106) (not p107)))
968(assert (or (not p11) (not p52) (not p108)))
969(assert (or p11 p52 (not p108)))
970(assert (or (not p11) p52 p108))
971(assert (or p11 (not p52) p108))
972(assert (or p107 p108 (not p109)))
973(assert (or (not p107) (not p108) (not p109)))
974(assert (or p107 (not p108) p109))
975(assert (or (not p107) p108 p109))
976(assert (or (not p52) (not p107) (not p110)))
977(assert (or (not p11) (not p107) (not p111)))
978(assert (or (not p11) (not p52) (not p112)))
979(assert (or (not p110) (not p111) (not p112) (not p113)))
980(assert (or (not p12) (not p53) (not p114)))
981(assert (or p12 p53 (not p114)))
982(assert (or (not p12) p53 p114))
983(assert (or p12 (not p53) p114))
984(assert (or p113 p114 (not p115)))
985(assert (or (not p113) (not p114) (not p115)))
986(assert (or p113 (not p114) p115))
987(assert (or (not p113) p114 p115))
988(assert (or (not p53) (not p113) (not p116)))
989(assert (or (not p12) (not p113) (not p117)))
990(assert (or (not p12) (not p53) (not p118)))
991(assert (or (not p116) (not p117) (not p118) (not p119)))
992(assert (or (not p13) (not p54) (not p120)))
993(assert (or p13 p54 (not p120)))
994(assert (or (not p13) p54 p120))
995(assert (or p13 (not p54) p120))
996(assert (or p119 p120 (not p121)))
997(assert (or (not p119) (not p120) (not p121)))
998(assert (or p119 (not p120) p121))
999(assert (or (not p119) p120 p121))
1000(assert (or (not p54) (not p119) (not p122)))
1001(assert (or (not p13) (not p119) (not p123)))
1002(assert (or (not p13) (not p54) (not p124)))
1003(assert (or (not p122) (not p123) (not p124) (not p125)))
1004(assert (or (not p14) (not p55) (not p126)))
1005(assert (or p14 p55 (not p126)))
1006(assert (or (not p14) p55 p126))
1007(assert (or p14 (not p55) p126))
1008(assert (or p125 p126 (not p127)))
1009(assert (or (not p125) (not p126) (not p127)))
1010(assert (or p125 (not p126) p127))
1011(assert (or (not p125) p126 p127))
1012(assert (or (not p55) (not p125) (not p128)))
1013(assert (or (not p14) (not p125) (not p129)))
1014(assert (or (not p14) (not p55) (not p130)))
1015(assert (or (not p128) (not p129) (not p130) (not p131)))
1016(assert (or (not p15) (not p56) (not p132)))
1017(assert (or p15 p56 (not p132)))
1018(assert (or (not p15) p56 p132))
1019(assert (or p15 (not p56) p132))
1020(assert (or p131 p132 (not p133)))
1021(assert (or (not p131) (not p132) (not p133)))
1022(assert (or p131 (not p132) p133))
1023(assert (or (not p131) p132 p133))
1024(assert (or (not p56) (not p131) (not p134)))
1025(assert (or (not p15) (not p131) (not p135)))
1026(assert (or (not p15) (not p56) (not p136)))
1027(assert (or (not p134) (not p135) (not p136) (not p137)))
1028(assert (or (not p16) (not p57) (not p138)))
1029(assert (or p16 p57 (not p138)))
1030(assert (or (not p16) p57 p138))
1031(assert (or p16 (not p57) p138))
1032(assert (or p137 p138 (not p139)))
1033(assert (or (not p137) (not p138) (not p139)))
1034(assert (or p137 (not p138) p139))
1035(assert (or (not p137) p138 p139))
1036(assert (or (not p57) (not p137) (not p140)))
1037(assert (or (not p16) (not p137) (not p141)))
1038(assert (or (not p16) (not p57) (not p142)))
1039(assert (or (not p140) (not p141) (not p142) (not p143)))
1040(assert (or (not p17) (not p58) (not p144)))
1041(assert (or p17 p58 (not p144)))
1042(assert (or (not p17) p58 p144))
1043(assert (or p17 (not p58) p144))
1044(assert (or p143 p144 (not p145)))
1045(assert (or (not p143) (not p144) (not p145)))
1046(assert (or p143 (not p144) p145))
1047(assert (or (not p143) p144 p145))
1048(assert (or (not p58) (not p143) (not p146)))
1049(assert (or (not p17) (not p143) (not p147)))
1050(assert (or (not p17) (not p58) (not p148)))
1051(assert (or (not p146) (not p147) (not p148) (not p149)))
1052(assert (or (not p18) (not p59) (not p150)))
1053(assert (or p18 p59 (not p150)))
1054(assert (or (not p18) p59 p150))
1055(assert (or p18 (not p59) p150))
1056(assert (or p149 p150 (not p151)))
1057(assert (or (not p149) (not p150) (not p151)))
1058(assert (or p149 (not p150) p151))
1059(assert (or (not p149) p150 p151))
1060(assert (or (not p59) (not p149) (not p152)))
1061(assert (or (not p18) (not p149) (not p153)))
1062(assert (or (not p18) (not p59) (not p154)))
1063(assert (or (not p152) (not p153) (not p154) (not p155)))
1064(assert (or (not p19) (not p60) (not p156)))
1065(assert (or p19 p60 (not p156)))
1066(assert (or (not p19) p60 p156))
1067(assert (or p19 (not p60) p156))
1068(assert (or p155 p156 (not p157)))
1069(assert (or (not p155) (not p156) (not p157)))
1070(assert (or p155 (not p156) p157))
1071(assert (or (not p155) p156 p157))
1072(assert (or (not p60) (not p155) (not p158)))
1073(assert (or (not p19) (not p155) (not p159)))
1074(assert (or (not p19) (not p60) (not p160)))
1075(assert (or (not p158) (not p159) (not p160) (not p161)))
1076(assert (or (not p20) (not p61) (not p162)))
1077(assert (or p20 p61 (not p162)))
1078(assert (or (not p20) p61 p162))
1079(assert (or p20 (not p61) p162))
1080(assert (or p161 p162 (not p163)))
1081(assert (or (not p161) (not p162) (not p163)))
1082(assert (or p161 (not p162) p163))
1083(assert (or (not p161) p162 p163))
1084(assert (or (not p61) (not p161) (not p164)))
1085(assert (or (not p20) (not p161) (not p165)))
1086(assert (or (not p20) (not p61) (not p166)))
1087(assert (or (not p164) (not p165) (not p166) (not p167)))
1088(assert (or (not p21) (not p62) (not p168)))
1089(assert (or p21 p62 (not p168)))
1090(assert (or (not p21) p62 p168))
1091(assert (or p21 (not p62) p168))
1092(assert (or p167 p168 (not p169)))
1093(assert (or (not p167) (not p168) (not p169)))
1094(assert (or p167 (not p168) p169))
1095(assert (or (not p167) p168 p169))
1096(assert (or (not p62) (not p167) (not p170)))
1097(assert (or (not p21) (not p167) (not p171)))
1098(assert (or (not p21) (not p62) (not p172)))
1099(assert (or (not p170) (not p171) (not p172) (not p173)))
1100(assert (or (not p22) (not p63) (not p174)))
1101(assert (or p22 p63 (not p174)))
1102(assert (or (not p22) p63 p174))
1103(assert (or p22 (not p63) p174))
1104(assert (or p173 p174 (not p175)))
1105(assert (or (not p173) (not p174) (not p175)))
1106(assert (or p173 (not p174) p175))
1107(assert (or (not p173) p174 p175))
1108(assert (or (not p63) (not p173) (not p176)))
1109(assert (or (not p22) (not p173) (not p177)))
1110(assert (or (not p22) (not p63) (not p178)))
1111(assert (or (not p176) (not p177) (not p178) (not p179)))
1112(assert (or (not p23) (not p44) (not p180)))
1113(assert (or p23 p44 (not p180)))
1114(assert (or (not p23) p44 p180))
1115(assert (or p23 (not p44) p180))
1116(assert (or (not p23) (not p44) (not p181)))
1117(assert (or (not p24) (not p45) (not p182)))
1118(assert (or p24 p45 (not p182)))
1119(assert (or (not p24) p45 p182))
1120(assert (or p24 (not p45) p182))
1121(assert (or (not p181) p182 (not p183)))
1122(assert (or p181 (not p182) (not p183)))
1123(assert (or (not p181) (not p182) p183))
1124(assert (or p181 p182 p183))
1125(assert (or (not p45) p181 (not p184)))
1126(assert (or (not p24) p181 (not p185)))
1127(assert (or (not p24) (not p45) (not p186)))
1128(assert (or (not p184) (not p185) (not p186) (not p187)))
1129(assert (or (not p25) (not p46) (not p188)))
1130(assert (or p25 p46 (not p188)))
1131(assert (or (not p25) p46 p188))
1132(assert (or p25 (not p46) p188))
1133(assert (or p187 p188 (not p189)))
1134(assert (or (not p187) (not p188) (not p189)))
1135(assert (or p187 (not p188) p189))
1136(assert (or (not p187) p188 p189))
1137(assert (or (not p46) (not p187) (not p190)))
1138(assert (or (not p25) (not p187) (not p191)))
1139(assert (or (not p25) (not p46) (not p192)))
1140(assert (or (not p190) (not p191) (not p192) (not p193)))
1141(assert (or (not p26) (not p47) (not p194)))
1142(assert (or p26 p47 (not p194)))
1143(assert (or (not p26) p47 p194))
1144(assert (or p26 (not p47) p194))
1145(assert (or p193 p194 (not p195)))
1146(assert (or (not p193) (not p194) (not p195)))
1147(assert (or p193 (not p194) p195))
1148(assert (or (not p193) p194 p195))
1149(assert (or (not p47) (not p193) (not p196)))
1150(assert (or (not p26) (not p193) (not p197)))
1151(assert (or (not p26) (not p47) (not p198)))
1152(assert (or (not p196) (not p197) (not p198) (not p199)))
1153(assert (or (not p27) (not p48) (not p200)))
1154(assert (or p27 p48 (not p200)))
1155(assert (or (not p27) p48 p200))
1156(assert (or p27 (not p48) p200))
1157(assert (or p199 p200 (not p201)))
1158(assert (or (not p199) (not p200) (not p201)))
1159(assert (or p199 (not p200) p201))
1160(assert (or (not p199) p200 p201))
1161(assert (or (not p48) (not p199) (not p202)))
1162(assert (or (not p27) (not p199) (not p203)))
1163(assert (or (not p27) (not p48) (not p204)))
1164(assert (or (not p202) (not p203) (not p204) (not p205)))
1165(assert (or (not p28) (not p49) (not p206)))
1166(assert (or p28 p49 (not p206)))
1167(assert (or (not p28) p49 p206))
1168(assert (or p28 (not p49) p206))
1169(assert (or p205 p206 (not p207)))
1170(assert (or (not p205) (not p206) (not p207)))
1171(assert (or p205 (not p206) p207))
1172(assert (or (not p205) p206 p207))
1173(assert (or (not p49) (not p205) (not p208)))
1174(assert (or (not p28) (not p205) (not p209)))
1175(assert (or (not p28) (not p49) (not p210)))
1176(assert (or (not p208) (not p209) (not p210) (not p211)))
1177(assert (or (not p29) (not p50) (not p212)))
1178(assert (or p29 p50 (not p212)))
1179(assert (or (not p29) p50 p212))
1180(assert (or p29 (not p50) p212))
1181(assert (or p211 p212 (not p213)))
1182(assert (or (not p211) (not p212) (not p213)))
1183(assert (or p211 (not p212) p213))
1184(assert (or (not p211) p212 p213))
1185(assert (or (not p50) (not p211) (not p214)))
1186(assert (or (not p29) (not p211) (not p215)))
1187(assert (or (not p29) (not p50) (not p216)))
1188(assert (or (not p214) (not p215) (not p216) (not p217)))
1189(assert (or (not p30) (not p51) (not p218)))
1190(assert (or p30 p51 (not p218)))
1191(assert (or (not p30) p51 p218))
1192(assert (or p30 (not p51) p218))
1193(assert (or p217 p218 (not p219)))
1194(assert (or (not p217) (not p218) (not p219)))
1195(assert (or p217 (not p218) p219))
1196(assert (or (not p217) p218 p219))
1197(assert (or (not p51) (not p217) (not p220)))
1198(assert (or (not p30) (not p217) (not p221)))
1199(assert (or (not p30) (not p51) (not p222)))
1200(assert (or (not p220) (not p221) (not p222) (not p223)))
1201(assert (or (not p31) (not p52) (not p224)))
1202(assert (or p31 p52 (not p224)))
1203(assert (or (not p31) p52 p224))
1204(assert (or p31 (not p52) p224))
1205(assert (or p223 p224 (not p225)))
1206(assert (or (not p223) (not p224) (not p225)))
1207(assert (or p223 (not p224) p225))
1208(assert (or (not p223) p224 p225))
1209(assert (or (not p52) (not p223) (not p226)))
1210(assert (or (not p31) (not p223) (not p227)))
1211(assert (or (not p31) (not p52) (not p228)))
1212(assert (or (not p226) (not p227) (not p228) (not p229)))
1213(assert (or (not p32) (not p53) (not p230)))
1214(assert (or p32 p53 (not p230)))
1215(assert (or (not p32) p53 p230))
1216(assert (or p32 (not p53) p230))
1217(assert (or p229 p230 (not p231)))
1218(assert (or (not p229) (not p230) (not p231)))
1219(assert (or p229 (not p230) p231))
1220(assert (or (not p229) p230 p231))
1221(assert (or (not p53) (not p229) (not p232)))
1222(assert (or (not p32) (not p229) (not p233)))
1223(assert (or (not p32) (not p53) (not p234)))
1224(assert (or (not p232) (not p233) (not p234) (not p235)))
1225(assert (or (not p33) (not p54) (not p236)))
1226(assert (or p33 p54 (not p236)))
1227(assert (or (not p33) p54 p236))
1228(assert (or p33 (not p54) p236))
1229(assert (or p235 p236 (not p237)))
1230(assert (or (not p235) (not p236) (not p237)))
1231(assert (or p235 (not p236) p237))
1232(assert (or (not p235) p236 p237))
1233(assert (or (not p54) (not p235) (not p238)))
1234(assert (or (not p33) (not p235) (not p239)))
1235(assert (or (not p33) (not p54) (not p240)))
1236(assert (or (not p238) (not p239) (not p240) (not p241)))
1237(assert (or (not p34) (not p55) (not p242)))
1238(assert (or p34 p55 (not p242)))
1239(assert (or (not p34) p55 p242))
1240(assert (or p34 (not p55) p242))
1241(assert (or p241 p242 (not p243)))
1242(assert (or (not p241) (not p242) (not p243)))
1243(assert (or p241 (not p242) p243))
1244(assert (or (not p241) p242 p243))
1245(assert (or (not p55) (not p241) (not p244)))
1246(assert (or (not p34) (not p241) (not p245)))
1247(assert (or (not p34) (not p55) (not p246)))
1248(assert (or (not p244) (not p245) (not p246) (not p247)))
1249(assert (or (not p35) (not p56) (not p248)))
1250(assert (or p35 p56 (not p248)))
1251(assert (or (not p35) p56 p248))
1252(assert (or p35 (not p56) p248))
1253(assert (or p247 p248 (not p249)))
1254(assert (or (not p247) (not p248) (not p249)))
1255(assert (or p247 (not p248) p249))
1256(assert (or (not p247) p248 p249))
1257(assert (or (not p56) (not p247) (not p250)))
1258(assert (or (not p35) (not p247) (not p251)))
1259(assert (or (not p35) (not p56) (not p252)))
1260(assert (or (not p250) (not p251) (not p252) (not p253)))
1261(assert (or (not p36) (not p57) (not p254)))
1262(assert (or p36 p57 (not p254)))
1263(assert (or (not p36) p57 p254))
1264(assert (or p36 (not p57) p254))
1265(assert (or p253 p254 (not p255)))
1266(assert (or (not p253) (not p254) (not p255)))
1267(assert (or p253 (not p254) p255))
1268(assert (or (not p253) p254 p255))
1269(assert (or (not p57) (not p253) (not p256)))
1270(assert (or (not p36) (not p253) (not p257)))
1271(assert (or (not p36) (not p57) (not p258)))
1272(assert (or (not p256) (not p257) (not p258) (not p259)))
1273(assert (or (not p37) (not p58) (not p260)))
1274(assert (or p37 p58 (not p260)))
1275(assert (or (not p37) p58 p260))
1276(assert (or p37 (not p58) p260))
1277(assert (or p259 p260 (not p261)))
1278(assert (or (not p259) (not p260) (not p261)))
1279(assert (or p259 (not p260) p261))
1280(assert (or (not p259) p260 p261))
1281(assert (or (not p58) (not p259) (not p262)))
1282(assert (or (not p37) (not p259) (not p263)))
1283(assert (or (not p37) (not p58) (not p264)))
1284(assert (or (not p262) (not p263) (not p264) (not p265)))
1285(assert (or (not p38) (not p59) (not p266)))
1286(assert (or p38 p59 (not p266)))
1287(assert (or (not p38) p59 p266))
1288(assert (or p38 (not p59) p266))
1289(assert (or p265 p266 (not p267)))
1290(assert (or (not p265) (not p266) (not p267)))
1291(assert (or p265 (not p266) p267))
1292(assert (or (not p265) p266 p267))
1293(assert (or (not p59) (not p265) (not p268)))
1294(assert (or (not p38) (not p265) (not p269)))
1295(assert (or (not p38) (not p59) (not p270)))
1296(assert (or (not p268) (not p269) (not p270) (not p271)))
1297(assert (or (not p39) (not p60) (not p272)))
1298(assert (or p39 p60 (not p272)))
1299(assert (or (not p39) p60 p272))
1300(assert (or p39 (not p60) p272))
1301(assert (or p271 p272 (not p273)))
1302(assert (or (not p271) (not p272) (not p273)))
1303(assert (or p271 (not p272) p273))
1304(assert (or (not p271) p272 p273))
1305(assert (or (not p60) (not p271) (not p274)))
1306(assert (or (not p39) (not p271) (not p275)))
1307(assert (or (not p39) (not p60) (not p276)))
1308(assert (or (not p274) (not p275) (not p276) (not p277)))
1309(assert (or (not p40) (not p61) (not p278)))
1310(assert (or p40 p61 (not p278)))
1311(assert (or (not p40) p61 p278))
1312(assert (or p40 (not p61) p278))
1313(assert (or p277 p278 (not p279)))
1314(assert (or (not p277) (not p278) (not p279)))
1315(assert (or p277 (not p278) p279))
1316(assert (or (not p277) p278 p279))
1317(assert (or (not p61) (not p277) (not p280)))
1318(assert (or (not p40) (not p277) (not p281)))
1319(assert (or (not p40) (not p61) (not p282)))
1320(assert (or (not p280) (not p281) (not p282) (not p283)))
1321(assert (or (not p41) (not p62) (not p284)))
1322(assert (or p41 p62 (not p284)))
1323(assert (or (not p41) p62 p284))
1324(assert (or p41 (not p62) p284))
1325(assert (or p283 p284 (not p285)))
1326(assert (or (not p283) (not p284) (not p285)))
1327(assert (or p283 (not p284) p285))
1328(assert (or (not p283) p284 p285))
1329(assert (or (not p62) (not p283) (not p286)))
1330(assert (or (not p41) (not p283) (not p287)))
1331(assert (or (not p41) (not p62) (not p288)))
1332(assert (or (not p286) (not p287) (not p288) (not p289)))
1333(assert (or (not p42) (not p63) (not p290)))
1334(assert (or p42 p63 (not p290)))
1335(assert (or (not p42) p63 p290))
1336(assert (or p42 (not p63) p290))
1337(assert (or p289 p290 (not p291)))
1338(assert (or (not p289) (not p290) (not p291)))
1339(assert (or p289 (not p290) p291))
1340(assert (or (not p289) p290 p291))
1341(assert (or (not p63) (not p289) (not p292)))
1342(assert (or (not p42) (not p289) (not p293)))
1343(assert (or (not p42) (not p63) (not p294)))
1344(assert (or (not p292) (not p293) (not p294) (not p295)))
1345
1346(assert (and
1347(= p3 p23)
1348(= p4 p24)
1349(= p5 p25)
1350(= p6 p26)
1351(= p7 p27)
1352(= p8 p28)
1353(= p9 p29)
1354(= p10 p30)
1355(= p11 p31)
1356(= p12 p32)
1357(= p13 p33)
1358(= p14 p34)
1359(= p15 p35)
1360(= p16 p36)
1361(= p17 p37)
1362(= p18 p38)
1363(= p19 p39)
1364(= p20 p40)
1365(= p21 p41)
1366(= p22 p42)))
1367
1368(assert (not (and
1369(= p64 p180)
1370(= p67 p183)
1371(= p73 p189)
1372(= p79 p195)
1373(= p85 p201)
1374(= p91 p207)
1375(= p97 p213)
1376(= p103 p219)
1377(= p109 p225)
1378(= p115 p231)
1379(= p121 p237)
1380(= p127 p243)
1381(= p133 p249)
1382(= p139 p255)
1383(= p145 p261)
1384(= p151 p267)
1385(= p157 p273)
1386(= p163 p279)
1387(= p169 p285)
1388(= p175 p291))))
1389
1390(check)
1391