%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU198+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri May 19 12:02:37 EDT 2023
% Result : Theorem 2.87s 3.61s
% Output : Proof 2.87s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.25 % Problem : SEU198+2 : TPTP v8.1.2. Released v3.3.0.
% 0.12/0.26 % Command : nanocop.sh %s %d
% 0.12/0.48 % Computer : n016.cluster.edu
% 0.12/0.48 % Model : x86_64 x86_64
% 0.12/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.48 % Memory : 8042.1875MB
% 0.12/0.48 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.48 % CPULimit : 300
% 0.12/0.48 % WCLimit : 300
% 0.12/0.48 % DateTime : Thu May 18 13:07:26 EDT 2023
% 0.12/0.48 % CPUTime :
% 2.87/3.61
% 2.87/3.61 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 2.87/3.61 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.87/3.61 %-----------------------------------------------------
% 2.87/3.61 ncf(matrix, plain, [(2595 ^ _349219) ^ [] : [-(relation(2593 ^ []))], (2597 ^ _349219) ^ [] : [subset(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])], (2 ^ _349219) ^ [_349363] : [-(_349363 = _349363)], (4 ^ _349219) ^ [_349470, _349472] : [_349472 = _349470, -(_349470 = _349472)], (10 ^ _349219) ^ [_349674, _349676, _349678] : [-(_349678 = _349674), _349678 = _349676, _349676 = _349674], (20 ^ _349219) ^ [_350015, _350017, _350019, _350021] : [-(element(_350019, _350015)), element(_350021, _350017), _350021 = _350019, _350017 = _350015], (34 ^ _349219) ^ [_350459, _350461, _350463, _350465] : [-(proper_subset(_350463, _350459)), proper_subset(_350465, _350461), _350465 = _350463, _350461 = _350459], (48 ^ _349219) ^ [_350903, _350905, _350907, _350909] : [-(disjoint(_350907, _350903)), disjoint(_350909, _350905), _350909 = _350907, _350905 = _350903], (62 ^ _349219) ^ [_351319, _351321] : [-(empty(_351319)), _351321 = _351319, empty(_351321)], (72 ^ _349219) ^ [_351642, _351644, _351646, _351648] : [-(are_equipotent(_351646, _351642)), are_equipotent(_351648, _351644), _351648 = _351646, _351644 = _351642], (86 ^ _349219) ^ [_352086, _352088, _352090, _352092] : [-(in(_352090, _352086)), in(_352092, _352088), _352092 = _352090, _352088 = _352086], (100 ^ _349219) ^ [_352502, _352504] : [-(relation(_352502)), _352504 = _352502, relation(_352504)], (110 ^ _349219) ^ [_352805, _352807, _352809, _352811] : [-(subset(_352809, _352805)), subset(_352811, _352807), _352811 = _352809, _352807 = _352805], (124 ^ _349219) ^ [_353241, _353243] : [_353243 = _353241, -(set_meet(_353243) = set_meet(_353241))], (130 ^ _349219) ^ [_353487, _353489, _353491, _353493] : [-(cartesian_product2(_353493, _353489) = cartesian_product2(_353491, _353487)), _353493 = _353491, _353489 = _353487], (140 ^ _349219) ^ [_353818, _353820] : [_353820 = _353818, -(relation_field(_353820) = relation_field(_353818))], (146 ^ _349219) ^ [_354036, _354038] : [_354038 = _354036, -(relation_inverse(_354038) = relation_inverse(_354036))], (152 ^ _349219) ^ [_354282, _354284, _354286, _354288] : [-(union_of_subsets(_354288, _354284) = union_of_subsets(_354286, _354282)), _354288 = _354286, _354284 = _354282], (162 ^ _349219) ^ [_354641, _354643, _354645, _354647] : [-(complements_of_subsets(_354647, _354643) = complements_of_subsets(_354645, _354641)), _354647 = _354645, _354643 = _354641], (172 ^ _349219) ^ [_355028, _355030, _355032, _355034, _355036, _355038] : [-(subset_difference(_355038, _355034, _355030) = subset_difference(_355036, _355032, _355028)), _355038 = _355036, _355034 = _355032, _355030 = _355028], (186 ^ _349219) ^ [_355488, _355490] : [_355490 = _355488, -(cast_to_subset(_355490) = cast_to_subset(_355488))], (192 ^ _349219) ^ [_355734, _355736, _355738, _355740] : [-(meet_of_subsets(_355740, _355736) = meet_of_subsets(_355738, _355734)), _355740 = _355738, _355736 = _355734], (202 ^ _349219) ^ [_356093, _356095, _356097, _356099] : [-(subset_complement(_356099, _356095) = subset_complement(_356097, _356093)), _356099 = _356097, _356095 = _356093], (212 ^ _349219) ^ [_356452, _356454, _356456, _356458] : [-(ordered_pair(_356458, _356454) = ordered_pair(_356456, _356452)), _356458 = _356456, _356454 = _356452], (222 ^ _349219) ^ [_356811, _356813, _356815, _356817] : [-(set_difference(_356817, _356813) = set_difference(_356815, _356811)), _356817 = _356815, _356813 = _356811], (232 ^ _349219) ^ [_357170, _357172, _357174, _357176] : [-(set_union2(_357176, _357172) = set_union2(_357174, _357170)), _357176 = _357174, _357172 = _357170], (242 ^ _349219) ^ [_357529, _357531, _357533, _357535] : [-(set_intersection2(_357535, _357531) = set_intersection2(_357533, _357529)), _357535 = _357533, _357531 = _357529], (252 ^ _349219) ^ [_357860, _357862] : [_357862 = _357860, -(relation_dom(_357862) = relation_dom(_357860))], (258 ^ _349219) ^ [_358106, _358108, _358110, _358112] : [-(relation_composition(_358112, _358108) = relation_composition(_358110, _358106)), _358112 = _358110, _358108 = _358106], (268 ^ _349219) ^ [_358437, _358439] : [_358439 = _358437, -(identity_relation(_358439) = identity_relation(_358437))], (274 ^ _349219) ^ [_358683, _358685, _358687, _358689] : [-(relation_dom_restriction(_358689, _358685) = relation_dom_restriction(_358687, _358683)), _358689 = _358687, _358685 = _358683], (284 ^ _349219) ^ [_359014, _359016] : [_359016 = _359014, -(union(_359016) = union(_359014))], (290 ^ _349219) ^ [_359232, _359234] : [_359234 = _359232, -(powerset(_359234) = powerset(_359232))], (296 ^ _349219) ^ [_359450, _359452] : [_359452 = _359450, -(singleton(_359452) = singleton(_359450))], (302 ^ _349219) ^ [_359696, _359698, _359700, _359702] : [-(unordered_pair(_359702, _359698) = unordered_pair(_359700, _359696)), _359702 = _359700, _359698 = _359696], (312 ^ _349219) ^ [_360027, _360029] : [_360029 = _360027, -(relation_rng(_360029) = relation_rng(_360027))], (318 ^ _349219) ^ [_360253, _360255, _360257, _360259] : [-(relation_rng_restriction(_360259, _360255) = relation_rng_restriction(_360257, _360253)), _360259 = _360257, _360255 = _360253], (328 ^ _349219) ^ [_360692, _360694] : [in(_360694, _360692), in(_360692, _360694)], (334 ^ _349219) ^ [_360903, _360905] : [proper_subset(_360905, _360903), proper_subset(_360903, _360905)], (340 ^ _349219) ^ [_361100] : [empty(_361100), -(relation(_361100))], (346 ^ _349219) ^ [_361285, _361287] : [-(unordered_pair(_361287, _361285) = unordered_pair(_361285, _361287))], (348 ^ _349219) ^ [_361385, _361387] : [-(set_union2(_361387, _361385) = set_union2(_361385, _361387))], (350 ^ _349219) ^ [_361485, _361487] : [-(set_intersection2(_361487, _361485) = set_intersection2(_361485, _361487))], (352 ^ _349219) ^ [_361600, _361602] : [relation(_361600), 355 ^ _349219 : [(378 ^ _349219) ^ [] : [-(_361600 = identity_relation(_361602)), 391 ^ _349219 : [(392 ^ _349219) ^ [] : [-(in(379 ^ [_361600, _361602], _361602))], (394 ^ _349219) ^ [] : [-(379 ^ [_361600, _361602] = 380 ^ [_361600, _361602])], (396 ^ _349219) ^ [] : [in(ordered_pair(379 ^ [_361600, _361602], 380 ^ [_361600, _361602]), _361600)]], 383 ^ _349219 : [(384 ^ _349219) ^ [] : [-(in(ordered_pair(379 ^ [_361600, _361602], 380 ^ [_361600, _361602]), _361600))], (386 ^ _349219) ^ [] : [in(379 ^ [_361600, _361602], _361602), 379 ^ [_361600, _361602] = 380 ^ [_361600, _361602]]]], (356 ^ _349219) ^ [] : [_361600 = identity_relation(_361602), 359 ^ _349219 : [(360 ^ _349219) ^ [_361910, _361912] : [in(ordered_pair(_361912, _361910), _361600), 363 ^ _349219 : [(364 ^ _349219) ^ [] : [-(in(_361912, _361602))], (366 ^ _349219) ^ [] : [-(_361912 = _361910)]]], (368 ^ _349219) ^ [_362173, _362175] : [-(in(ordered_pair(_362175, _362173), _361600)), in(_362175, _361602), _362175 = _362173]]]]], (400 ^ _349219) ^ [_363281, _363283] : [_363283 = _363281, 403 ^ _349219 : [(404 ^ _349219) ^ [] : [-(subset(_363283, _363281))], (406 ^ _349219) ^ [] : [-(subset(_363281, _363283))]]], (408 ^ _349219) ^ [_363518, _363520] : [-(_363520 = _363518), subset(_363520, _363518), subset(_363518, _363520)], (418 ^ _349219) ^ [_363805] : [relation(_363805), 421 ^ _349219 : [(422 ^ _349219) ^ [_363991, _363993] : [relation(_363991), 425 ^ _349219 : [(448 ^ _349219) ^ [] : [-(_363991 = relation_dom_restriction(_363805, _363993)), 461 ^ _349219 : [(462 ^ _349219) ^ [] : [-(in(449 ^ [_363805, _363991, _363993], _363993))], (464 ^ _349219) ^ [] : [-(in(ordered_pair(449 ^ [_363805, _363991, _363993], 450 ^ [_363805, _363991, _363993]), _363805))], (466 ^ _349219) ^ [] : [in(ordered_pair(449 ^ [_363805, _363991, _363993], 450 ^ [_363805, _363991, _363993]), _363991)]], 453 ^ _349219 : [(454 ^ _349219) ^ [] : [-(in(ordered_pair(449 ^ [_363805, _363991, _363993], 450 ^ [_363805, _363991, _363993]), _363991))], (456 ^ _349219) ^ [] : [in(449 ^ [_363805, _363991, _363993], _363993), in(ordered_pair(449 ^ [_363805, _363991, _363993], 450 ^ [_363805, _363991, _363993]), _363805)]]], (426 ^ _349219) ^ [] : [_363991 = relation_dom_restriction(_363805, _363993), 429 ^ _349219 : [(430 ^ _349219) ^ [_364316, _364318] : [in(ordered_pair(_364318, _364316), _363991), 433 ^ _349219 : [(434 ^ _349219) ^ [] : [-(in(_364318, _363993))], (436 ^ _349219) ^ [] : [-(in(ordered_pair(_364318, _364316), _363805))]]], (438 ^ _349219) ^ [_364595, _364597] : [-(in(ordered_pair(_364597, _364595), _363991)), in(_364597, _363993), in(ordered_pair(_364597, _364595), _363805)]]]]]]], (470 ^ _349219) ^ [_365764, _365766] : [relation(_365764), 473 ^ _349219 : [(474 ^ _349219) ^ [_365935] : [relation(_365935), 477 ^ _349219 : [(500 ^ _349219) ^ [] : [-(_365935 = relation_rng_restriction(_365766, _365764)), 513 ^ _349219 : [(514 ^ _349219) ^ [] : [-(in(502 ^ [_365764, _365766, _365935], _365766))], (516 ^ _349219) ^ [] : [-(in(ordered_pair(501 ^ [_365764, _365766, _365935], 502 ^ [_365764, _365766, _365935]), _365764))], (518 ^ _349219) ^ [] : [in(ordered_pair(501 ^ [_365764, _365766, _365935], 502 ^ [_365764, _365766, _365935]), _365935)]], 505 ^ _349219 : [(506 ^ _349219) ^ [] : [-(in(ordered_pair(501 ^ [_365764, _365766, _365935], 502 ^ [_365764, _365766, _365935]), _365935))], (508 ^ _349219) ^ [] : [in(502 ^ [_365764, _365766, _365935], _365766), in(ordered_pair(501 ^ [_365764, _365766, _365935], 502 ^ [_365764, _365766, _365935]), _365764)]]], (478 ^ _349219) ^ [] : [_365935 = relation_rng_restriction(_365766, _365764), 481 ^ _349219 : [(482 ^ _349219) ^ [_366262, _366264] : [in(ordered_pair(_366264, _366262), _365935), 485 ^ _349219 : [(486 ^ _349219) ^ [] : [-(in(_366262, _365766))], (488 ^ _349219) ^ [] : [-(in(ordered_pair(_366264, _366262), _365764))]]], (490 ^ _349219) ^ [_366541, _366543] : [-(in(ordered_pair(_366543, _366541), _365935)), in(_366541, _365766), in(ordered_pair(_366543, _366541), _365764)]]]]]]], (534 ^ _349219) ^ [_368177] : [536 ^ _349219 : [(537 ^ _349219) ^ [] : [-(in(535 ^ [_368177], _368177))], (539 ^ _349219) ^ [_368414, _368416] : [535 ^ [_368177] = ordered_pair(_368416, _368414)]], -(relation(_368177))], (522 ^ _349219) ^ [_367716] : [relation(_367716), 525 ^ _349219 : [(526 ^ _349219) ^ [_367864] : [in(_367864, _367716), -(_367864 = ordered_pair(529 ^ [_367716, _367864], 530 ^ [_367716, _367864]))]]], (592 ^ _349219) ^ [_370312, _370314] : [_370314 = empty_set, 595 ^ _349219 : [(596 ^ _349219) ^ [] : [_370312 = set_meet(_370314), -(_370312 = empty_set)], (602 ^ _349219) ^ [] : [_370312 = empty_set, -(_370312 = set_meet(_370314))]]], (543 ^ _349219) ^ [_368605, _368607] : [-(_368607 = empty_set), 546 ^ _349219 : [(570 ^ _349219) ^ [] : [-(_368605 = set_meet(_368607)), 574 ^ _349219 : [(575 ^ _349219) ^ [] : [-(in(571 ^ [_368605, _368607], _368605))], (578 ^ _349219) ^ [] : [-(in(576 ^ [_368605, _368607], _368607))], (580 ^ _349219) ^ [] : [in(571 ^ [_368605, _368607], 576 ^ [_368605, _368607])]], 581 ^ _349219 : [(588 ^ _349219) ^ [] : [in(571 ^ [_368605, _368607], _368605)], (582 ^ _349219) ^ [_370007] : [in(_370007, _368607), -(in(571 ^ [_368605, _368607], _370007))]]], (547 ^ _349219) ^ [] : [_368605 = set_meet(_368607), 550 ^ _349219 : [(561 ^ _349219) ^ [_369233] : [563 ^ _349219 : [(564 ^ _349219) ^ [] : [-(in(562 ^ [_368605, _368607, _369233], _368607))], (566 ^ _349219) ^ [] : [in(_369233, 562 ^ [_368605, _368607, _369233])]], -(in(_369233, _368605))], (551 ^ _349219) ^ [_368903] : [in(_368903, _368605), 554 ^ _349219 : [(555 ^ _349219) ^ [_369048] : [in(_369048, _368607), -(in(_368903, _369048))]]]]]]], (624 ^ _349219) ^ [_371330, _371332] : [-(_371330 = singleton(_371332)), 628 ^ _349219 : [(629 ^ _349219) ^ [] : [-(in(625 ^ [_371330, _371332], _371330))], (631 ^ _349219) ^ [] : [625 ^ [_371330, _371332] = _371332]], 632 ^ _349219 : [(633 ^ _349219) ^ [] : [-(625 ^ [_371330, _371332] = _371332)], (635 ^ _349219) ^ [] : [in(625 ^ [_371330, _371332], _371330)]]], (608 ^ _349219) ^ [_370809, _370811] : [_370809 = singleton(_370811), 611 ^ _349219 : [(612 ^ _349219) ^ [_370979] : [in(_370979, _370809), -(_370979 = _370811)], (618 ^ _349219) ^ [_371151] : [_371151 = _370811, -(in(_371151, _370809))]]], (639 ^ _349219) ^ [_371881] : [_371881 = empty_set, 642 ^ _349219 : [(643 ^ _349219) ^ [_371994] : [in(_371994, _371881)]]], (645 ^ _349219) ^ [_372060] : [-(in(646 ^ [_372060], _372060)), -(_372060 = empty_set)], (668 ^ _349219) ^ [_372872, _372874] : [-(_372872 = powerset(_372874)), 672 ^ _349219 : [(673 ^ _349219) ^ [] : [-(in(669 ^ [_372872, _372874], _372872))], (675 ^ _349219) ^ [] : [subset(669 ^ [_372872, _372874], _372874)]], 676 ^ _349219 : [(677 ^ _349219) ^ [] : [-(subset(669 ^ [_372872, _372874], _372874))], (679 ^ _349219) ^ [] : [in(669 ^ [_372872, _372874], _372872)]]], (652 ^ _349219) ^ [_372351, _372353] : [_372351 = powerset(_372353), 655 ^ _349219 : [(656 ^ _349219) ^ [_372521] : [in(_372521, _372351), -(subset(_372521, _372353))], (662 ^ _349219) ^ [_372693] : [subset(_372693, _372353), -(in(_372693, _372351))]]], (683 ^ _349219) ^ [_373394] : [relation(_373394), 686 ^ _349219 : [(687 ^ _349219) ^ [_373552] : [relation(_373552), 690 ^ _349219 : [(707 ^ _349219) ^ [] : [-(_373394 = _373552), 712 ^ _349219 : [(713 ^ _349219) ^ [] : [-(in(ordered_pair(708 ^ [_373394, _373552], 709 ^ [_373394, _373552]), _373394))], (715 ^ _349219) ^ [] : [in(ordered_pair(708 ^ [_373394, _373552], 709 ^ [_373394, _373552]), _373552)]], 716 ^ _349219 : [(717 ^ _349219) ^ [] : [-(in(ordered_pair(708 ^ [_373394, _373552], 709 ^ [_373394, _373552]), _373552))], (719 ^ _349219) ^ [] : [in(ordered_pair(708 ^ [_373394, _373552], 709 ^ [_373394, _373552]), _373394)]]], (691 ^ _349219) ^ [] : [_373394 = _373552, 694 ^ _349219 : [(695 ^ _349219) ^ [_373857, _373859] : [in(ordered_pair(_373859, _373857), _373394), -(in(ordered_pair(_373859, _373857), _373552))], (701 ^ _349219) ^ [_374047, _374049] : [in(ordered_pair(_374049, _374047), _373552), -(in(ordered_pair(_374049, _374047), _373394))]]]]]]], (723 ^ _349219) ^ [_374884, _374886] : [-(empty(_374886)), 726 ^ _349219 : [(727 ^ _349219) ^ [] : [element(_374884, _374886), -(in(_374884, _374886))], (733 ^ _349219) ^ [] : [in(_374884, _374886), -(element(_374884, _374886))]]], (739 ^ _349219) ^ [_375297, _375299] : [empty(_375299), 742 ^ _349219 : [(743 ^ _349219) ^ [] : [element(_375297, _375299), -(empty(_375297))], (749 ^ _349219) ^ [] : [empty(_375297), -(element(_375297, _375299))]]], (777 ^ _349219) ^ [_376522, _376524, _376526] : [-(_376522 = unordered_pair(_376526, _376524)), 781 ^ _349219 : [(782 ^ _349219) ^ [] : [-(in(778 ^ [_376522, _376524, _376526], _376522))], (784 ^ _349219) ^ [] : [778 ^ [_376522, _376524, _376526] = _376526], (786 ^ _349219) ^ [] : [778 ^ [_376522, _376524, _376526] = _376524]], 787 ^ _349219 : [(794 ^ _349219) ^ [] : [in(778 ^ [_376522, _376524, _376526], _376522)], (788 ^ _349219) ^ [] : [-(778 ^ [_376522, _376524, _376526] = _376526), -(778 ^ [_376522, _376524, _376526] = _376524)]]], (755 ^ _349219) ^ [_375797, _375799, _375801] : [_375797 = unordered_pair(_375801, _375799), 758 ^ _349219 : [(769 ^ _349219) ^ [_376257] : [770 ^ _349219 : [(771 ^ _349219) ^ [] : [_376257 = _375801], (773 ^ _349219) ^ [] : [_376257 = _375799]], -(in(_376257, _375797))], (759 ^ _349219) ^ [_375979] : [in(_375979, _375797), -(_375979 = _375801), -(_375979 = _375799)]]], (820 ^ _349219) ^ [_378041, _378043, _378045] : [-(_378041 = set_union2(_378045, _378043)), 824 ^ _349219 : [(825 ^ _349219) ^ [] : [-(in(821 ^ [_378041, _378043, _378045], _378041))], (827 ^ _349219) ^ [] : [in(821 ^ [_378041, _378043, _378045], _378045)], (829 ^ _349219) ^ [] : [in(821 ^ [_378041, _378043, _378045], _378043)]], 830 ^ _349219 : [(837 ^ _349219) ^ [] : [in(821 ^ [_378041, _378043, _378045], _378041)], (831 ^ _349219) ^ [] : [-(in(821 ^ [_378041, _378043, _378045], _378045)), -(in(821 ^ [_378041, _378043, _378045], _378043))]]], (798 ^ _349219) ^ [_377316, _377318, _377320] : [_377316 = set_union2(_377320, _377318), 801 ^ _349219 : [(812 ^ _349219) ^ [_377776] : [813 ^ _349219 : [(814 ^ _349219) ^ [] : [in(_377776, _377320)], (816 ^ _349219) ^ [] : [in(_377776, _377318)]], -(in(_377776, _377316))], (802 ^ _349219) ^ [_377498] : [in(_377498, _377316), -(in(_377498, _377320)), -(in(_377498, _377318))]]], (871 ^ _349219) ^ [_380092, _380094, _380096] : [-(_380092 = cartesian_product2(_380096, _380094)), 889 ^ _349219 : [(890 ^ _349219) ^ [] : [-(in(887 ^ [_380092, _380094, _380096], _380096))], (892 ^ _349219) ^ [] : [-(in(888 ^ [_380092, _380094, _380096], _380094))], (894 ^ _349219) ^ [] : [-(872 ^ [_380092, _380094, _380096] = ordered_pair(887 ^ [_380092, _380094, _380096], 888 ^ [_380092, _380094, _380096]))], (896 ^ _349219) ^ [] : [in(872 ^ [_380092, _380094, _380096], _380092)]], 875 ^ _349219 : [(876 ^ _349219) ^ [] : [-(in(872 ^ [_380092, _380094, _380096], _380092))], (878 ^ _349219) ^ [_380430, _380432] : [in(_380432, _380096), in(_380430, _380094), 872 ^ [_380092, _380094, _380096] = ordered_pair(_380432, _380430)]]], (841 ^ _349219) ^ [_378835, _378837, _378839] : [_378835 = cartesian_product2(_378839, _378837), 844 ^ _349219 : [(845 ^ _349219) ^ [_379036] : [in(_379036, _378835), 850 ^ _349219 : [(851 ^ _349219) ^ [] : [-(in(848 ^ [_378835, _378837, _378839, _379036], _378839))], (853 ^ _349219) ^ [] : [-(in(849 ^ [_378835, _378837, _378839, _379036], _378837))], (855 ^ _349219) ^ [] : [-(_379036 = ordered_pair(848 ^ [_378835, _378837, _378839, _379036], 849 ^ [_378835, _378837, _378839, _379036]))]]], (857 ^ _349219) ^ [_379596] : [-(in(_379596, _378835)), 858 ^ _349219 : [(859 ^ _349219) ^ [_379726, _379728] : [in(_379728, _378839), in(_379726, _378837), _379596 = ordered_pair(_379728, _379726)]]]]], (900 ^ _349219) ^ [_381326] : [relation(_381326), 903 ^ _349219 : [(904 ^ _349219) ^ [_381484] : [relation(_381484), 907 ^ _349219 : [(918 ^ _349219) ^ [] : [921 ^ _349219 : [(922 ^ _349219) ^ [] : [-(in(ordered_pair(919 ^ [_381326, _381484], 920 ^ [_381326, _381484]), _381326))], (924 ^ _349219) ^ [] : [in(ordered_pair(919 ^ [_381326, _381484], 920 ^ [_381326, _381484]), _381484)]], -(subset(_381326, _381484))], (908 ^ _349219) ^ [] : [subset(_381326, _381484), 911 ^ _349219 : [(912 ^ _349219) ^ [_381760, _381762] : [in(ordered_pair(_381762, _381760), _381326), -(in(ordered_pair(_381762, _381760), _381484))]]]]]]], (938 ^ _349219) ^ [_382723, _382725] : [940 ^ _349219 : [(941 ^ _349219) ^ [] : [-(in(939 ^ [_382723, _382725], _382725))], (943 ^ _349219) ^ [] : [in(939 ^ [_382723, _382725], _382723)]], -(subset(_382725, _382723))], (928 ^ _349219) ^ [_382409, _382411] : [subset(_382411, _382409), 931 ^ _349219 : [(932 ^ _349219) ^ [_382546] : [in(_382546, _382411), -(in(_382546, _382409))]]], (969 ^ _349219) ^ [_383848, _383850, _383852] : [-(_383848 = set_intersection2(_383852, _383850)), 981 ^ _349219 : [(982 ^ _349219) ^ [] : [-(in(970 ^ [_383848, _383850, _383852], _383852))], (984 ^ _349219) ^ [] : [-(in(970 ^ [_383848, _383850, _383852], _383850))], (986 ^ _349219) ^ [] : [in(970 ^ [_383848, _383850, _383852], _383848)]], 973 ^ _349219 : [(974 ^ _349219) ^ [] : [-(in(970 ^ [_383848, _383850, _383852], _383848))], (976 ^ _349219) ^ [] : [in(970 ^ [_383848, _383850, _383852], _383852), in(970 ^ [_383848, _383850, _383852], _383850)]]], (947 ^ _349219) ^ [_383123, _383125, _383127] : [_383123 = set_intersection2(_383127, _383125), 950 ^ _349219 : [(951 ^ _349219) ^ [_383305] : [in(_383305, _383123), 954 ^ _349219 : [(955 ^ _349219) ^ [] : [-(in(_383305, _383127))], (957 ^ _349219) ^ [] : [-(in(_383305, _383125))]]], (959 ^ _349219) ^ [_383564] : [-(in(_383564, _383123)), in(_383564, _383127), in(_383564, _383125)]]], (990 ^ _349219) ^ [_384587] : [relation(_384587), 993 ^ _349219 : [(1011 ^ _349219) ^ [_385399] : [-(_385399 = relation_dom(_384587)), 1015 ^ _349219 : [(1016 ^ _349219) ^ [] : [-(in(1012 ^ [_384587, _385399], _385399))], (1018 ^ _349219) ^ [_385662] : [in(ordered_pair(1012 ^ [_384587, _385399], _385662), _384587)]], 1020 ^ _349219 : [(1021 ^ _349219) ^ [] : [-(in(ordered_pair(1012 ^ [_384587, _385399], 1019 ^ [_384587, _385399]), _384587))], (1023 ^ _349219) ^ [] : [in(1012 ^ [_384587, _385399], _385399)]]], (994 ^ _349219) ^ [_384768] : [_384768 = relation_dom(_384587), 997 ^ _349219 : [(998 ^ _349219) ^ [_384948] : [in(_384948, _384768), -(in(ordered_pair(_384948, 1001 ^ [_384587, _384768, _384948]), _384587))], (1005 ^ _349219) ^ [_385192] : [1006 ^ _349219 : [(1007 ^ _349219) ^ [_385271] : [in(ordered_pair(_385192, _385271), _384587)]], -(in(_385192, _384768))]]]]], (1027 ^ _349219) ^ [_386013] : [-(cast_to_subset(_386013) = _386013)], (1052 ^ _349219) ^ [_386996, _386998] : [-(_386996 = union(_386998)), 1065 ^ _349219 : [(1066 ^ _349219) ^ [] : [-(in(1053 ^ [_386996, _386998], 1064 ^ [_386996, _386998]))], (1068 ^ _349219) ^ [] : [-(in(1064 ^ [_386996, _386998], _386998))], (1070 ^ _349219) ^ [] : [in(1053 ^ [_386996, _386998], _386996)]], 1056 ^ _349219 : [(1057 ^ _349219) ^ [] : [-(in(1053 ^ [_386996, _386998], _386996))], (1059 ^ _349219) ^ [_387279] : [in(1053 ^ [_386996, _386998], _387279), in(_387279, _386998)]]], (1029 ^ _349219) ^ [_386151, _386153] : [_386151 = union(_386153), 1032 ^ _349219 : [(1033 ^ _349219) ^ [_386332] : [in(_386332, _386151), 1037 ^ _349219 : [(1038 ^ _349219) ^ [] : [-(in(_386332, 1036 ^ [_386151, _386153, _386332]))], (1040 ^ _349219) ^ [] : [-(in(1036 ^ [_386151, _386153, _386332], _386153))]]], (1042 ^ _349219) ^ [_386659] : [-(in(_386659, _386151)), 1043 ^ _349219 : [(1044 ^ _349219) ^ [_386757] : [in(_386659, _386757), in(_386757, _386153)]]]]], (1096 ^ _349219) ^ [_388617, _388619, _388621] : [-(_388617 = set_difference(_388621, _388619)), 1108 ^ _349219 : [(1109 ^ _349219) ^ [] : [-(in(1097 ^ [_388617, _388619, _388621], _388621))], (1111 ^ _349219) ^ [] : [in(1097 ^ [_388617, _388619, _388621], _388619)], (1113 ^ _349219) ^ [] : [in(1097 ^ [_388617, _388619, _388621], _388617)]], 1100 ^ _349219 : [(1101 ^ _349219) ^ [] : [-(in(1097 ^ [_388617, _388619, _388621], _388617))], (1103 ^ _349219) ^ [] : [in(1097 ^ [_388617, _388619, _388621], _388621), -(in(1097 ^ [_388617, _388619, _388621], _388619))]]], (1074 ^ _349219) ^ [_387886, _387888, _387890] : [_387886 = set_difference(_387890, _387888), 1077 ^ _349219 : [(1078 ^ _349219) ^ [_388070] : [in(_388070, _387886), 1081 ^ _349219 : [(1082 ^ _349219) ^ [] : [-(in(_388070, _387890))], (1084 ^ _349219) ^ [] : [in(_388070, _387888)]]], (1086 ^ _349219) ^ [_388330] : [-(in(_388330, _387886)), in(_388330, _387890), -(in(_388330, _387888))]]], (1117 ^ _349219) ^ [_389360] : [relation(_389360), 1120 ^ _349219 : [(1138 ^ _349219) ^ [_390172] : [-(_390172 = relation_rng(_389360)), 1142 ^ _349219 : [(1143 ^ _349219) ^ [] : [-(in(1139 ^ [_389360, _390172], _390172))], (1145 ^ _349219) ^ [_390435] : [in(ordered_pair(_390435, 1139 ^ [_389360, _390172]), _389360)]], 1147 ^ _349219 : [(1148 ^ _349219) ^ [] : [-(in(ordered_pair(1146 ^ [_389360, _390172], 1139 ^ [_389360, _390172]), _389360))], (1150 ^ _349219) ^ [] : [in(1139 ^ [_389360, _390172], _390172)]]], (1121 ^ _349219) ^ [_389541] : [_389541 = relation_rng(_389360), 1124 ^ _349219 : [(1125 ^ _349219) ^ [_389721] : [in(_389721, _389541), -(in(ordered_pair(1128 ^ [_389360, _389541, _389721], _389721), _389360))], (1132 ^ _349219) ^ [_389965] : [1133 ^ _349219 : [(1134 ^ _349219) ^ [_390044] : [in(ordered_pair(_390044, _389965), _389360)]], -(in(_389965, _389541))]]]]], (1154 ^ _349219) ^ [_390815, _390817] : [element(_390815, powerset(_390817)), -(subset_complement(_390817, _390815) = set_difference(_390817, _390815))], (1160 ^ _349219) ^ [_391026, _391028] : [-(ordered_pair(_391028, _391026) = unordered_pair(unordered_pair(_391028, _391026), singleton(_391028)))], (1162 ^ _349219) ^ [_391132] : [relation(_391132), -(relation_field(_391132) = set_union2(relation_dom(_391132), relation_rng(_391132)))], (1168 ^ _349219) ^ [_391338] : [relation(_391338), 1171 ^ _349219 : [(1172 ^ _349219) ^ [_391498] : [relation(_391498), 1175 ^ _349219 : [(1192 ^ _349219) ^ [] : [-(_391498 = relation_inverse(_391338)), 1197 ^ _349219 : [(1198 ^ _349219) ^ [] : [-(in(ordered_pair(1193 ^ [_391338, _391498], 1194 ^ [_391338, _391498]), _391498))], (1200 ^ _349219) ^ [] : [in(ordered_pair(1194 ^ [_391338, _391498], 1193 ^ [_391338, _391498]), _391338)]], 1201 ^ _349219 : [(1202 ^ _349219) ^ [] : [-(in(ordered_pair(1194 ^ [_391338, _391498], 1193 ^ [_391338, _391498]), _391338))], (1204 ^ _349219) ^ [] : [in(ordered_pair(1193 ^ [_391338, _391498], 1194 ^ [_391338, _391498]), _391498)]]], (1176 ^ _349219) ^ [] : [_391498 = relation_inverse(_391338), 1179 ^ _349219 : [(1180 ^ _349219) ^ [_391807, _391809] : [in(ordered_pair(_391809, _391807), _391498), -(in(ordered_pair(_391807, _391809), _391338))], (1186 ^ _349219) ^ [_391997, _391999] : [in(ordered_pair(_391997, _391999), _391338), -(in(ordered_pair(_391999, _391997), _391498))]]]]]]], (1208 ^ _349219) ^ [_392845, _392847] : [disjoint(_392847, _392845), -(set_intersection2(_392847, _392845) = empty_set)], (1214 ^ _349219) ^ [_393013, _393015] : [set_intersection2(_393015, _393013) = empty_set, -(disjoint(_393015, _393013))], (1220 ^ _349219) ^ [_393217] : [relation(_393217), 1223 ^ _349219 : [(1224 ^ _349219) ^ [_393402] : [relation(_393402), 1227 ^ _349219 : [(1228 ^ _349219) ^ [_393583] : [relation(_393583), 1231 ^ _349219 : [(1255 ^ _349219) ^ [] : [-(_393583 = relation_composition(_393217, _393402)), 1269 ^ _349219 : [(1270 ^ _349219) ^ [] : [-(in(ordered_pair(1256 ^ [_393217, _393402, _393583], 1268 ^ [_393217, _393402, _393583]), _393217))], (1272 ^ _349219) ^ [] : [-(in(ordered_pair(1268 ^ [_393217, _393402, _393583], 1257 ^ [_393217, _393402, _393583]), _393402))], (1274 ^ _349219) ^ [] : [in(ordered_pair(1256 ^ [_393217, _393402, _393583], 1257 ^ [_393217, _393402, _393583]), _393583)]], 1260 ^ _349219 : [(1261 ^ _349219) ^ [] : [-(in(ordered_pair(1256 ^ [_393217, _393402, _393583], 1257 ^ [_393217, _393402, _393583]), _393583))], (1263 ^ _349219) ^ [_395047] : [in(ordered_pair(1256 ^ [_393217, _393402, _393583], _395047), _393217), in(ordered_pair(_395047, 1257 ^ [_393217, _393402, _393583]), _393402)]]], (1232 ^ _349219) ^ [] : [_393583 = relation_composition(_393217, _393402), 1235 ^ _349219 : [(1236 ^ _349219) ^ [_393918, _393920] : [in(ordered_pair(_393920, _393918), _393583), 1240 ^ _349219 : [(1241 ^ _349219) ^ [] : [-(in(ordered_pair(_393920, 1239 ^ [_393217, _393402, _393583, _393918, _393920]), _393217))], (1243 ^ _349219) ^ [] : [-(in(ordered_pair(1239 ^ [_393217, _393402, _393583, _393918, _393920], _393918), _393402))]]], (1245 ^ _349219) ^ [_394303, _394305] : [-(in(ordered_pair(_394305, _394303), _393583)), 1246 ^ _349219 : [(1247 ^ _349219) ^ [_394416] : [in(ordered_pair(_394305, _394416), _393217), in(ordered_pair(_394416, _394303), _393402)]]]]]]]]]]], (1278 ^ _349219) ^ [_395733, _395735] : [element(_395733, powerset(powerset(_395735))), 1281 ^ _349219 : [(1282 ^ _349219) ^ [_395913] : [element(_395913, powerset(powerset(_395735))), 1285 ^ _349219 : [(1306 ^ _349219) ^ [] : [-(_395913 = complements_of_subsets(_395735, _395733)), 1308 ^ _349219 : [(1309 ^ _349219) ^ [] : [-(element(1307 ^ [_395733, _395735, _395913], powerset(_395735)))], (1311 ^ _349219) ^ [] : [1312 ^ _349219 : [(1313 ^ _349219) ^ [] : [-(in(1307 ^ [_395733, _395735, _395913], _395913))], (1315 ^ _349219) ^ [] : [in(subset_complement(_395735, 1307 ^ [_395733, _395735, _395913]), _395733)]], 1316 ^ _349219 : [(1317 ^ _349219) ^ [] : [-(in(subset_complement(_395735, 1307 ^ [_395733, _395735, _395913]), _395733))], (1319 ^ _349219) ^ [] : [in(1307 ^ [_395733, _395735, _395913], _395913)]]]]], (1286 ^ _349219) ^ [] : [_395913 = complements_of_subsets(_395735, _395733), 1289 ^ _349219 : [(1290 ^ _349219) ^ [_396201] : [element(_396201, powerset(_395735)), 1293 ^ _349219 : [(1294 ^ _349219) ^ [] : [in(_396201, _395913), -(in(subset_complement(_395735, _396201), _395733))], (1300 ^ _349219) ^ [] : [in(subset_complement(_395735, _396201), _395733), -(in(_396201, _395913))]]]]]]]]], (1323 ^ _349219) ^ [_397324, _397326] : [proper_subset(_397326, _397324), 1326 ^ _349219 : [(1327 ^ _349219) ^ [] : [-(subset(_397326, _397324))], (1329 ^ _349219) ^ [] : [_397326 = _397324]]], (1331 ^ _349219) ^ [_397562, _397564] : [-(proper_subset(_397564, _397562)), subset(_397564, _397562), -(_397564 = _397562)], (1341 ^ _349219) ^ [] : [true___, -(true___)], (1347 ^ _349219) ^ [] : [true___, -(true___)], (1353 ^ _349219) ^ [] : [true___, -(true___)], (1359 ^ _349219) ^ [] : [true___, -(true___)], (1365 ^ _349219) ^ [] : [true___, -(true___)], (1371 ^ _349219) ^ [] : [true___, -(true___)], (1377 ^ _349219) ^ [_398551] : [-(element(cast_to_subset(_398551), powerset(_398551)))], (1379 ^ _349219) ^ [] : [true___, -(true___)], (1385 ^ _349219) ^ [] : [true___, -(true___)], (1391 ^ _349219) ^ [] : [true___, -(true___)], (1397 ^ _349219) ^ [] : [true___, -(true___)], (1403 ^ _349219) ^ [_399138, _399140] : [element(_399138, powerset(_399140)), -(element(subset_complement(_399140, _399138), powerset(_399140)))], (1409 ^ _349219) ^ [] : [true___, -(true___)], (1415 ^ _349219) ^ [] : [true___, -(true___)], (1421 ^ _349219) ^ [_399586] : [relation(_399586), -(relation(relation_inverse(_399586)))], (1427 ^ _349219) ^ [] : [true___, -(true___)], (1433 ^ _349219) ^ [] : [true___, -(true___)], (1439 ^ _349219) ^ [_400028, _400030] : [-(relation(relation_composition(_400030, _400028))), relation(_400030), relation(_400028)], (1449 ^ _349219) ^ [_400327, _400329] : [element(_400327, powerset(powerset(_400329))), -(element(union_of_subsets(_400329, _400327), powerset(_400329)))], (1455 ^ _349219) ^ [_400526] : [-(relation(identity_relation(_400526)))], (1457 ^ _349219) ^ [_400634, _400636] : [element(_400634, powerset(powerset(_400636))), -(element(meet_of_subsets(_400636, _400634), powerset(_400636)))], (1463 ^ _349219) ^ [_400876, _400878, _400880] : [-(element(subset_difference(_400880, _400878, _400876), powerset(_400880))), element(_400878, powerset(_400880)), element(_400876, powerset(_400880))], (1473 ^ _349219) ^ [_401205, _401207] : [relation(_401207), -(relation(relation_dom_restriction(_401207, _401205)))], (1479 ^ _349219) ^ [_401417, _401419] : [element(_401417, powerset(powerset(_401419))), -(element(complements_of_subsets(_401419, _401417), powerset(powerset(_401419))))], (1485 ^ _349219) ^ [_401649, _401651] : [relation(_401649), -(relation(relation_rng_restriction(_401651, _401649)))], (1491 ^ _349219) ^ [] : [true___, -(true___)], (1498 ^ _349219) ^ [_401990] : [-(element(1496 ^ [_401990], _401990))], (1500 ^ _349219) ^ [_402102, _402104] : [1507 ^ _349219 : [(1508 ^ _349219) ^ [] : [-(empty(relation_composition(_402102, _402104)))], (1510 ^ _349219) ^ [] : [-(relation(relation_composition(_402102, _402104)))]], empty(_402104), relation(_402102)], (1512 ^ _349219) ^ [_402480, _402482] : [-(relation(set_intersection2(_402482, _402480))), relation(_402482), relation(_402480)], (1522 ^ _349219) ^ [_402749] : [empty(powerset(_402749))], (1524 ^ _349219) ^ [] : [-(empty(empty_set))], (1526 ^ _349219) ^ [_402894, _402896] : [empty(ordered_pair(_402896, _402894))], (1528 ^ _349219) ^ [_403005, _403007] : [-(relation(set_union2(_403007, _403005))), relation(_403007), relation(_403005)], (1538 ^ _349219) ^ [_403274] : [empty(singleton(_403274))], (1540 ^ _349219) ^ [_403382, _403384] : [-(empty(_403384)), empty(set_union2(_403384, _403382))], (1546 ^ _349219) ^ [_403582, _403584] : [empty(unordered_pair(_403584, _403582))], (1548 ^ _349219) ^ [_403693, _403695] : [-(empty(_403695)), empty(set_union2(_403693, _403695))], (1554 ^ _349219) ^ [] : [-(empty(empty_set))], (1556 ^ _349219) ^ [] : [-(relation(empty_set))], (1558 ^ _349219) ^ [_404017, _404019] : [empty(cartesian_product2(_404019, _404017)), -(empty(_404019)), -(empty(_404017))], (1568 ^ _349219) ^ [_404309] : [empty(relation_dom(_404309)), -(empty(_404309)), relation(_404309)], (1578 ^ _349219) ^ [_404586] : [empty(relation_rng(_404586)), -(empty(_404586)), relation(_404586)], (1588 ^ _349219) ^ [_404863] : [empty(_404863), 1591 ^ _349219 : [(1592 ^ _349219) ^ [] : [-(empty(relation_dom(_404863)))], (1594 ^ _349219) ^ [] : [-(relation(relation_dom(_404863)))]]], (1596 ^ _349219) ^ [_405128] : [empty(_405128), 1599 ^ _349219 : [(1600 ^ _349219) ^ [] : [-(empty(relation_rng(_405128)))], (1602 ^ _349219) ^ [] : [-(relation(relation_rng(_405128)))]]], (1604 ^ _349219) ^ [_405407, _405409] : [1611 ^ _349219 : [(1612 ^ _349219) ^ [] : [-(empty(relation_composition(_405409, _405407)))], (1614 ^ _349219) ^ [] : [-(relation(relation_composition(_405409, _405407)))]], empty(_405409), relation(_405407)], (1616 ^ _349219) ^ [_405770, _405772] : [-(set_union2(_405772, _405772) = _405772)], (1618 ^ _349219) ^ [_405867, _405869] : [-(set_intersection2(_405869, _405869) = _405869)], (1620 ^ _349219) ^ [_405979, _405981] : [element(_405979, powerset(_405981)), -(subset_complement(_405981, subset_complement(_405981, _405979)) = _405979)], (1626 ^ _349219) ^ [_406191] : [relation(_406191), -(relation_inverse(relation_inverse(_406191)) = _406191)], (1632 ^ _349219) ^ [_406401, _406403] : [element(_406401, powerset(powerset(_406403))), -(complements_of_subsets(_406403, complements_of_subsets(_406403, _406401)) = _406401)], (1638 ^ _349219) ^ [_406615, _406617] : [proper_subset(_406617, _406617)], (1640 ^ _349219) ^ [_406694] : [singleton(_406694) = empty_set], (1642 ^ _349219) ^ [_406803, _406805] : [in(_406805, _406803), -(set_union2(singleton(_406805), _406803) = _406803)], (1648 ^ _349219) ^ [_407023, _407025] : [disjoint(singleton(_407025), _407023), in(_407025, _407023)], (1654 ^ _349219) ^ [_407236, _407238] : [-(in(_407238, _407236)), -(disjoint(singleton(_407238), _407236))], (1660 ^ _349219) ^ [_407482, _407484] : [subset(singleton(_407484), _407482), -(in(_407484, _407482))], (1666 ^ _349219) ^ [_407648, _407650] : [in(_407650, _407648), -(subset(singleton(_407650), _407648))], (1672 ^ _349219) ^ [_407893, _407895] : [set_difference(_407895, _407893) = empty_set, -(subset(_407895, _407893))], (1678 ^ _349219) ^ [_408061, _408063] : [subset(_408063, _408061), -(set_difference(_408063, _408061) = empty_set)], (1684 ^ _349219) ^ [_408279, _408281] : [element(_408279, powerset(_408281)), 1687 ^ _349219 : [(1688 ^ _349219) ^ [_408420] : [in(_408420, _408279), -(in(_408420, _408281))]]], (1694 ^ _349219) ^ [_408659, _408661, _408663] : [subset(_408663, _408661), -(in(_408659, _408663)), -(subset(_408663, set_difference(_408661, singleton(_408659))))], (1714 ^ _349219) ^ [_409268, _409270] : [1715 ^ _349219 : [(1716 ^ _349219) ^ [] : [_409270 = empty_set], (1718 ^ _349219) ^ [] : [_409270 = singleton(_409268)]], -(subset(_409270, singleton(_409268)))], (1704 ^ _349219) ^ [_409008, _409010] : [subset(_409010, singleton(_409008)), -(_409010 = empty_set), -(_409010 = singleton(_409008))], (1722 ^ _349219) ^ [_409562, _409564] : [in(_409564, _409562), -(subset(_409564, union(_409562)))], (1728 ^ _349219) ^ [_409833, _409835, _409837, _409839] : [in(ordered_pair(_409839, _409837), cartesian_product2(_409835, _409833)), 1731 ^ _349219 : [(1732 ^ _349219) ^ [] : [-(in(_409839, _409835))], (1734 ^ _349219) ^ [] : [-(in(_409837, _409833))]]], (1736 ^ _349219) ^ [_410098, _410100, _410102, _410104] : [-(in(ordered_pair(_410104, _410102), cartesian_product2(_410100, _410098))), in(_410104, _410100), in(_410102, _410098)], (1746 ^ _349219) ^ [_410431, _410433] : [1748 ^ _349219 : [(1749 ^ _349219) ^ [] : [-(in(1747 ^ [_410431, _410433], _410433))], (1751 ^ _349219) ^ [] : [in(1747 ^ [_410431, _410433], _410431)]], -(element(_410433, powerset(_410431)))], (1756 ^ _349219) ^ [] : [-(empty(1754 ^ []))], (1758 ^ _349219) ^ [] : [-(relation(1754 ^ []))], (1760 ^ _349219) ^ [_410925] : [-(empty(_410925)), 1764 ^ _349219 : [(1765 ^ _349219) ^ [] : [-(element(1763 ^ [_410925], powerset(_410925)))], (1767 ^ _349219) ^ [] : [empty(1763 ^ [_410925])]]], (1770 ^ _349219) ^ [] : [-(empty(1768 ^ []))], (1773 ^ _349219) ^ [] : [empty(1771 ^ [])], (1775 ^ _349219) ^ [] : [-(relation(1771 ^ []))], (1778 ^ _349219) ^ [_411547] : [-(element(1776 ^ [_411547], powerset(_411547)))], (1780 ^ _349219) ^ [_411598] : [-(empty(1776 ^ [_411598]))], (1783 ^ _349219) ^ [] : [empty(1781 ^ [])], (1785 ^ _349219) ^ [_411801, _411803] : [element(_411801, powerset(powerset(_411803))), -(union_of_subsets(_411803, _411801) = union(_411801))], (1791 ^ _349219) ^ [_412029, _412031] : [element(_412029, powerset(powerset(_412031))), -(meet_of_subsets(_412031, _412029) = set_meet(_412029))], (1797 ^ _349219) ^ [_412271, _412273, _412275] : [-(subset_difference(_412275, _412273, _412271) = set_difference(_412273, _412271)), element(_412273, powerset(_412275)), element(_412271, powerset(_412275))], (1807 ^ _349219) ^ [_412587, _412589] : [-(subset(_412589, _412589))], (1809 ^ _349219) ^ [_412696, _412698] : [disjoint(_412698, _412696), -(disjoint(_412696, _412698))], (1815 ^ _349219) ^ [_412963, _412965, _412967, _412969] : [in(ordered_pair(_412969, _412967), cartesian_product2(_412965, _412963)), 1818 ^ _349219 : [(1819 ^ _349219) ^ [] : [-(in(_412969, _412965))], (1821 ^ _349219) ^ [] : [-(in(_412967, _412963))]]], (1823 ^ _349219) ^ [_413228, _413230, _413232, _413234] : [-(in(ordered_pair(_413234, _413232), cartesian_product2(_413230, _413228))), in(_413234, _413230), in(_413232, _413228)], (1833 ^ _349219) ^ [_413589, _413591, _413593, _413595] : [unordered_pair(_413595, _413593) = unordered_pair(_413591, _413589), -(_413595 = _413591), -(_413595 = _413589)], (1843 ^ _349219) ^ [_413939, _413941, _413943] : [relation(_413939), 1846 ^ _349219 : [(1847 ^ _349219) ^ [] : [in(_413943, relation_rng(relation_rng_restriction(_413941, _413939))), 1850 ^ _349219 : [(1851 ^ _349219) ^ [] : [-(in(_413943, _413941))], (1853 ^ _349219) ^ [] : [-(in(_413943, relation_rng(_413939)))]]], (1855 ^ _349219) ^ [] : [-(in(_413943, relation_rng(relation_rng_restriction(_413941, _413939)))), in(_413943, _413941), in(_413943, relation_rng(_413939))]]], (1865 ^ _349219) ^ [_414612, _414614, _414616] : [subset(_414616, _414614), 1868 ^ _349219 : [(1869 ^ _349219) ^ [] : [-(subset(cartesian_product2(_414616, _414612), cartesian_product2(_414614, _414612)))], (1871 ^ _349219) ^ [] : [-(subset(cartesian_product2(_414612, _414616), cartesian_product2(_414612, _414614)))]]], (1873 ^ _349219) ^ [_414957, _414959, _414961, _414963] : [-(subset(cartesian_product2(_414963, _414959), cartesian_product2(_414961, _414957))), subset(_414963, _414961), subset(_414959, _414957)], (1883 ^ _349219) ^ [_415288, _415290] : [subset(_415290, _415288), -(set_union2(_415290, _415288) = _415288)], (1890 ^ _349219) ^ [_415610] : [-(in(_415610, 1888 ^ [_415610]))], (1892 ^ _349219) ^ [_415722, _415724, _415726] : [-(in(_415722, 1888 ^ [_415726])), in(_415724, 1888 ^ [_415726]), subset(_415722, _415724)], (1902 ^ _349219) ^ [_416037, _416039] : [in(_416037, 1888 ^ [_416039]), -(in(powerset(_416037), 1888 ^ [_416039]))], (1908 ^ _349219) ^ [_416237, _416239] : [subset(_416237, 1888 ^ [_416239]), -(are_equipotent(_416237, 1888 ^ [_416239])), -(in(_416237, 1888 ^ [_416239]))], (1918 ^ _349219) ^ [_416562, _416564] : [-(subset(set_intersection2(_416564, _416562), _416564))], (1920 ^ _349219) ^ [_416688, _416690, _416692] : [-(subset(_416692, set_intersection2(_416690, _416688))), subset(_416692, _416690), subset(_416692, _416688)], (1930 ^ _349219) ^ [_416974] : [-(set_union2(_416974, empty_set) = _416974)], (1932 ^ _349219) ^ [_417084, _417086] : [in(_417086, _417084), -(element(_417086, _417084))], (1938 ^ _349219) ^ [_417308, _417310, _417312] : [-(subset(_417312, _417308)), subset(_417312, _417310), subset(_417310, _417308)], (1948 ^ _349219) ^ [] : [-(powerset(empty_set) = singleton(empty_set))], (1950 ^ _349219) ^ [_417684, _417686, _417688] : [relation(_417684), in(ordered_pair(_417688, _417686), _417684), 1957 ^ _349219 : [(1958 ^ _349219) ^ [] : [-(in(_417688, relation_dom(_417684)))], (1960 ^ _349219) ^ [] : [-(in(_417686, relation_rng(_417684)))]]], (1962 ^ _349219) ^ [_418068] : [relation(_418068), -(subset(_418068, cartesian_product2(relation_dom(_418068), relation_rng(_418068))))], (1968 ^ _349219) ^ [_418270] : [relation(_418270), 1971 ^ _349219 : [(1972 ^ _349219) ^ [_418420] : [relation(_418420), subset(_418270, _418420), 1979 ^ _349219 : [(1980 ^ _349219) ^ [] : [-(subset(relation_dom(_418270), relation_dom(_418420)))], (1982 ^ _349219) ^ [] : [-(subset(relation_rng(_418270), relation_rng(_418420)))]]]]], (1984 ^ _349219) ^ [_418829, _418831, _418833] : [subset(_418833, _418831), -(subset(set_intersection2(_418833, _418829), set_intersection2(_418831, _418829)))], (1990 ^ _349219) ^ [_419057, _419059] : [subset(_419059, _419057), -(set_intersection2(_419059, _419057) = _419059)], (1996 ^ _349219) ^ [_419244] : [-(set_intersection2(_419244, empty_set) = empty_set)], (1998 ^ _349219) ^ [_419354, _419356] : [element(_419356, _419354), -(empty(_419354)), -(in(_419356, _419354))], (2008 ^ _349219) ^ [_419652, _419654] : [-(_419654 = _419652), 2012 ^ _349219 : [(2013 ^ _349219) ^ [] : [-(in(2009 ^ [_419652, _419654], _419654))], (2015 ^ _349219) ^ [] : [in(2009 ^ [_419652, _419654], _419652)]], 2016 ^ _349219 : [(2017 ^ _349219) ^ [] : [-(in(2009 ^ [_419652, _419654], _419652))], (2019 ^ _349219) ^ [] : [in(2009 ^ [_419652, _419654], _419654)]]], (2023 ^ _349219) ^ [_420153] : [-(subset(empty_set, _420153))], (2025 ^ _349219) ^ [_420274, _420276, _420278] : [relation(_420274), in(ordered_pair(_420278, _420276), _420274), 2032 ^ _349219 : [(2033 ^ _349219) ^ [] : [-(in(_420278, relation_field(_420274)))], (2035 ^ _349219) ^ [] : [-(in(_420276, relation_field(_420274)))]]], (2037 ^ _349219) ^ [_420686, _420688, _420690] : [subset(_420690, _420688), -(subset(set_difference(_420690, _420686), set_difference(_420688, _420686)))], (2043 ^ _349219) ^ [_420942, _420944, _420946, _420948] : [ordered_pair(_420948, _420946) = ordered_pair(_420944, _420942), 2046 ^ _349219 : [(2047 ^ _349219) ^ [] : [-(_420948 = _420944)], (2049 ^ _349219) ^ [] : [-(_420946 = _420942)]]], (2051 ^ _349219) ^ [_421240, _421242] : [-(subset(set_difference(_421242, _421240), _421242))], (2053 ^ _349219) ^ [_421338] : [relation(_421338), 2056 ^ _349219 : [(2057 ^ _349219) ^ [] : [-(relation_rng(_421338) = relation_dom(relation_inverse(_421338)))], (2059 ^ _349219) ^ [] : [-(relation_dom(_421338) = relation_rng(relation_inverse(_421338)))]]], (2061 ^ _349219) ^ [_421666, _421668] : [set_difference(_421668, _421666) = empty_set, -(subset(_421668, _421666))], (2067 ^ _349219) ^ [_421834, _421836] : [subset(_421836, _421834), -(set_difference(_421836, _421834) = empty_set)], (2073 ^ _349219) ^ [_422081, _422083] : [subset(singleton(_422083), _422081), -(in(_422083, _422081))], (2079 ^ _349219) ^ [_422247, _422249] : [in(_422249, _422247), -(subset(singleton(_422249), _422247))], (2085 ^ _349219) ^ [_422506, _422508, _422510] : [subset(unordered_pair(_422510, _422508), _422506), 2088 ^ _349219 : [(2089 ^ _349219) ^ [] : [-(in(_422510, _422506))], (2091 ^ _349219) ^ [] : [-(in(_422508, _422506))]]], (2093 ^ _349219) ^ [_422757, _422759, _422761] : [-(subset(unordered_pair(_422761, _422759), _422757)), in(_422761, _422757), in(_422759, _422757)], (2103 ^ _349219) ^ [_423059, _423061] : [-(set_union2(_423061, set_difference(_423059, _423061)) = set_union2(_423061, _423059))], (2115 ^ _349219) ^ [_423466, _423468] : [2116 ^ _349219 : [(2117 ^ _349219) ^ [] : [_423468 = empty_set], (2119 ^ _349219) ^ [] : [_423468 = singleton(_423466)]], -(subset(_423468, singleton(_423466)))], (2105 ^ _349219) ^ [_423206, _423208] : [subset(_423208, singleton(_423206)), -(_423208 = empty_set), -(_423208 = singleton(_423206))], (2123 ^ _349219) ^ [_423731] : [-(set_difference(_423731, empty_set) = _423731)], (2125 ^ _349219) ^ [_423870, _423872] : [element(_423872, powerset(_423870)), -(subset(_423872, _423870))], (2131 ^ _349219) ^ [_424036, _424038] : [subset(_424038, _424036), -(element(_424038, powerset(_424036)))], (2137 ^ _349219) ^ [_424272, _424274] : [-(disjoint(_424274, _424272)), 2141 ^ _349219 : [(2142 ^ _349219) ^ [] : [-(in(2140 ^ [_424272, _424274], _424274))], (2144 ^ _349219) ^ [] : [-(in(2140 ^ [_424272, _424274], _424272))]]], (2146 ^ _349219) ^ [_424586, _424588] : [disjoint(_424588, _424586), 2147 ^ _349219 : [(2148 ^ _349219) ^ [_424678] : [in(_424678, _424588), in(_424678, _424586)]]], (2156 ^ _349219) ^ [_424935] : [subset(_424935, empty_set), -(_424935 = empty_set)], (2162 ^ _349219) ^ [_425124, _425126] : [-(set_difference(set_union2(_425126, _425124), _425124) = set_difference(_425126, _425124))], (2164 ^ _349219) ^ [_425242, _425244] : [element(_425242, powerset(_425244)), 2167 ^ _349219 : [(2168 ^ _349219) ^ [_425394] : [element(_425394, powerset(_425244)), 2171 ^ _349219 : [(2172 ^ _349219) ^ [] : [disjoint(_425242, _425394), -(subset(_425242, subset_complement(_425244, _425394)))], (2178 ^ _349219) ^ [] : [subset(_425242, subset_complement(_425244, _425394)), -(disjoint(_425242, _425394))]]]]], (2184 ^ _349219) ^ [_425878] : [relation(_425878), 2187 ^ _349219 : [(2188 ^ _349219) ^ [_426015] : [relation(_426015), -(subset(relation_dom(relation_composition(_425878, _426015)), relation_dom(_425878)))]]], (2194 ^ _349219) ^ [_426230] : [relation(_426230), 2197 ^ _349219 : [(2198 ^ _349219) ^ [_426367] : [relation(_426367), -(subset(relation_rng(relation_composition(_426230, _426367)), relation_rng(_426367)))]]], (2204 ^ _349219) ^ [_426596, _426598] : [subset(_426598, _426596), -(_426596 = set_union2(_426598, set_difference(_426596, _426598)))], (2210 ^ _349219) ^ [_426804] : [relation(_426804), 2213 ^ _349219 : [(2214 ^ _349219) ^ [_426951] : [relation(_426951), subset(relation_rng(_426804), relation_dom(_426951)), -(relation_dom(relation_composition(_426804, _426951)) = relation_dom(_426804))]]], (2224 ^ _349219) ^ [_427277, _427279] : [element(_427277, powerset(powerset(_427279))), -(_427277 = empty_set), complements_of_subsets(_427279, _427277) = empty_set], (2234 ^ _349219) ^ [_427594, _427596] : [in(_427596, _427594), -(set_union2(singleton(_427596), _427594) = _427594)], (2240 ^ _349219) ^ [_427800] : [relation(_427800), 2243 ^ _349219 : [(2244 ^ _349219) ^ [_427947] : [relation(_427947), subset(relation_dom(_427800), relation_rng(_427947)), -(relation_rng(relation_composition(_427947, _427800)) = relation_rng(_427800))]]], (2254 ^ _349219) ^ [_428273, _428275] : [element(_428273, powerset(powerset(_428275))), -(_428273 = empty_set), -(subset_difference(_428275, cast_to_subset(_428275), union_of_subsets(_428275, _428273)) = meet_of_subsets(_428275, complements_of_subsets(_428275, _428273)))], (2264 ^ _349219) ^ [_428613, _428615] : [element(_428613, powerset(powerset(_428615))), -(_428613 = empty_set), -(union_of_subsets(_428615, complements_of_subsets(_428615, _428613)) = subset_difference(_428615, cast_to_subset(_428615), meet_of_subsets(_428615, _428613)))], (2274 ^ _349219) ^ [_428938, _428940] : [-(set_difference(_428940, set_difference(_428940, _428938)) = set_intersection2(_428940, _428938))], (2276 ^ _349219) ^ [_429027] : [-(set_difference(empty_set, _429027) = empty_set)], (2278 ^ _349219) ^ [_429151, _429153, _429155] : [-(element(_429155, _429151)), in(_429155, _429153), element(_429153, powerset(_429151))], (2288 ^ _349219) ^ [_429484, _429486] : [-(disjoint(_429486, _429484)), -(in(2291 ^ [_429484, _429486], set_intersection2(_429486, _429484)))], (2295 ^ _349219) ^ [_429719, _429721] : [2296 ^ _349219 : [(2297 ^ _349219) ^ [_429792] : [in(_429792, set_intersection2(_429721, _429719))]], disjoint(_429721, _429719)], (2301 ^ _349219) ^ [_429944] : [-(_429944 = empty_set), 2304 ^ _349219 : [(2305 ^ _349219) ^ [_430104] : [element(_430104, powerset(_429944)), 2308 ^ _349219 : [(2309 ^ _349219) ^ [_430258] : [element(_430258, _429944), -(in(_430258, _430104)), -(in(_430258, subset_complement(_429944, _430104)))]]]]], (2319 ^ _349219) ^ [_430604, _430606, _430608] : [element(_430604, powerset(_430608)), in(_430606, subset_complement(_430608, _430604)), in(_430606, _430604)], (2329 ^ _349219) ^ [_430910] : [relation(_430910), -(in(ordered_pair(2334 ^ [_430910], 2335 ^ [_430910]), _430910)), -(_430910 = empty_set)], (2341 ^ _349219) ^ [_431342, _431344, _431346] : [in(_431346, _431344), element(_431344, powerset(_431342)), empty(_431342)], (2351 ^ _349219) ^ [] : [-(relation_dom(empty_set) = empty_set)], (2353 ^ _349219) ^ [] : [-(relation_rng(empty_set) = empty_set)], (2355 ^ _349219) ^ [_431760, _431762] : [subset(_431762, _431760), proper_subset(_431760, _431762)], (2361 ^ _349219) ^ [_431983, _431985, _431987] : [-(disjoint(_431987, _431983)), subset(_431987, _431985), disjoint(_431985, _431983)], (2371 ^ _349219) ^ [_432278] : [relation(_432278), 2376 ^ _349219 : [(2377 ^ _349219) ^ [] : [relation_dom(_432278) = empty_set], (2379 ^ _349219) ^ [] : [relation_rng(_432278) = empty_set]], -(_432278 = empty_set)], (2383 ^ _349219) ^ [_432631] : [relation(_432631), 2386 ^ _349219 : [(2387 ^ _349219) ^ [] : [relation_dom(_432631) = empty_set, -(relation_rng(_432631) = empty_set)], (2393 ^ _349219) ^ [] : [relation_rng(_432631) = empty_set, -(relation_dom(_432631) = empty_set)]]], (2399 ^ _349219) ^ [_433114, _433116] : [set_difference(_433116, singleton(_433114)) = _433116, in(_433114, _433116)], (2405 ^ _349219) ^ [_433287, _433289] : [-(in(_433287, _433289)), -(set_difference(_433289, singleton(_433287)) = _433289)], (2411 ^ _349219) ^ [_433483] : [-(unordered_pair(_433483, _433483) = singleton(_433483))], (2413 ^ _349219) ^ [_433581] : [empty(_433581), -(_433581 = empty_set)], (2419 ^ _349219) ^ [_433783, _433785] : [subset(singleton(_433785), singleton(_433783)), -(_433785 = _433783)], (2425 ^ _349219) ^ [_433992] : [-(relation_dom(identity_relation(_433992)) = _433992)], (2427 ^ _349219) ^ [_434040] : [-(relation_rng(identity_relation(_434040)) = _434040)], (2429 ^ _349219) ^ [_434181, _434183, _434185, _434187] : [relation(_434181), 2432 ^ _349219 : [(2433 ^ _349219) ^ [] : [in(ordered_pair(_434187, _434185), relation_composition(identity_relation(_434183), _434181)), 2436 ^ _349219 : [(2437 ^ _349219) ^ [] : [-(in(_434187, _434183))], (2439 ^ _349219) ^ [] : [-(in(ordered_pair(_434187, _434185), _434181))]]], (2441 ^ _349219) ^ [] : [-(in(ordered_pair(_434187, _434185), relation_composition(identity_relation(_434183), _434181))), in(_434187, _434183), in(ordered_pair(_434187, _434185), _434181)]]], (2451 ^ _349219) ^ [_434874, _434876] : [in(_434876, _434874), empty(_434874)], (2457 ^ _349219) ^ [_435066, _435068] : [-(subset(_435068, set_union2(_435068, _435066)))], (2459 ^ _349219) ^ [_435207, _435209] : [disjoint(_435209, _435207), -(set_difference(_435209, _435207) = _435209)], (2465 ^ _349219) ^ [_435375, _435377] : [set_difference(_435377, _435375) = _435377, -(disjoint(_435377, _435375))], (2471 ^ _349219) ^ [_435607, _435609, _435611] : [relation(_435607), 2474 ^ _349219 : [(2475 ^ _349219) ^ [] : [in(_435611, relation_dom(relation_dom_restriction(_435607, _435609))), 2478 ^ _349219 : [(2479 ^ _349219) ^ [] : [-(in(_435611, _435609))], (2481 ^ _349219) ^ [] : [-(in(_435611, relation_dom(_435607)))]]], (2483 ^ _349219) ^ [] : [-(in(_435611, relation_dom(relation_dom_restriction(_435607, _435609)))), in(_435611, _435609), in(_435611, relation_dom(_435607))]]], (2493 ^ _349219) ^ [_436266, _436268] : [relation(_436266), -(subset(relation_dom_restriction(_436266, _436268), _436266))], (2499 ^ _349219) ^ [_436480, _436482] : [empty(_436482), -(_436482 = _436480), empty(_436480)], (2509 ^ _349219) ^ [_436791, _436793, _436795] : [-(subset(set_union2(_436795, _436791), _436793)), subset(_436795, _436793), subset(_436791, _436793)], (2519 ^ _349219) ^ [_437120, _437122, _437124] : [singleton(_437124) = unordered_pair(_437122, _437120), -(_437124 = _437122)], (2525 ^ _349219) ^ [_437346, _437348] : [relation(_437346), -(relation_dom(relation_dom_restriction(_437346, _437348)) = set_intersection2(relation_dom(_437346), _437348))], (2531 ^ _349219) ^ [_437574, _437576] : [in(_437576, _437574), -(subset(_437576, union(_437574)))], (2537 ^ _349219) ^ [_437788, _437790] : [relation(_437788), -(relation_dom_restriction(_437788, _437790) = relation_composition(identity_relation(_437790), _437788))], (2543 ^ _349219) ^ [_438012, _438014] : [relation(_438012), -(subset(relation_rng(relation_dom_restriction(_438012, _438014)), relation_rng(_438012)))], (2549 ^ _349219) ^ [_438205] : [-(union(powerset(_438205)) = _438205)], (2587 ^ _349219) ^ [_439726, _439728, _439730] : [singleton(_439730) = unordered_pair(_439728, _439726), -(_439728 = _439726)], (2552 ^ _349219) ^ [_438446] : [-(in(_438446, 2550 ^ [_438446]))], (2554 ^ _349219) ^ [_438558, _438560, _438562] : [-(in(_438558, 2550 ^ [_438562])), in(_438560, 2550 ^ [_438562]), subset(_438558, _438560)], (2564 ^ _349219) ^ [_438873, _438875] : [in(_438873, 2550 ^ [_438875]), 2568 ^ _349219 : [(2569 ^ _349219) ^ [] : [-(in(2567 ^ [_438873, _438875], 2550 ^ [_438875]))], (2571 ^ _349219) ^ [_439185] : [subset(_439185, _438873), -(in(_439185, 2567 ^ [_438873, _438875]))]]], (2577 ^ _349219) ^ [_439392, _439394] : [subset(_439392, 2550 ^ [_439394]), -(are_equipotent(_439392, 2550 ^ [_439394])), -(in(_439392, 2550 ^ [_439394]))]], input).
% 2.87/3.61 ncf('1',plain,[set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []) = set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []), 1078 : in(562 ^ [set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])), set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []), set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []))], set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])), 1084 : in(562 ^ [set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])), set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []), set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []))], 2592 ^ [])],start(1074 ^ 0,bind([[_387886, _387888, _387890, _388070], [set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []), 2592 ^ [], relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 562 ^ [set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])), set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []), set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []))]]]))).
% 2.87/3.61 ncf('1.1',plain,[-(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []) = set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []))],extension(2 ^ 1,bind([[_349363], [set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])]]))).
% 2.87/3.61 ncf('1.2',plain,[-(in(562 ^ [set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])), set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []), set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []))], set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []))), 561 : -(in(set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])), set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])))), 561 : set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])) = set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])), 547 : -(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []) = empty_set)],extension(543 ^ 3,bind([[_368605, _368607, _369233], [set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])), set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []), set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []))]]))).
% 2.87/3.61 ncf('1.2.1',plain,[in(set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])), set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []))), in(set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])), set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])))],extension(328 ^ 8,bind([[_360692, _360694], [set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])), set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []))]]))).
% 2.87/3.61 ncf('1.2.1.1',plain,[-(in(set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])), set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []))))],reduction('1.2')).
% 2.87/3.61 ncf('1.2.2',plain,[-(set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])) = set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])))],extension(2 ^ 6,bind([[_349363], [set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []))]]))).
% 2.87/3.61 ncf('1.2.3',plain,[set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []) = empty_set, -(subset(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []))],extension(1672 ^ 4,bind([[_407893, _407895], [2592 ^ [], relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ []))]]))).
% 2.87/3.61 ncf('1.2.3.1',plain,[subset(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])],extension(2597 ^ 5)).
% 2.87/3.61 ncf('1.3',plain,[-(in(562 ^ [set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])), set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []), set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []))], 2592 ^ [])), 1847 : in(562 ^ [set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])), set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []), set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []))], relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ []))), 1847 : relation(2593 ^ [])],extension(1843 ^ 5,bind([[_413939, _413941, _413943], [2593 ^ [], 2592 ^ [], 562 ^ [set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])), set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []), set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []))]]]))).
% 2.87/3.61 ncf('1.3.1',plain,[-(in(562 ^ [set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ [])), set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []), set_meet(set_difference(relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ [])), 2592 ^ []))], relation_rng(relation_rng_restriction(2592 ^ [], 2593 ^ []))))],extension(1082 ^ 8)).
% 2.87/3.61 ncf('1.3.2',plain,[-(relation(2593 ^ []))],extension(2595 ^ 6)).
% 2.87/3.61 %-----------------------------------------------------
% 2.87/3.61 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------