%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU212+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n018.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:40 EDT 2023
% Result : Theorem 0.39s 1.37s
% Output : Proof 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.11 % Problem : SEU212+2 : TPTP v8.1.2. Released v3.3.0.
% 0.08/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n018.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 18 13:33:57 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.39/1.37
% 0.39/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.39/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.39/1.37 %-----------------------------------------------------
% 0.39/1.37 ncf(matrix, plain, [(2970 ^ _399991) ^ [] : [-(relation(2968 ^ []))], (2972 ^ _399991) ^ [] : [-(function(2968 ^ []))], (2974 ^ _399991) ^ [] : [2983 ^ _399991 : [(2984 ^ _399991) ^ [] : [-(in(2966 ^ [], relation_dom(2968 ^ [])))], (2986 ^ _399991) ^ [] : [-(2967 ^ [] = apply(2968 ^ [], 2966 ^ []))], (2988 ^ _399991) ^ [] : [in(ordered_pair(2966 ^ [], 2967 ^ []), 2968 ^ [])]], 2975 ^ _399991 : [(2976 ^ _399991) ^ [] : [-(in(ordered_pair(2966 ^ [], 2967 ^ []), 2968 ^ []))], (2978 ^ _399991) ^ [] : [in(2966 ^ [], relation_dom(2968 ^ [])), 2967 ^ [] = apply(2968 ^ [], 2966 ^ [])]]], (2 ^ _399991) ^ [_400135] : [-(_400135 = _400135)], (4 ^ _399991) ^ [_400242, _400244] : [_400244 = _400242, -(_400242 = _400244)], (10 ^ _399991) ^ [_400446, _400448, _400450] : [-(_400450 = _400446), _400450 = _400448, _400448 = _400446], (20 ^ _399991) ^ [_400759, _400761] : [-(relation_empty_yielding(_400759)), _400761 = _400759, relation_empty_yielding(_400761)], (30 ^ _399991) ^ [_401082, _401084, _401086, _401088] : [-(element(_401086, _401082)), element(_401088, _401084), _401088 = _401086, _401084 = _401082], (44 ^ _399991) ^ [_401526, _401528, _401530, _401532] : [-(proper_subset(_401530, _401526)), proper_subset(_401532, _401528), _401532 = _401530, _401528 = _401526], (58 ^ _399991) ^ [_401970, _401972, _401974, _401976] : [-(disjoint(_401974, _401970)), disjoint(_401976, _401972), _401976 = _401974, _401972 = _401970], (72 ^ _399991) ^ [_402386, _402388] : [-(empty(_402386)), _402388 = _402386, empty(_402388)], (82 ^ _399991) ^ [_402709, _402711, _402713, _402715] : [-(subset(_402713, _402709)), subset(_402715, _402711), _402715 = _402713, _402711 = _402709], (96 ^ _399991) ^ [_403153, _403155, _403157, _403159] : [-(are_equipotent(_403157, _403153)), are_equipotent(_403159, _403155), _403159 = _403157, _403155 = _403153], (110 ^ _399991) ^ [_403569, _403571] : [-(relation(_403569)), _403571 = _403569, relation(_403571)], (120 ^ _399991) ^ [_403864, _403866] : [-(function(_403864)), _403866 = _403864, function(_403866)], (130 ^ _399991) ^ [_404167, _404169, _404171, _404173] : [-(in(_404171, _404167)), in(_404173, _404169), _404173 = _404171, _404169 = _404167], (144 ^ _399991) ^ [_404607, _404609] : [_404609 = _404607, -(set_meet(_404609) = set_meet(_404607))], (150 ^ _399991) ^ [_404853, _404855, _404857, _404859] : [-(relation_rng_restriction(_404859, _404855) = relation_rng_restriction(_404857, _404853)), _404859 = _404857, _404855 = _404853], (160 ^ _399991) ^ [_405212, _405214, _405216, _405218] : [-(relation_image(_405218, _405214) = relation_image(_405216, _405212)), _405218 = _405216, _405214 = _405212], (170 ^ _399991) ^ [_405571, _405573, _405575, _405577] : [-(relation_inverse_image(_405577, _405573) = relation_inverse_image(_405575, _405571)), _405577 = _405575, _405573 = _405571], (180 ^ _399991) ^ [_405930, _405932, _405934, _405936] : [-(cartesian_product2(_405936, _405932) = cartesian_product2(_405934, _405930)), _405936 = _405934, _405932 = _405930], (190 ^ _399991) ^ [_406261, _406263] : [_406263 = _406261, -(relation_field(_406263) = relation_field(_406261))], (196 ^ _399991) ^ [_406479, _406481] : [_406481 = _406479, -(relation_inverse(_406481) = relation_inverse(_406479))], (202 ^ _399991) ^ [_406725, _406727, _406729, _406731] : [-(union_of_subsets(_406731, _406727) = union_of_subsets(_406729, _406725)), _406731 = _406729, _406727 = _406725], (212 ^ _399991) ^ [_407084, _407086, _407088, _407090] : [-(complements_of_subsets(_407090, _407086) = complements_of_subsets(_407088, _407084)), _407090 = _407088, _407086 = _407084], (222 ^ _399991) ^ [_407471, _407473, _407475, _407477, _407479, _407481] : [-(subset_difference(_407481, _407477, _407473) = subset_difference(_407479, _407475, _407471)), _407481 = _407479, _407477 = _407475, _407473 = _407471], (236 ^ _399991) ^ [_407931, _407933] : [_407933 = _407931, -(cast_to_subset(_407933) = cast_to_subset(_407931))], (242 ^ _399991) ^ [_408177, _408179, _408181, _408183] : [-(meet_of_subsets(_408183, _408179) = meet_of_subsets(_408181, _408177)), _408183 = _408181, _408179 = _408177], (252 ^ _399991) ^ [_408536, _408538, _408540, _408542] : [-(subset_complement(_408542, _408538) = subset_complement(_408540, _408536)), _408542 = _408540, _408538 = _408536], (262 ^ _399991) ^ [_408895, _408897, _408899, _408901] : [-(set_difference(_408901, _408897) = set_difference(_408899, _408895)), _408901 = _408899, _408897 = _408895], (272 ^ _399991) ^ [_409254, _409256, _409258, _409260] : [-(set_union2(_409260, _409256) = set_union2(_409258, _409254)), _409260 = _409258, _409256 = _409254], (282 ^ _399991) ^ [_409613, _409615, _409617, _409619] : [-(set_intersection2(_409619, _409615) = set_intersection2(_409617, _409613)), _409619 = _409617, _409615 = _409613], (292 ^ _399991) ^ [_409972, _409974, _409976, _409978] : [-(relation_composition(_409978, _409974) = relation_composition(_409976, _409972)), _409978 = _409976, _409974 = _409972], (302 ^ _399991) ^ [_410303, _410305] : [_410305 = _410303, -(identity_relation(_410305) = identity_relation(_410303))], (308 ^ _399991) ^ [_410549, _410551, _410553, _410555] : [-(relation_dom_restriction(_410555, _410551) = relation_dom_restriction(_410553, _410549)), _410555 = _410553, _410551 = _410549], (318 ^ _399991) ^ [_410880, _410882] : [_410882 = _410880, -(relation_rng(_410882) = relation_rng(_410880))], (324 ^ _399991) ^ [_411098, _411100] : [_411100 = _411098, -(union(_411100) = union(_411098))], (330 ^ _399991) ^ [_411316, _411318] : [_411318 = _411316, -(powerset(_411318) = powerset(_411316))], (336 ^ _399991) ^ [_411534, _411536] : [_411536 = _411534, -(singleton(_411536) = singleton(_411534))], (342 ^ _399991) ^ [_411780, _411782, _411784, _411786] : [-(unordered_pair(_411786, _411782) = unordered_pair(_411784, _411780)), _411786 = _411784, _411782 = _411780], (352 ^ _399991) ^ [_412139, _412141, _412143, _412145] : [-(ordered_pair(_412145, _412141) = ordered_pair(_412143, _412139)), _412145 = _412143, _412141 = _412139], (362 ^ _399991) ^ [_412470, _412472] : [_412472 = _412470, -(relation_dom(_412472) = relation_dom(_412470))], (368 ^ _399991) ^ [_412696, _412698, _412700, _412702] : [-(apply(_412702, _412698) = apply(_412700, _412696)), _412702 = _412700, _412698 = _412696], (378 ^ _399991) ^ [_413157, _413159] : [in(_413159, _413157), in(_413157, _413159)], (384 ^ _399991) ^ [_413368, _413370] : [proper_subset(_413370, _413368), proper_subset(_413368, _413370)], (390 ^ _399991) ^ [_413565] : [empty(_413565), -(function(_413565))], (396 ^ _399991) ^ [_413751] : [empty(_413751), -(relation(_413751))], (402 ^ _399991) ^ [_413936, _413938] : [-(unordered_pair(_413938, _413936) = unordered_pair(_413936, _413938))], (404 ^ _399991) ^ [_414036, _414038] : [-(set_union2(_414038, _414036) = set_union2(_414036, _414038))], (406 ^ _399991) ^ [_414136, _414138] : [-(set_intersection2(_414138, _414136) = set_intersection2(_414136, _414138))], (408 ^ _399991) ^ [_414251, _414253] : [relation(_414251), 411 ^ _399991 : [(434 ^ _399991) ^ [] : [-(_414251 = identity_relation(_414253)), 447 ^ _399991 : [(448 ^ _399991) ^ [] : [-(in(435 ^ [_414251, _414253], _414253))], (450 ^ _399991) ^ [] : [-(435 ^ [_414251, _414253] = 436 ^ [_414251, _414253])], (452 ^ _399991) ^ [] : [in(ordered_pair(435 ^ [_414251, _414253], 436 ^ [_414251, _414253]), _414251)]], 439 ^ _399991 : [(440 ^ _399991) ^ [] : [-(in(ordered_pair(435 ^ [_414251, _414253], 436 ^ [_414251, _414253]), _414251))], (442 ^ _399991) ^ [] : [in(435 ^ [_414251, _414253], _414253), 435 ^ [_414251, _414253] = 436 ^ [_414251, _414253]]]], (412 ^ _399991) ^ [] : [_414251 = identity_relation(_414253), 415 ^ _399991 : [(416 ^ _399991) ^ [_414561, _414563] : [in(ordered_pair(_414563, _414561), _414251), 419 ^ _399991 : [(420 ^ _399991) ^ [] : [-(in(_414563, _414253))], (422 ^ _399991) ^ [] : [-(_414563 = _414561)]]], (424 ^ _399991) ^ [_414824, _414826] : [-(in(ordered_pair(_414826, _414824), _414251)), in(_414826, _414253), _414826 = _414824]]]]], (456 ^ _399991) ^ [_415932, _415934] : [_415934 = _415932, 459 ^ _399991 : [(460 ^ _399991) ^ [] : [-(subset(_415934, _415932))], (462 ^ _399991) ^ [] : [-(subset(_415932, _415934))]]], (464 ^ _399991) ^ [_416169, _416171] : [-(_416171 = _416169), subset(_416171, _416169), subset(_416169, _416171)], (474 ^ _399991) ^ [_416456] : [relation(_416456), 477 ^ _399991 : [(478 ^ _399991) ^ [_416642, _416644] : [relation(_416642), 481 ^ _399991 : [(504 ^ _399991) ^ [] : [-(_416642 = relation_dom_restriction(_416456, _416644)), 517 ^ _399991 : [(518 ^ _399991) ^ [] : [-(in(505 ^ [_416456, _416642, _416644], _416644))], (520 ^ _399991) ^ [] : [-(in(ordered_pair(505 ^ [_416456, _416642, _416644], 506 ^ [_416456, _416642, _416644]), _416456))], (522 ^ _399991) ^ [] : [in(ordered_pair(505 ^ [_416456, _416642, _416644], 506 ^ [_416456, _416642, _416644]), _416642)]], 509 ^ _399991 : [(510 ^ _399991) ^ [] : [-(in(ordered_pair(505 ^ [_416456, _416642, _416644], 506 ^ [_416456, _416642, _416644]), _416642))], (512 ^ _399991) ^ [] : [in(505 ^ [_416456, _416642, _416644], _416644), in(ordered_pair(505 ^ [_416456, _416642, _416644], 506 ^ [_416456, _416642, _416644]), _416456)]]], (482 ^ _399991) ^ [] : [_416642 = relation_dom_restriction(_416456, _416644), 485 ^ _399991 : [(486 ^ _399991) ^ [_416967, _416969] : [in(ordered_pair(_416969, _416967), _416642), 489 ^ _399991 : [(490 ^ _399991) ^ [] : [-(in(_416969, _416644))], (492 ^ _399991) ^ [] : [-(in(ordered_pair(_416969, _416967), _416456))]]], (494 ^ _399991) ^ [_417246, _417248] : [-(in(ordered_pair(_417248, _417246), _416642)), in(_417248, _416644), in(ordered_pair(_417248, _417246), _416456)]]]]]]], (526 ^ _399991) ^ [_418415, _418417] : [relation(_418415), 529 ^ _399991 : [(530 ^ _399991) ^ [_418586] : [relation(_418586), 533 ^ _399991 : [(556 ^ _399991) ^ [] : [-(_418586 = relation_rng_restriction(_418417, _418415)), 569 ^ _399991 : [(570 ^ _399991) ^ [] : [-(in(558 ^ [_418415, _418417, _418586], _418417))], (572 ^ _399991) ^ [] : [-(in(ordered_pair(557 ^ [_418415, _418417, _418586], 558 ^ [_418415, _418417, _418586]), _418415))], (574 ^ _399991) ^ [] : [in(ordered_pair(557 ^ [_418415, _418417, _418586], 558 ^ [_418415, _418417, _418586]), _418586)]], 561 ^ _399991 : [(562 ^ _399991) ^ [] : [-(in(ordered_pair(557 ^ [_418415, _418417, _418586], 558 ^ [_418415, _418417, _418586]), _418586))], (564 ^ _399991) ^ [] : [in(558 ^ [_418415, _418417, _418586], _418417), in(ordered_pair(557 ^ [_418415, _418417, _418586], 558 ^ [_418415, _418417, _418586]), _418415)]]], (534 ^ _399991) ^ [] : [_418586 = relation_rng_restriction(_418417, _418415), 537 ^ _399991 : [(538 ^ _399991) ^ [_418913, _418915] : [in(ordered_pair(_418915, _418913), _418586), 541 ^ _399991 : [(542 ^ _399991) ^ [] : [-(in(_418913, _418417))], (544 ^ _399991) ^ [] : [-(in(ordered_pair(_418915, _418913), _418415))]]], (546 ^ _399991) ^ [_419192, _419194] : [-(in(ordered_pair(_419194, _419192), _418586)), in(_419192, _418417), in(ordered_pair(_419194, _419192), _418415)]]]]]]], (578 ^ _399991) ^ [_420338] : [relation(_420338), 581 ^ _399991 : [(605 ^ _399991) ^ [_421451, _421453] : [-(_421451 = relation_image(_420338, _421453)), 618 ^ _399991 : [(619 ^ _399991) ^ [] : [-(in(ordered_pair(617 ^ [_420338, _421451, _421453], 606 ^ [_420338, _421451, _421453]), _420338))], (621 ^ _399991) ^ [] : [-(in(617 ^ [_420338, _421451, _421453], _421453))], (623 ^ _399991) ^ [] : [in(606 ^ [_420338, _421451, _421453], _421451)]], 609 ^ _399991 : [(610 ^ _399991) ^ [] : [-(in(606 ^ [_420338, _421451, _421453], _421451))], (612 ^ _399991) ^ [_421755] : [in(ordered_pair(_421755, 606 ^ [_420338, _421451, _421453]), _420338), in(_421755, _421453)]]], (582 ^ _399991) ^ [_420545, _420547] : [_420545 = relation_image(_420338, _420547), 585 ^ _399991 : [(586 ^ _399991) ^ [_420737] : [in(_420737, _420545), 590 ^ _399991 : [(591 ^ _399991) ^ [] : [-(in(ordered_pair(589 ^ [_420338, _420545, _420547, _420737], _420737), _420338))], (593 ^ _399991) ^ [] : [-(in(589 ^ [_420338, _420545, _420547, _420737], _420547))]]], (595 ^ _399991) ^ [_421091] : [-(in(_421091, _420545)), 596 ^ _399991 : [(597 ^ _399991) ^ [_421196] : [in(ordered_pair(_421196, _421091), _420338), in(_421196, _420547)]]]]]]], (627 ^ _399991) ^ [_422357] : [relation(_422357), 630 ^ _399991 : [(654 ^ _399991) ^ [_423470, _423472] : [-(_423470 = relation_inverse_image(_422357, _423472)), 667 ^ _399991 : [(668 ^ _399991) ^ [] : [-(in(ordered_pair(655 ^ [_422357, _423470, _423472], 666 ^ [_422357, _423470, _423472]), _422357))], (670 ^ _399991) ^ [] : [-(in(666 ^ [_422357, _423470, _423472], _423472))], (672 ^ _399991) ^ [] : [in(655 ^ [_422357, _423470, _423472], _423470)]], 658 ^ _399991 : [(659 ^ _399991) ^ [] : [-(in(655 ^ [_422357, _423470, _423472], _423470))], (661 ^ _399991) ^ [_423774] : [in(ordered_pair(655 ^ [_422357, _423470, _423472], _423774), _422357), in(_423774, _423472)]]], (631 ^ _399991) ^ [_422564, _422566] : [_422564 = relation_inverse_image(_422357, _422566), 634 ^ _399991 : [(635 ^ _399991) ^ [_422756] : [in(_422756, _422564), 639 ^ _399991 : [(640 ^ _399991) ^ [] : [-(in(ordered_pair(_422756, 638 ^ [_422357, _422564, _422566, _422756]), _422357))], (642 ^ _399991) ^ [] : [-(in(638 ^ [_422357, _422564, _422566, _422756], _422566))]]], (644 ^ _399991) ^ [_423110] : [-(in(_423110, _422564)), 645 ^ _399991 : [(646 ^ _399991) ^ [_423215] : [in(ordered_pair(_423110, _423215), _422357), in(_423215, _422566)]]]]]]], (688 ^ _399991) ^ [_424866] : [690 ^ _399991 : [(691 ^ _399991) ^ [] : [-(in(689 ^ [_424866], _424866))], (693 ^ _399991) ^ [_425103, _425105] : [689 ^ [_424866] = ordered_pair(_425105, _425103)]], -(relation(_424866))], (676 ^ _399991) ^ [_424405] : [relation(_424405), 679 ^ _399991 : [(680 ^ _399991) ^ [_424553] : [in(_424553, _424405), -(_424553 = ordered_pair(683 ^ [_424405, _424553], 684 ^ [_424405, _424553]))]]], (746 ^ _399991) ^ [_427001, _427003] : [_427003 = empty_set, 749 ^ _399991 : [(750 ^ _399991) ^ [] : [_427001 = set_meet(_427003), -(_427001 = empty_set)], (756 ^ _399991) ^ [] : [_427001 = empty_set, -(_427001 = set_meet(_427003))]]], (697 ^ _399991) ^ [_425294, _425296] : [-(_425296 = empty_set), 700 ^ _399991 : [(724 ^ _399991) ^ [] : [-(_425294 = set_meet(_425296)), 728 ^ _399991 : [(729 ^ _399991) ^ [] : [-(in(725 ^ [_425294, _425296], _425294))], (732 ^ _399991) ^ [] : [-(in(730 ^ [_425294, _425296], _425296))], (734 ^ _399991) ^ [] : [in(725 ^ [_425294, _425296], 730 ^ [_425294, _425296])]], 735 ^ _399991 : [(742 ^ _399991) ^ [] : [in(725 ^ [_425294, _425296], _425294)], (736 ^ _399991) ^ [_426696] : [in(_426696, _425296), -(in(725 ^ [_425294, _425296], _426696))]]], (701 ^ _399991) ^ [] : [_425294 = set_meet(_425296), 704 ^ _399991 : [(715 ^ _399991) ^ [_425922] : [717 ^ _399991 : [(718 ^ _399991) ^ [] : [-(in(716 ^ [_425294, _425296, _425922], _425296))], (720 ^ _399991) ^ [] : [in(_425922, 716 ^ [_425294, _425296, _425922])]], -(in(_425922, _425294))], (705 ^ _399991) ^ [_425592] : [in(_425592, _425294), 708 ^ _399991 : [(709 ^ _399991) ^ [_425737] : [in(_425737, _425296), -(in(_425592, _425737))]]]]]]], (778 ^ _399991) ^ [_428019, _428021] : [-(_428019 = singleton(_428021)), 782 ^ _399991 : [(783 ^ _399991) ^ [] : [-(in(779 ^ [_428019, _428021], _428019))], (785 ^ _399991) ^ [] : [779 ^ [_428019, _428021] = _428021]], 786 ^ _399991 : [(787 ^ _399991) ^ [] : [-(779 ^ [_428019, _428021] = _428021)], (789 ^ _399991) ^ [] : [in(779 ^ [_428019, _428021], _428019)]]], (762 ^ _399991) ^ [_427498, _427500] : [_427498 = singleton(_427500), 765 ^ _399991 : [(766 ^ _399991) ^ [_427668] : [in(_427668, _427498), -(_427668 = _427500)], (772 ^ _399991) ^ [_427840] : [_427840 = _427500, -(in(_427840, _427498))]]], (793 ^ _399991) ^ [_428570] : [_428570 = empty_set, 796 ^ _399991 : [(797 ^ _399991) ^ [_428683] : [in(_428683, _428570)]]], (799 ^ _399991) ^ [_428749] : [-(in(800 ^ [_428749], _428749)), -(_428749 = empty_set)], (822 ^ _399991) ^ [_429561, _429563] : [-(_429561 = powerset(_429563)), 826 ^ _399991 : [(827 ^ _399991) ^ [] : [-(in(823 ^ [_429561, _429563], _429561))], (829 ^ _399991) ^ [] : [subset(823 ^ [_429561, _429563], _429563)]], 830 ^ _399991 : [(831 ^ _399991) ^ [] : [-(subset(823 ^ [_429561, _429563], _429563))], (833 ^ _399991) ^ [] : [in(823 ^ [_429561, _429563], _429561)]]], (806 ^ _399991) ^ [_429040, _429042] : [_429040 = powerset(_429042), 809 ^ _399991 : [(810 ^ _399991) ^ [_429210] : [in(_429210, _429040), -(subset(_429210, _429042))], (816 ^ _399991) ^ [_429382] : [subset(_429382, _429042), -(in(_429382, _429040))]]], (837 ^ _399991) ^ [_430083] : [relation(_430083), 840 ^ _399991 : [(841 ^ _399991) ^ [_430241] : [relation(_430241), 844 ^ _399991 : [(861 ^ _399991) ^ [] : [-(_430083 = _430241), 866 ^ _399991 : [(867 ^ _399991) ^ [] : [-(in(ordered_pair(862 ^ [_430083, _430241], 863 ^ [_430083, _430241]), _430083))], (869 ^ _399991) ^ [] : [in(ordered_pair(862 ^ [_430083, _430241], 863 ^ [_430083, _430241]), _430241)]], 870 ^ _399991 : [(871 ^ _399991) ^ [] : [-(in(ordered_pair(862 ^ [_430083, _430241], 863 ^ [_430083, _430241]), _430241))], (873 ^ _399991) ^ [] : [in(ordered_pair(862 ^ [_430083, _430241], 863 ^ [_430083, _430241]), _430083)]]], (845 ^ _399991) ^ [] : [_430083 = _430241, 848 ^ _399991 : [(849 ^ _399991) ^ [_430546, _430548] : [in(ordered_pair(_430548, _430546), _430083), -(in(ordered_pair(_430548, _430546), _430241))], (855 ^ _399991) ^ [_430736, _430738] : [in(ordered_pair(_430738, _430736), _430241), -(in(ordered_pair(_430738, _430736), _430083))]]]]]]], (877 ^ _399991) ^ [_431573, _431575] : [-(empty(_431575)), 880 ^ _399991 : [(881 ^ _399991) ^ [] : [element(_431573, _431575), -(in(_431573, _431575))], (887 ^ _399991) ^ [] : [in(_431573, _431575), -(element(_431573, _431575))]]], (893 ^ _399991) ^ [_431986, _431988] : [empty(_431988), 896 ^ _399991 : [(897 ^ _399991) ^ [] : [element(_431986, _431988), -(empty(_431986))], (903 ^ _399991) ^ [] : [empty(_431986), -(element(_431986, _431988))]]], (931 ^ _399991) ^ [_433211, _433213, _433215] : [-(_433211 = unordered_pair(_433215, _433213)), 935 ^ _399991 : [(936 ^ _399991) ^ [] : [-(in(932 ^ [_433211, _433213, _433215], _433211))], (938 ^ _399991) ^ [] : [932 ^ [_433211, _433213, _433215] = _433215], (940 ^ _399991) ^ [] : [932 ^ [_433211, _433213, _433215] = _433213]], 941 ^ _399991 : [(948 ^ _399991) ^ [] : [in(932 ^ [_433211, _433213, _433215], _433211)], (942 ^ _399991) ^ [] : [-(932 ^ [_433211, _433213, _433215] = _433215), -(932 ^ [_433211, _433213, _433215] = _433213)]]], (909 ^ _399991) ^ [_432486, _432488, _432490] : [_432486 = unordered_pair(_432490, _432488), 912 ^ _399991 : [(923 ^ _399991) ^ [_432946] : [924 ^ _399991 : [(925 ^ _399991) ^ [] : [_432946 = _432490], (927 ^ _399991) ^ [] : [_432946 = _432488]], -(in(_432946, _432486))], (913 ^ _399991) ^ [_432668] : [in(_432668, _432486), -(_432668 = _432490), -(_432668 = _432488)]]], (974 ^ _399991) ^ [_434730, _434732, _434734] : [-(_434730 = set_union2(_434734, _434732)), 978 ^ _399991 : [(979 ^ _399991) ^ [] : [-(in(975 ^ [_434730, _434732, _434734], _434730))], (981 ^ _399991) ^ [] : [in(975 ^ [_434730, _434732, _434734], _434734)], (983 ^ _399991) ^ [] : [in(975 ^ [_434730, _434732, _434734], _434732)]], 984 ^ _399991 : [(991 ^ _399991) ^ [] : [in(975 ^ [_434730, _434732, _434734], _434730)], (985 ^ _399991) ^ [] : [-(in(975 ^ [_434730, _434732, _434734], _434734)), -(in(975 ^ [_434730, _434732, _434734], _434732))]]], (952 ^ _399991) ^ [_434005, _434007, _434009] : [_434005 = set_union2(_434009, _434007), 955 ^ _399991 : [(966 ^ _399991) ^ [_434465] : [967 ^ _399991 : [(968 ^ _399991) ^ [] : [in(_434465, _434009)], (970 ^ _399991) ^ [] : [in(_434465, _434007)]], -(in(_434465, _434005))], (956 ^ _399991) ^ [_434187] : [in(_434187, _434005), -(in(_434187, _434009)), -(in(_434187, _434007))]]], (1025 ^ _399991) ^ [_436781, _436783, _436785] : [-(_436781 = cartesian_product2(_436785, _436783)), 1043 ^ _399991 : [(1044 ^ _399991) ^ [] : [-(in(1041 ^ [_436781, _436783, _436785], _436785))], (1046 ^ _399991) ^ [] : [-(in(1042 ^ [_436781, _436783, _436785], _436783))], (1048 ^ _399991) ^ [] : [-(1026 ^ [_436781, _436783, _436785] = ordered_pair(1041 ^ [_436781, _436783, _436785], 1042 ^ [_436781, _436783, _436785]))], (1050 ^ _399991) ^ [] : [in(1026 ^ [_436781, _436783, _436785], _436781)]], 1029 ^ _399991 : [(1030 ^ _399991) ^ [] : [-(in(1026 ^ [_436781, _436783, _436785], _436781))], (1032 ^ _399991) ^ [_437119, _437121] : [in(_437121, _436785), in(_437119, _436783), 1026 ^ [_436781, _436783, _436785] = ordered_pair(_437121, _437119)]]], (995 ^ _399991) ^ [_435524, _435526, _435528] : [_435524 = cartesian_product2(_435528, _435526), 998 ^ _399991 : [(999 ^ _399991) ^ [_435725] : [in(_435725, _435524), 1004 ^ _399991 : [(1005 ^ _399991) ^ [] : [-(in(1002 ^ [_435524, _435526, _435528, _435725], _435528))], (1007 ^ _399991) ^ [] : [-(in(1003 ^ [_435524, _435526, _435528, _435725], _435526))], (1009 ^ _399991) ^ [] : [-(_435725 = ordered_pair(1002 ^ [_435524, _435526, _435528, _435725], 1003 ^ [_435524, _435526, _435528, _435725]))]]], (1011 ^ _399991) ^ [_436285] : [-(in(_436285, _435524)), 1012 ^ _399991 : [(1013 ^ _399991) ^ [_436415, _436417] : [in(_436417, _435528), in(_436415, _435526), _436285 = ordered_pair(_436417, _436415)]]]]], (1054 ^ _399991) ^ [_438015] : [relation(_438015), 1057 ^ _399991 : [(1058 ^ _399991) ^ [_438173] : [relation(_438173), 1061 ^ _399991 : [(1072 ^ _399991) ^ [] : [1075 ^ _399991 : [(1076 ^ _399991) ^ [] : [-(in(ordered_pair(1073 ^ [_438015, _438173], 1074 ^ [_438015, _438173]), _438015))], (1078 ^ _399991) ^ [] : [in(ordered_pair(1073 ^ [_438015, _438173], 1074 ^ [_438015, _438173]), _438173)]], -(subset(_438015, _438173))], (1062 ^ _399991) ^ [] : [subset(_438015, _438173), 1065 ^ _399991 : [(1066 ^ _399991) ^ [_438449, _438451] : [in(ordered_pair(_438451, _438449), _438015), -(in(ordered_pair(_438451, _438449), _438173))]]]]]]], (1092 ^ _399991) ^ [_439412, _439414] : [1094 ^ _399991 : [(1095 ^ _399991) ^ [] : [-(in(1093 ^ [_439412, _439414], _439414))], (1097 ^ _399991) ^ [] : [in(1093 ^ [_439412, _439414], _439412)]], -(subset(_439414, _439412))], (1082 ^ _399991) ^ [_439098, _439100] : [subset(_439100, _439098), 1085 ^ _399991 : [(1086 ^ _399991) ^ [_439235] : [in(_439235, _439100), -(in(_439235, _439098))]]], (1123 ^ _399991) ^ [_440537, _440539, _440541] : [-(_440537 = set_intersection2(_440541, _440539)), 1135 ^ _399991 : [(1136 ^ _399991) ^ [] : [-(in(1124 ^ [_440537, _440539, _440541], _440541))], (1138 ^ _399991) ^ [] : [-(in(1124 ^ [_440537, _440539, _440541], _440539))], (1140 ^ _399991) ^ [] : [in(1124 ^ [_440537, _440539, _440541], _440537)]], 1127 ^ _399991 : [(1128 ^ _399991) ^ [] : [-(in(1124 ^ [_440537, _440539, _440541], _440537))], (1130 ^ _399991) ^ [] : [in(1124 ^ [_440537, _440539, _440541], _440541), in(1124 ^ [_440537, _440539, _440541], _440539)]]], (1101 ^ _399991) ^ [_439812, _439814, _439816] : [_439812 = set_intersection2(_439816, _439814), 1104 ^ _399991 : [(1105 ^ _399991) ^ [_439994] : [in(_439994, _439812), 1108 ^ _399991 : [(1109 ^ _399991) ^ [] : [-(in(_439994, _439816))], (1111 ^ _399991) ^ [] : [-(in(_439994, _439814))]]], (1113 ^ _399991) ^ [_440253] : [-(in(_440253, _439812)), in(_440253, _439816), in(_440253, _439814)]]], (1144 ^ _399991) ^ [_441276] : [relation(_441276), function(_441276), 1151 ^ _399991 : [(1152 ^ _399991) ^ [_441568, _441570] : [in(_441570, relation_dom(_441276)), 1155 ^ _399991 : [(1156 ^ _399991) ^ [] : [_441568 = apply(_441276, _441570), -(in(ordered_pair(_441570, _441568), _441276))], (1162 ^ _399991) ^ [] : [in(ordered_pair(_441570, _441568), _441276), -(_441568 = apply(_441276, _441570))]]], (1168 ^ _399991) ^ [_442020, _442022] : [-(in(_442022, relation_dom(_441276))), 1171 ^ _399991 : [(1172 ^ _399991) ^ [] : [_442020 = apply(_441276, _442022), -(_442020 = empty_set)], (1178 ^ _399991) ^ [] : [_442020 = empty_set, -(_442020 = apply(_441276, _442022))]]]]], (1184 ^ _399991) ^ [_442509] : [relation(_442509), 1187 ^ _399991 : [(1205 ^ _399991) ^ [_443321] : [-(_443321 = relation_dom(_442509)), 1209 ^ _399991 : [(1210 ^ _399991) ^ [] : [-(in(1206 ^ [_442509, _443321], _443321))], (1212 ^ _399991) ^ [_443584] : [in(ordered_pair(1206 ^ [_442509, _443321], _443584), _442509)]], 1214 ^ _399991 : [(1215 ^ _399991) ^ [] : [-(in(ordered_pair(1206 ^ [_442509, _443321], 1213 ^ [_442509, _443321]), _442509))], (1217 ^ _399991) ^ [] : [in(1206 ^ [_442509, _443321], _443321)]]], (1188 ^ _399991) ^ [_442690] : [_442690 = relation_dom(_442509), 1191 ^ _399991 : [(1192 ^ _399991) ^ [_442870] : [in(_442870, _442690), -(in(ordered_pair(_442870, 1195 ^ [_442509, _442690, _442870]), _442509))], (1199 ^ _399991) ^ [_443114] : [1200 ^ _399991 : [(1201 ^ _399991) ^ [_443193] : [in(ordered_pair(_443114, _443193), _442509)]], -(in(_443114, _442690))]]]]], (1221 ^ _399991) ^ [_443935] : [-(cast_to_subset(_443935) = _443935)], (1246 ^ _399991) ^ [_444918, _444920] : [-(_444918 = union(_444920)), 1259 ^ _399991 : [(1260 ^ _399991) ^ [] : [-(in(1247 ^ [_444918, _444920], 1258 ^ [_444918, _444920]))], (1262 ^ _399991) ^ [] : [-(in(1258 ^ [_444918, _444920], _444920))], (1264 ^ _399991) ^ [] : [in(1247 ^ [_444918, _444920], _444918)]], 1250 ^ _399991 : [(1251 ^ _399991) ^ [] : [-(in(1247 ^ [_444918, _444920], _444918))], (1253 ^ _399991) ^ [_445201] : [in(1247 ^ [_444918, _444920], _445201), in(_445201, _444920)]]], (1223 ^ _399991) ^ [_444073, _444075] : [_444073 = union(_444075), 1226 ^ _399991 : [(1227 ^ _399991) ^ [_444254] : [in(_444254, _444073), 1231 ^ _399991 : [(1232 ^ _399991) ^ [] : [-(in(_444254, 1230 ^ [_444073, _444075, _444254]))], (1234 ^ _399991) ^ [] : [-(in(1230 ^ [_444073, _444075, _444254], _444075))]]], (1236 ^ _399991) ^ [_444581] : [-(in(_444581, _444073)), 1237 ^ _399991 : [(1238 ^ _399991) ^ [_444679] : [in(_444581, _444679), in(_444679, _444075)]]]]], (1290 ^ _399991) ^ [_446539, _446541, _446543] : [-(_446539 = set_difference(_446543, _446541)), 1302 ^ _399991 : [(1303 ^ _399991) ^ [] : [-(in(1291 ^ [_446539, _446541, _446543], _446543))], (1305 ^ _399991) ^ [] : [in(1291 ^ [_446539, _446541, _446543], _446541)], (1307 ^ _399991) ^ [] : [in(1291 ^ [_446539, _446541, _446543], _446539)]], 1294 ^ _399991 : [(1295 ^ _399991) ^ [] : [-(in(1291 ^ [_446539, _446541, _446543], _446539))], (1297 ^ _399991) ^ [] : [in(1291 ^ [_446539, _446541, _446543], _446543), -(in(1291 ^ [_446539, _446541, _446543], _446541))]]], (1268 ^ _399991) ^ [_445808, _445810, _445812] : [_445808 = set_difference(_445812, _445810), 1271 ^ _399991 : [(1272 ^ _399991) ^ [_445992] : [in(_445992, _445808), 1275 ^ _399991 : [(1276 ^ _399991) ^ [] : [-(in(_445992, _445812))], (1278 ^ _399991) ^ [] : [in(_445992, _445810)]]], (1280 ^ _399991) ^ [_446252] : [-(in(_446252, _445808)), in(_446252, _445812), -(in(_446252, _445810))]]], (1311 ^ _399991) ^ [_447282] : [relation(_447282), 1314 ^ _399991 : [(1332 ^ _399991) ^ [_448094] : [-(_448094 = relation_rng(_447282)), 1336 ^ _399991 : [(1337 ^ _399991) ^ [] : [-(in(1333 ^ [_447282, _448094], _448094))], (1339 ^ _399991) ^ [_448357] : [in(ordered_pair(_448357, 1333 ^ [_447282, _448094]), _447282)]], 1341 ^ _399991 : [(1342 ^ _399991) ^ [] : [-(in(ordered_pair(1340 ^ [_447282, _448094], 1333 ^ [_447282, _448094]), _447282))], (1344 ^ _399991) ^ [] : [in(1333 ^ [_447282, _448094], _448094)]]], (1315 ^ _399991) ^ [_447463] : [_447463 = relation_rng(_447282), 1318 ^ _399991 : [(1319 ^ _399991) ^ [_447643] : [in(_447643, _447463), -(in(ordered_pair(1322 ^ [_447282, _447463, _447643], _447643), _447282))], (1326 ^ _399991) ^ [_447887] : [1327 ^ _399991 : [(1328 ^ _399991) ^ [_447966] : [in(ordered_pair(_447966, _447887), _447282)]], -(in(_447887, _447463))]]]]], (1348 ^ _399991) ^ [_448737, _448739] : [element(_448737, powerset(_448739)), -(subset_complement(_448739, _448737) = set_difference(_448739, _448737))], (1354 ^ _399991) ^ [_448948, _448950] : [-(ordered_pair(_448950, _448948) = unordered_pair(unordered_pair(_448950, _448948), singleton(_448950)))], (1356 ^ _399991) ^ [_449054] : [relation(_449054), -(relation_field(_449054) = set_union2(relation_dom(_449054), relation_rng(_449054)))], (1362 ^ _399991) ^ [_449260] : [relation(_449260), 1365 ^ _399991 : [(1366 ^ _399991) ^ [_449420] : [relation(_449420), 1369 ^ _399991 : [(1386 ^ _399991) ^ [] : [-(_449420 = relation_inverse(_449260)), 1391 ^ _399991 : [(1392 ^ _399991) ^ [] : [-(in(ordered_pair(1387 ^ [_449260, _449420], 1388 ^ [_449260, _449420]), _449420))], (1394 ^ _399991) ^ [] : [in(ordered_pair(1388 ^ [_449260, _449420], 1387 ^ [_449260, _449420]), _449260)]], 1395 ^ _399991 : [(1396 ^ _399991) ^ [] : [-(in(ordered_pair(1388 ^ [_449260, _449420], 1387 ^ [_449260, _449420]), _449260))], (1398 ^ _399991) ^ [] : [in(ordered_pair(1387 ^ [_449260, _449420], 1388 ^ [_449260, _449420]), _449420)]]], (1370 ^ _399991) ^ [] : [_449420 = relation_inverse(_449260), 1373 ^ _399991 : [(1374 ^ _399991) ^ [_449729, _449731] : [in(ordered_pair(_449731, _449729), _449420), -(in(ordered_pair(_449729, _449731), _449260))], (1380 ^ _399991) ^ [_449919, _449921] : [in(ordered_pair(_449919, _449921), _449260), -(in(ordered_pair(_449921, _449919), _449420))]]]]]]], (1402 ^ _399991) ^ [_450767, _450769] : [disjoint(_450769, _450767), -(set_intersection2(_450769, _450767) = empty_set)], (1408 ^ _399991) ^ [_450935, _450937] : [set_intersection2(_450937, _450935) = empty_set, -(disjoint(_450937, _450935))], (1414 ^ _399991) ^ [_451139] : [relation(_451139), 1417 ^ _399991 : [(1418 ^ _399991) ^ [_451324] : [relation(_451324), 1421 ^ _399991 : [(1422 ^ _399991) ^ [_451505] : [relation(_451505), 1425 ^ _399991 : [(1449 ^ _399991) ^ [] : [-(_451505 = relation_composition(_451139, _451324)), 1463 ^ _399991 : [(1464 ^ _399991) ^ [] : [-(in(ordered_pair(1450 ^ [_451139, _451324, _451505], 1462 ^ [_451139, _451324, _451505]), _451139))], (1466 ^ _399991) ^ [] : [-(in(ordered_pair(1462 ^ [_451139, _451324, _451505], 1451 ^ [_451139, _451324, _451505]), _451324))], (1468 ^ _399991) ^ [] : [in(ordered_pair(1450 ^ [_451139, _451324, _451505], 1451 ^ [_451139, _451324, _451505]), _451505)]], 1454 ^ _399991 : [(1455 ^ _399991) ^ [] : [-(in(ordered_pair(1450 ^ [_451139, _451324, _451505], 1451 ^ [_451139, _451324, _451505]), _451505))], (1457 ^ _399991) ^ [_452969] : [in(ordered_pair(1450 ^ [_451139, _451324, _451505], _452969), _451139), in(ordered_pair(_452969, 1451 ^ [_451139, _451324, _451505]), _451324)]]], (1426 ^ _399991) ^ [] : [_451505 = relation_composition(_451139, _451324), 1429 ^ _399991 : [(1430 ^ _399991) ^ [_451840, _451842] : [in(ordered_pair(_451842, _451840), _451505), 1434 ^ _399991 : [(1435 ^ _399991) ^ [] : [-(in(ordered_pair(_451842, 1433 ^ [_451139, _451324, _451505, _451840, _451842]), _451139))], (1437 ^ _399991) ^ [] : [-(in(ordered_pair(1433 ^ [_451139, _451324, _451505, _451840, _451842], _451840), _451324))]]], (1439 ^ _399991) ^ [_452225, _452227] : [-(in(ordered_pair(_452227, _452225), _451505)), 1440 ^ _399991 : [(1441 ^ _399991) ^ [_452338] : [in(ordered_pair(_452227, _452338), _451139), in(ordered_pair(_452338, _452225), _451324)]]]]]]]]]]], (1472 ^ _399991) ^ [_453655, _453657] : [element(_453655, powerset(powerset(_453657))), 1475 ^ _399991 : [(1476 ^ _399991) ^ [_453835] : [element(_453835, powerset(powerset(_453657))), 1479 ^ _399991 : [(1500 ^ _399991) ^ [] : [-(_453835 = complements_of_subsets(_453657, _453655)), 1502 ^ _399991 : [(1503 ^ _399991) ^ [] : [-(element(1501 ^ [_453655, _453657, _453835], powerset(_453657)))], (1505 ^ _399991) ^ [] : [1506 ^ _399991 : [(1507 ^ _399991) ^ [] : [-(in(1501 ^ [_453655, _453657, _453835], _453835))], (1509 ^ _399991) ^ [] : [in(subset_complement(_453657, 1501 ^ [_453655, _453657, _453835]), _453655)]], 1510 ^ _399991 : [(1511 ^ _399991) ^ [] : [-(in(subset_complement(_453657, 1501 ^ [_453655, _453657, _453835]), _453655))], (1513 ^ _399991) ^ [] : [in(1501 ^ [_453655, _453657, _453835], _453835)]]]]], (1480 ^ _399991) ^ [] : [_453835 = complements_of_subsets(_453657, _453655), 1483 ^ _399991 : [(1484 ^ _399991) ^ [_454123] : [element(_454123, powerset(_453657)), 1487 ^ _399991 : [(1488 ^ _399991) ^ [] : [in(_454123, _453835), -(in(subset_complement(_453657, _454123), _453655))], (1494 ^ _399991) ^ [] : [in(subset_complement(_453657, _454123), _453655), -(in(_454123, _453835))]]]]]]]]], (1517 ^ _399991) ^ [_455246, _455248] : [proper_subset(_455248, _455246), 1520 ^ _399991 : [(1521 ^ _399991) ^ [] : [-(subset(_455248, _455246))], (1523 ^ _399991) ^ [] : [_455248 = _455246]]], (1525 ^ _399991) ^ [_455484, _455486] : [-(proper_subset(_455486, _455484)), subset(_455486, _455484), -(_455486 = _455484)], (1535 ^ _399991) ^ [] : [true___, -(true___)], (1541 ^ _399991) ^ [] : [true___, -(true___)], (1547 ^ _399991) ^ [] : [true___, -(true___)], (1553 ^ _399991) ^ [] : [true___, -(true___)], (1559 ^ _399991) ^ [] : [true___, -(true___)], (1565 ^ _399991) ^ [] : [true___, -(true___)], (1571 ^ _399991) ^ [] : [true___, -(true___)], (1577 ^ _399991) ^ [] : [true___, -(true___)], (1583 ^ _399991) ^ [_456711] : [-(element(cast_to_subset(_456711), powerset(_456711)))], (1585 ^ _399991) ^ [] : [true___, -(true___)], (1591 ^ _399991) ^ [] : [true___, -(true___)], (1597 ^ _399991) ^ [] : [true___, -(true___)], (1603 ^ _399991) ^ [] : [true___, -(true___)], (1609 ^ _399991) ^ [_457298, _457300] : [element(_457298, powerset(_457300)), -(element(subset_complement(_457300, _457298), powerset(_457300)))], (1615 ^ _399991) ^ [] : [true___, -(true___)], (1621 ^ _399991) ^ [] : [true___, -(true___)], (1627 ^ _399991) ^ [_457746] : [relation(_457746), -(relation(relation_inverse(_457746)))], (1633 ^ _399991) ^ [] : [true___, -(true___)], (1639 ^ _399991) ^ [] : [true___, -(true___)], (1645 ^ _399991) ^ [_458188, _458190] : [-(relation(relation_composition(_458190, _458188))), relation(_458190), relation(_458188)], (1655 ^ _399991) ^ [_458487, _458489] : [element(_458487, powerset(powerset(_458489))), -(element(union_of_subsets(_458489, _458487), powerset(_458489)))], (1661 ^ _399991) ^ [_458686] : [-(relation(identity_relation(_458686)))], (1663 ^ _399991) ^ [_458794, _458796] : [element(_458794, powerset(powerset(_458796))), -(element(meet_of_subsets(_458796, _458794), powerset(_458796)))], (1669 ^ _399991) ^ [_459036, _459038, _459040] : [-(element(subset_difference(_459040, _459038, _459036), powerset(_459040))), element(_459038, powerset(_459040)), element(_459036, powerset(_459040))], (1679 ^ _399991) ^ [_459365, _459367] : [relation(_459367), -(relation(relation_dom_restriction(_459367, _459365)))], (1685 ^ _399991) ^ [_459577, _459579] : [element(_459577, powerset(powerset(_459579))), -(element(complements_of_subsets(_459579, _459577), powerset(powerset(_459579))))], (1691 ^ _399991) ^ [_459809, _459811] : [relation(_459809), -(relation(relation_rng_restriction(_459811, _459809)))], (1697 ^ _399991) ^ [] : [true___, -(true___)], (1703 ^ _399991) ^ [] : [true___, -(true___)], (1710 ^ _399991) ^ [_460269] : [-(element(1708 ^ [_460269], _460269))], (1712 ^ _399991) ^ [_460381, _460383] : [1719 ^ _399991 : [(1720 ^ _399991) ^ [] : [-(empty(relation_composition(_460381, _460383)))], (1722 ^ _399991) ^ [] : [-(relation(relation_composition(_460381, _460383)))]], empty(_460383), relation(_460381)], (1724 ^ _399991) ^ [] : [-(empty(empty_set))], (1726 ^ _399991) ^ [] : [-(relation(empty_set))], (1728 ^ _399991) ^ [] : [-(relation_empty_yielding(empty_set))], (1730 ^ _399991) ^ [_460922, _460924] : [-(relation(set_intersection2(_460924, _460922))), relation(_460924), relation(_460922)], (1740 ^ _399991) ^ [_461191] : [empty(powerset(_461191))], (1742 ^ _399991) ^ [] : [-(empty(empty_set))], (1744 ^ _399991) ^ [_461336, _461338] : [empty(ordered_pair(_461338, _461336))], (1746 ^ _399991) ^ [_461447, _461449] : [-(relation(set_union2(_461449, _461447))), relation(_461449), relation(_461447)], (1756 ^ _399991) ^ [_461716] : [empty(singleton(_461716))], (1758 ^ _399991) ^ [_461824, _461826] : [-(empty(_461826)), empty(set_union2(_461826, _461824))], (1764 ^ _399991) ^ [_462024, _462026] : [empty(unordered_pair(_462026, _462024))], (1766 ^ _399991) ^ [_462135, _462137] : [-(empty(_462137)), empty(set_union2(_462135, _462137))], (1772 ^ _399991) ^ [] : [-(empty(empty_set))], (1774 ^ _399991) ^ [] : [-(relation(empty_set))], (1776 ^ _399991) ^ [_462459, _462461] : [empty(cartesian_product2(_462461, _462459)), -(empty(_462461)), -(empty(_462459))], (1786 ^ _399991) ^ [_462751] : [empty(relation_dom(_462751)), -(empty(_462751)), relation(_462751)], (1796 ^ _399991) ^ [_463028] : [empty(relation_rng(_463028)), -(empty(_463028)), relation(_463028)], (1806 ^ _399991) ^ [_463305] : [empty(_463305), 1809 ^ _399991 : [(1810 ^ _399991) ^ [] : [-(empty(relation_dom(_463305)))], (1812 ^ _399991) ^ [] : [-(relation(relation_dom(_463305)))]]], (1814 ^ _399991) ^ [_463570] : [empty(_463570), 1817 ^ _399991 : [(1818 ^ _399991) ^ [] : [-(empty(relation_rng(_463570)))], (1820 ^ _399991) ^ [] : [-(relation(relation_rng(_463570)))]]], (1822 ^ _399991) ^ [_463849, _463851] : [1829 ^ _399991 : [(1830 ^ _399991) ^ [] : [-(empty(relation_composition(_463851, _463849)))], (1832 ^ _399991) ^ [] : [-(relation(relation_composition(_463851, _463849)))]], empty(_463851), relation(_463849)], (1834 ^ _399991) ^ [_464212, _464214] : [-(set_union2(_464214, _464214) = _464214)], (1836 ^ _399991) ^ [_464309, _464311] : [-(set_intersection2(_464311, _464311) = _464311)], (1838 ^ _399991) ^ [_464421, _464423] : [element(_464421, powerset(_464423)), -(subset_complement(_464423, subset_complement(_464423, _464421)) = _464421)], (1844 ^ _399991) ^ [_464633] : [relation(_464633), -(relation_inverse(relation_inverse(_464633)) = _464633)], (1850 ^ _399991) ^ [_464843, _464845] : [element(_464843, powerset(powerset(_464845))), -(complements_of_subsets(_464845, complements_of_subsets(_464845, _464843)) = _464843)], (1856 ^ _399991) ^ [_465057, _465059] : [proper_subset(_465059, _465059)], (1858 ^ _399991) ^ [_465136] : [singleton(_465136) = empty_set], (1860 ^ _399991) ^ [_465245, _465247] : [in(_465247, _465245), -(set_union2(singleton(_465247), _465245) = _465245)], (1866 ^ _399991) ^ [_465465, _465467] : [disjoint(singleton(_465467), _465465), in(_465467, _465465)], (1872 ^ _399991) ^ [_465678, _465680] : [-(in(_465680, _465678)), -(disjoint(singleton(_465680), _465678))], (1878 ^ _399991) ^ [_465924, _465926] : [subset(singleton(_465926), _465924), -(in(_465926, _465924))], (1884 ^ _399991) ^ [_466090, _466092] : [in(_466092, _466090), -(subset(singleton(_466092), _466090))], (1890 ^ _399991) ^ [_466335, _466337] : [set_difference(_466337, _466335) = empty_set, -(subset(_466337, _466335))], (1896 ^ _399991) ^ [_466503, _466505] : [subset(_466505, _466503), -(set_difference(_466505, _466503) = empty_set)], (1902 ^ _399991) ^ [_466721, _466723] : [element(_466721, powerset(_466723)), 1905 ^ _399991 : [(1906 ^ _399991) ^ [_466862] : [in(_466862, _466721), -(in(_466862, _466723))]]], (1912 ^ _399991) ^ [_467101, _467103, _467105] : [subset(_467105, _467103), -(in(_467101, _467105)), -(subset(_467105, set_difference(_467103, singleton(_467101))))], (1932 ^ _399991) ^ [_467710, _467712] : [1933 ^ _399991 : [(1934 ^ _399991) ^ [] : [_467712 = empty_set], (1936 ^ _399991) ^ [] : [_467712 = singleton(_467710)]], -(subset(_467712, singleton(_467710)))], (1922 ^ _399991) ^ [_467450, _467452] : [subset(_467452, singleton(_467450)), -(_467452 = empty_set), -(_467452 = singleton(_467450))], (1940 ^ _399991) ^ [_468004, _468006] : [in(_468006, _468004), -(subset(_468006, union(_468004)))], (1946 ^ _399991) ^ [_468275, _468277, _468279, _468281] : [in(ordered_pair(_468281, _468279), cartesian_product2(_468277, _468275)), 1949 ^ _399991 : [(1950 ^ _399991) ^ [] : [-(in(_468281, _468277))], (1952 ^ _399991) ^ [] : [-(in(_468279, _468275))]]], (1954 ^ _399991) ^ [_468540, _468542, _468544, _468546] : [-(in(ordered_pair(_468546, _468544), cartesian_product2(_468542, _468540))), in(_468546, _468542), in(_468544, _468540)], (1964 ^ _399991) ^ [_468873, _468875] : [1966 ^ _399991 : [(1967 ^ _399991) ^ [] : [-(in(1965 ^ [_468873, _468875], _468875))], (1969 ^ _399991) ^ [] : [in(1965 ^ [_468873, _468875], _468873)]], -(element(_468875, powerset(_468873)))], (1974 ^ _399991) ^ [] : [-(relation(1972 ^ []))], (1976 ^ _399991) ^ [] : [-(function(1972 ^ []))], (1979 ^ _399991) ^ [] : [-(empty(1977 ^ []))], (1981 ^ _399991) ^ [] : [-(relation(1977 ^ []))], (1983 ^ _399991) ^ [_469516] : [-(empty(_469516)), 1987 ^ _399991 : [(1988 ^ _399991) ^ [] : [-(element(1986 ^ [_469516], powerset(_469516)))], (1990 ^ _399991) ^ [] : [empty(1986 ^ [_469516])]]], (1993 ^ _399991) ^ [] : [-(empty(1991 ^ []))], (1996 ^ _399991) ^ [] : [empty(1994 ^ [])], (1998 ^ _399991) ^ [] : [-(relation(1994 ^ []))], (2001 ^ _399991) ^ [_470138] : [-(element(1999 ^ [_470138], powerset(_470138)))], (2003 ^ _399991) ^ [_470189] : [-(empty(1999 ^ [_470189]))], (2006 ^ _399991) ^ [] : [empty(2004 ^ [])], (2009 ^ _399991) ^ [] : [-(relation(2007 ^ []))], (2011 ^ _399991) ^ [] : [-(relation_empty_yielding(2007 ^ []))], (2013 ^ _399991) ^ [_470541, _470543] : [element(_470541, powerset(powerset(_470543))), -(union_of_subsets(_470543, _470541) = union(_470541))], (2019 ^ _399991) ^ [_470769, _470771] : [element(_470769, powerset(powerset(_470771))), -(meet_of_subsets(_470771, _470769) = set_meet(_470769))], (2025 ^ _399991) ^ [_471011, _471013, _471015] : [-(subset_difference(_471015, _471013, _471011) = set_difference(_471013, _471011)), element(_471013, powerset(_471015)), element(_471011, powerset(_471015))], (2035 ^ _399991) ^ [_471327, _471329] : [-(subset(_471329, _471329))], (2037 ^ _399991) ^ [_471436, _471438] : [disjoint(_471438, _471436), -(disjoint(_471436, _471438))], (2043 ^ _399991) ^ [_471703, _471705, _471707, _471709] : [in(ordered_pair(_471709, _471707), cartesian_product2(_471705, _471703)), 2046 ^ _399991 : [(2047 ^ _399991) ^ [] : [-(in(_471709, _471705))], (2049 ^ _399991) ^ [] : [-(in(_471707, _471703))]]], (2051 ^ _399991) ^ [_471968, _471970, _471972, _471974] : [-(in(ordered_pair(_471974, _471972), cartesian_product2(_471970, _471968))), in(_471974, _471970), in(_471972, _471968)], (2061 ^ _399991) ^ [_472329, _472331, _472333, _472335] : [unordered_pair(_472335, _472333) = unordered_pair(_472331, _472329), -(_472335 = _472331), -(_472335 = _472329)], (2071 ^ _399991) ^ [_472679, _472681, _472683] : [relation(_472679), 2074 ^ _399991 : [(2075 ^ _399991) ^ [] : [in(_472683, relation_rng(relation_rng_restriction(_472681, _472679))), 2078 ^ _399991 : [(2079 ^ _399991) ^ [] : [-(in(_472683, _472681))], (2081 ^ _399991) ^ [] : [-(in(_472683, relation_rng(_472679)))]]], (2083 ^ _399991) ^ [] : [-(in(_472683, relation_rng(relation_rng_restriction(_472681, _472679)))), in(_472683, _472681), in(_472683, relation_rng(_472679))]]], (2093 ^ _399991) ^ [_473338, _473340] : [relation(_473338), -(subset(relation_rng(relation_rng_restriction(_473340, _473338)), _473340))], (2099 ^ _399991) ^ [_473556, _473558] : [relation(_473556), -(subset(relation_rng_restriction(_473558, _473556), _473556))], (2105 ^ _399991) ^ [_473770, _473772] : [relation(_473770), -(subset(relation_rng(relation_rng_restriction(_473772, _473770)), relation_rng(_473770)))], (2111 ^ _399991) ^ [_474006, _474008, _474010] : [subset(_474010, _474008), 2114 ^ _399991 : [(2115 ^ _399991) ^ [] : [-(subset(cartesian_product2(_474010, _474006), cartesian_product2(_474008, _474006)))], (2117 ^ _399991) ^ [] : [-(subset(cartesian_product2(_474006, _474010), cartesian_product2(_474006, _474008)))]]], (2119 ^ _399991) ^ [_474323, _474325] : [relation(_474323), -(relation_rng(relation_rng_restriction(_474325, _474323)) = set_intersection2(relation_rng(_474323), _474325))], (2125 ^ _399991) ^ [_474579, _474581, _474583, _474585] : [-(subset(cartesian_product2(_474585, _474581), cartesian_product2(_474583, _474579))), subset(_474585, _474583), subset(_474581, _474579)], (2135 ^ _399991) ^ [_474910, _474912] : [subset(_474912, _474910), -(set_union2(_474912, _474910) = _474910)], (2142 ^ _399991) ^ [_475232] : [-(in(_475232, 2140 ^ [_475232]))], (2144 ^ _399991) ^ [_475344, _475346, _475348] : [-(in(_475344, 2140 ^ [_475348])), in(_475346, 2140 ^ [_475348]), subset(_475344, _475346)], (2154 ^ _399991) ^ [_475659, _475661] : [in(_475659, 2140 ^ [_475661]), -(in(powerset(_475659), 2140 ^ [_475661]))], (2160 ^ _399991) ^ [_475859, _475861] : [subset(_475859, 2140 ^ [_475861]), -(are_equipotent(_475859, 2140 ^ [_475861])), -(in(_475859, 2140 ^ [_475861]))], (2170 ^ _399991) ^ [_476213, _476215, _476217] : [relation(_476213), -(relation_dom_restriction(relation_rng_restriction(_476217, _476213), _476215) = relation_rng_restriction(_476217, relation_dom_restriction(_476213, _476215)))], (2176 ^ _399991) ^ [_476465, _476467, _476469] : [relation(_476465), 2179 ^ _399991 : [(2180 ^ _399991) ^ [] : [in(_476469, relation_image(_476465, _476467)), 2184 ^ _399991 : [(2185 ^ _399991) ^ [] : [-(in(2183 ^ [_476465, _476467, _476469], relation_dom(_476465)))], (2187 ^ _399991) ^ [] : [-(in(ordered_pair(2183 ^ [_476465, _476467, _476469], _476469), _476465))], (2189 ^ _399991) ^ [] : [-(in(2183 ^ [_476465, _476467, _476469], _476467))]]], (2191 ^ _399991) ^ [] : [-(in(_476469, relation_image(_476465, _476467))), 2192 ^ _399991 : [(2193 ^ _399991) ^ [_477066] : [in(_477066, relation_dom(_476465)), in(ordered_pair(_477066, _476469), _476465), in(_477066, _476467)]]]]], (2205 ^ _399991) ^ [_477463, _477465] : [relation(_477463), -(subset(relation_image(_477463, _477465), relation_rng(_477463)))], (2211 ^ _399991) ^ [_477681, _477683] : [relation(_477681), -(relation_image(_477681, _477683) = relation_image(_477681, set_intersection2(relation_dom(_477681), _477683)))], (2217 ^ _399991) ^ [_477897] : [relation(_477897), -(relation_image(_477897, relation_dom(_477897)) = relation_rng(_477897))], (2223 ^ _399991) ^ [_478099] : [relation(_478099), 2226 ^ _399991 : [(2227 ^ _399991) ^ [_478239] : [relation(_478239), -(relation_rng(relation_composition(_478099, _478239)) = relation_image(_478239, relation_rng(_478099)))]]], (2233 ^ _399991) ^ [_478488, _478490, _478492] : [relation(_478488), 2236 ^ _399991 : [(2237 ^ _399991) ^ [] : [in(_478492, relation_inverse_image(_478488, _478490)), 2241 ^ _399991 : [(2242 ^ _399991) ^ [] : [-(in(2240 ^ [_478488, _478490, _478492], relation_rng(_478488)))], (2244 ^ _399991) ^ [] : [-(in(ordered_pair(_478492, 2240 ^ [_478488, _478490, _478492]), _478488))], (2246 ^ _399991) ^ [] : [-(in(2240 ^ [_478488, _478490, _478492], _478490))]]], (2248 ^ _399991) ^ [] : [-(in(_478492, relation_inverse_image(_478488, _478490))), 2249 ^ _399991 : [(2250 ^ _399991) ^ [_479089] : [in(_479089, relation_rng(_478488)), in(ordered_pair(_478492, _479089), _478488), in(_479089, _478490)]]]]], (2262 ^ _399991) ^ [_479486, _479488] : [relation(_479486), -(subset(relation_inverse_image(_479486, _479488), relation_dom(_479486)))], (2268 ^ _399991) ^ [_479704, _479706] : [relation(_479704), -(_479706 = empty_set), subset(_479706, relation_rng(_479704)), relation_inverse_image(_479704, _479706) = empty_set], (2282 ^ _399991) ^ [_480118, _480120, _480122] : [relation(_480118), subset(_480122, _480120), -(subset(relation_inverse_image(_480118, _480122), relation_inverse_image(_480118, _480120)))], (2292 ^ _399991) ^ [_480422, _480424] : [-(subset(set_intersection2(_480424, _480422), _480424))], (2294 ^ _399991) ^ [_480548, _480550, _480552] : [-(subset(_480552, set_intersection2(_480550, _480548))), subset(_480552, _480550), subset(_480552, _480548)], (2304 ^ _399991) ^ [_480834] : [-(set_union2(_480834, empty_set) = _480834)], (2306 ^ _399991) ^ [_480944, _480946] : [in(_480946, _480944), -(element(_480946, _480944))], (2312 ^ _399991) ^ [_481168, _481170, _481172] : [-(subset(_481172, _481168)), subset(_481172, _481170), subset(_481170, _481168)], (2322 ^ _399991) ^ [] : [-(powerset(empty_set) = singleton(empty_set))], (2324 ^ _399991) ^ [_481544, _481546, _481548] : [relation(_481544), in(ordered_pair(_481548, _481546), _481544), 2331 ^ _399991 : [(2332 ^ _399991) ^ [] : [-(in(_481548, relation_dom(_481544)))], (2334 ^ _399991) ^ [] : [-(in(_481546, relation_rng(_481544)))]]], (2336 ^ _399991) ^ [_481928] : [relation(_481928), -(subset(_481928, cartesian_product2(relation_dom(_481928), relation_rng(_481928))))], (2342 ^ _399991) ^ [_482130] : [relation(_482130), 2345 ^ _399991 : [(2346 ^ _399991) ^ [_482280] : [relation(_482280), subset(_482130, _482280), 2353 ^ _399991 : [(2354 ^ _399991) ^ [] : [-(subset(relation_dom(_482130), relation_dom(_482280)))], (2356 ^ _399991) ^ [] : [-(subset(relation_rng(_482130), relation_rng(_482280)))]]]]], (2358 ^ _399991) ^ [_482689, _482691, _482693] : [subset(_482693, _482691), -(subset(set_intersection2(_482693, _482689), set_intersection2(_482691, _482689)))], (2364 ^ _399991) ^ [_482917, _482919] : [subset(_482919, _482917), -(set_intersection2(_482919, _482917) = _482919)], (2370 ^ _399991) ^ [_483104] : [-(set_intersection2(_483104, empty_set) = empty_set)], (2372 ^ _399991) ^ [_483214, _483216] : [element(_483216, _483214), -(empty(_483214)), -(in(_483216, _483214))], (2382 ^ _399991) ^ [_483512, _483514] : [-(_483514 = _483512), 2386 ^ _399991 : [(2387 ^ _399991) ^ [] : [-(in(2383 ^ [_483512, _483514], _483514))], (2389 ^ _399991) ^ [] : [in(2383 ^ [_483512, _483514], _483512)]], 2390 ^ _399991 : [(2391 ^ _399991) ^ [] : [-(in(2383 ^ [_483512, _483514], _483512))], (2393 ^ _399991) ^ [] : [in(2383 ^ [_483512, _483514], _483514)]]], (2397 ^ _399991) ^ [_484013] : [-(subset(empty_set, _484013))], (2399 ^ _399991) ^ [_484134, _484136, _484138] : [relation(_484134), in(ordered_pair(_484138, _484136), _484134), 2406 ^ _399991 : [(2407 ^ _399991) ^ [] : [-(in(_484138, relation_field(_484134)))], (2409 ^ _399991) ^ [] : [-(in(_484136, relation_field(_484134)))]]], (2411 ^ _399991) ^ [_484546, _484548, _484550] : [subset(_484550, _484548), -(subset(set_difference(_484550, _484546), set_difference(_484548, _484546)))], (2417 ^ _399991) ^ [_484802, _484804, _484806, _484808] : [ordered_pair(_484808, _484806) = ordered_pair(_484804, _484802), 2420 ^ _399991 : [(2421 ^ _399991) ^ [] : [-(_484808 = _484804)], (2423 ^ _399991) ^ [] : [-(_484806 = _484802)]]], (2425 ^ _399991) ^ [_485100, _485102] : [-(subset(set_difference(_485102, _485100), _485102))], (2427 ^ _399991) ^ [_485198] : [relation(_485198), 2430 ^ _399991 : [(2431 ^ _399991) ^ [] : [-(relation_rng(_485198) = relation_dom(relation_inverse(_485198)))], (2433 ^ _399991) ^ [] : [-(relation_dom(_485198) = relation_rng(relation_inverse(_485198)))]]], (2435 ^ _399991) ^ [_485526, _485528] : [set_difference(_485528, _485526) = empty_set, -(subset(_485528, _485526))], (2441 ^ _399991) ^ [_485694, _485696] : [subset(_485696, _485694), -(set_difference(_485696, _485694) = empty_set)], (2447 ^ _399991) ^ [_485941, _485943] : [subset(singleton(_485943), _485941), -(in(_485943, _485941))], (2453 ^ _399991) ^ [_486107, _486109] : [in(_486109, _486107), -(subset(singleton(_486109), _486107))], (2459 ^ _399991) ^ [_486366, _486368, _486370] : [subset(unordered_pair(_486370, _486368), _486366), 2462 ^ _399991 : [(2463 ^ _399991) ^ [] : [-(in(_486370, _486366))], (2465 ^ _399991) ^ [] : [-(in(_486368, _486366))]]], (2467 ^ _399991) ^ [_486617, _486619, _486621] : [-(subset(unordered_pair(_486621, _486619), _486617)), in(_486621, _486617), in(_486619, _486617)], (2477 ^ _399991) ^ [_486919, _486921] : [-(set_union2(_486921, set_difference(_486919, _486921)) = set_union2(_486921, _486919))], (2489 ^ _399991) ^ [_487326, _487328] : [2490 ^ _399991 : [(2491 ^ _399991) ^ [] : [_487328 = empty_set], (2493 ^ _399991) ^ [] : [_487328 = singleton(_487326)]], -(subset(_487328, singleton(_487326)))], (2479 ^ _399991) ^ [_487066, _487068] : [subset(_487068, singleton(_487066)), -(_487068 = empty_set), -(_487068 = singleton(_487066))], (2497 ^ _399991) ^ [_487591] : [-(set_difference(_487591, empty_set) = _487591)], (2499 ^ _399991) ^ [_487730, _487732] : [element(_487732, powerset(_487730)), -(subset(_487732, _487730))], (2505 ^ _399991) ^ [_487896, _487898] : [subset(_487898, _487896), -(element(_487898, powerset(_487896)))], (2511 ^ _399991) ^ [_488132, _488134] : [-(disjoint(_488134, _488132)), 2515 ^ _399991 : [(2516 ^ _399991) ^ [] : [-(in(2514 ^ [_488132, _488134], _488134))], (2518 ^ _399991) ^ [] : [-(in(2514 ^ [_488132, _488134], _488132))]]], (2520 ^ _399991) ^ [_488446, _488448] : [disjoint(_488448, _488446), 2521 ^ _399991 : [(2522 ^ _399991) ^ [_488538] : [in(_488538, _488448), in(_488538, _488446)]]], (2530 ^ _399991) ^ [_488795] : [subset(_488795, empty_set), -(_488795 = empty_set)], (2536 ^ _399991) ^ [_488984, _488986] : [-(set_difference(set_union2(_488986, _488984), _488984) = set_difference(_488986, _488984))], (2538 ^ _399991) ^ [_489102, _489104] : [element(_489102, powerset(_489104)), 2541 ^ _399991 : [(2542 ^ _399991) ^ [_489254] : [element(_489254, powerset(_489104)), 2545 ^ _399991 : [(2546 ^ _399991) ^ [] : [disjoint(_489102, _489254), -(subset(_489102, subset_complement(_489104, _489254)))], (2552 ^ _399991) ^ [] : [subset(_489102, subset_complement(_489104, _489254)), -(disjoint(_489102, _489254))]]]]], (2558 ^ _399991) ^ [_489738] : [relation(_489738), 2561 ^ _399991 : [(2562 ^ _399991) ^ [_489875] : [relation(_489875), -(subset(relation_dom(relation_composition(_489738, _489875)), relation_dom(_489738)))]]], (2568 ^ _399991) ^ [_490090] : [relation(_490090), 2571 ^ _399991 : [(2572 ^ _399991) ^ [_490227] : [relation(_490227), -(subset(relation_rng(relation_composition(_490090, _490227)), relation_rng(_490227)))]]], (2578 ^ _399991) ^ [_490456, _490458] : [subset(_490458, _490456), -(_490456 = set_union2(_490458, set_difference(_490456, _490458)))], (2584 ^ _399991) ^ [_490664] : [relation(_490664), 2587 ^ _399991 : [(2588 ^ _399991) ^ [_490811] : [relation(_490811), subset(relation_rng(_490664), relation_dom(_490811)), -(relation_dom(relation_composition(_490664, _490811)) = relation_dom(_490664))]]], (2598 ^ _399991) ^ [_491137, _491139] : [element(_491137, powerset(powerset(_491139))), -(_491137 = empty_set), complements_of_subsets(_491139, _491137) = empty_set], (2608 ^ _399991) ^ [_491454, _491456] : [in(_491456, _491454), -(set_union2(singleton(_491456), _491454) = _491454)], (2614 ^ _399991) ^ [_491660] : [relation(_491660), 2617 ^ _399991 : [(2618 ^ _399991) ^ [_491807] : [relation(_491807), subset(relation_dom(_491660), relation_rng(_491807)), -(relation_rng(relation_composition(_491807, _491660)) = relation_rng(_491660))]]], (2628 ^ _399991) ^ [_492133, _492135] : [element(_492133, powerset(powerset(_492135))), -(_492133 = empty_set), -(subset_difference(_492135, cast_to_subset(_492135), union_of_subsets(_492135, _492133)) = meet_of_subsets(_492135, complements_of_subsets(_492135, _492133)))], (2638 ^ _399991) ^ [_492473, _492475] : [element(_492473, powerset(powerset(_492475))), -(_492473 = empty_set), -(union_of_subsets(_492475, complements_of_subsets(_492475, _492473)) = subset_difference(_492475, cast_to_subset(_492475), meet_of_subsets(_492475, _492473)))], (2648 ^ _399991) ^ [_492798, _492800] : [-(set_difference(_492800, set_difference(_492800, _492798)) = set_intersection2(_492800, _492798))], (2650 ^ _399991) ^ [_492887] : [-(set_difference(empty_set, _492887) = empty_set)], (2652 ^ _399991) ^ [_493011, _493013, _493015] : [-(element(_493015, _493011)), in(_493015, _493013), element(_493013, powerset(_493011))], (2662 ^ _399991) ^ [_493344, _493346] : [-(disjoint(_493346, _493344)), -(in(2665 ^ [_493344, _493346], set_intersection2(_493346, _493344)))], (2669 ^ _399991) ^ [_493579, _493581] : [2670 ^ _399991 : [(2671 ^ _399991) ^ [_493652] : [in(_493652, set_intersection2(_493581, _493579))]], disjoint(_493581, _493579)], (2675 ^ _399991) ^ [_493804] : [-(_493804 = empty_set), 2678 ^ _399991 : [(2679 ^ _399991) ^ [_493964] : [element(_493964, powerset(_493804)), 2682 ^ _399991 : [(2683 ^ _399991) ^ [_494118] : [element(_494118, _493804), -(in(_494118, _493964)), -(in(_494118, subset_complement(_493804, _493964)))]]]]], (2693 ^ _399991) ^ [_494464, _494466, _494468] : [element(_494464, powerset(_494468)), in(_494466, subset_complement(_494468, _494464)), in(_494466, _494464)], (2703 ^ _399991) ^ [_494770] : [relation(_494770), -(in(ordered_pair(2708 ^ [_494770], 2709 ^ [_494770]), _494770)), -(_494770 = empty_set)], (2715 ^ _399991) ^ [_495202, _495204, _495206] : [in(_495206, _495204), element(_495204, powerset(_495202)), empty(_495202)], (2725 ^ _399991) ^ [] : [-(relation_dom(empty_set) = empty_set)], (2727 ^ _399991) ^ [] : [-(relation_rng(empty_set) = empty_set)], (2729 ^ _399991) ^ [_495620, _495622] : [subset(_495622, _495620), proper_subset(_495620, _495622)], (2735 ^ _399991) ^ [_495843, _495845, _495847] : [-(disjoint(_495847, _495843)), subset(_495847, _495845), disjoint(_495845, _495843)], (2745 ^ _399991) ^ [_496138] : [relation(_496138), 2750 ^ _399991 : [(2751 ^ _399991) ^ [] : [relation_dom(_496138) = empty_set], (2753 ^ _399991) ^ [] : [relation_rng(_496138) = empty_set]], -(_496138 = empty_set)], (2757 ^ _399991) ^ [_496491] : [relation(_496491), 2760 ^ _399991 : [(2761 ^ _399991) ^ [] : [relation_dom(_496491) = empty_set, -(relation_rng(_496491) = empty_set)], (2767 ^ _399991) ^ [] : [relation_rng(_496491) = empty_set, -(relation_dom(_496491) = empty_set)]]], (2773 ^ _399991) ^ [_496974, _496976] : [set_difference(_496976, singleton(_496974)) = _496976, in(_496974, _496976)], (2779 ^ _399991) ^ [_497147, _497149] : [-(in(_497147, _497149)), -(set_difference(_497149, singleton(_497147)) = _497149)], (2785 ^ _399991) ^ [_497343] : [-(unordered_pair(_497343, _497343) = singleton(_497343))], (2787 ^ _399991) ^ [_497441] : [empty(_497441), -(_497441 = empty_set)], (2793 ^ _399991) ^ [_497643, _497645] : [subset(singleton(_497645), singleton(_497643)), -(_497645 = _497643)], (2799 ^ _399991) ^ [_497852] : [-(relation_dom(identity_relation(_497852)) = _497852)], (2801 ^ _399991) ^ [_497900] : [-(relation_rng(identity_relation(_497900)) = _497900)], (2803 ^ _399991) ^ [_498041, _498043, _498045, _498047] : [relation(_498041), 2806 ^ _399991 : [(2807 ^ _399991) ^ [] : [in(ordered_pair(_498047, _498045), relation_composition(identity_relation(_498043), _498041)), 2810 ^ _399991 : [(2811 ^ _399991) ^ [] : [-(in(_498047, _498043))], (2813 ^ _399991) ^ [] : [-(in(ordered_pair(_498047, _498045), _498041))]]], (2815 ^ _399991) ^ [] : [-(in(ordered_pair(_498047, _498045), relation_composition(identity_relation(_498043), _498041))), in(_498047, _498043), in(ordered_pair(_498047, _498045), _498041)]]], (2825 ^ _399991) ^ [_498734, _498736] : [in(_498736, _498734), empty(_498734)], (2831 ^ _399991) ^ [_498926, _498928] : [-(subset(_498928, set_union2(_498928, _498926)))], (2833 ^ _399991) ^ [_499067, _499069] : [disjoint(_499069, _499067), -(set_difference(_499069, _499067) = _499069)], (2839 ^ _399991) ^ [_499235, _499237] : [set_difference(_499237, _499235) = _499237, -(disjoint(_499237, _499235))], (2845 ^ _399991) ^ [_499467, _499469, _499471] : [relation(_499467), 2848 ^ _399991 : [(2849 ^ _399991) ^ [] : [in(_499471, relation_dom(relation_dom_restriction(_499467, _499469))), 2852 ^ _399991 : [(2853 ^ _399991) ^ [] : [-(in(_499471, _499469))], (2855 ^ _399991) ^ [] : [-(in(_499471, relation_dom(_499467)))]]], (2857 ^ _399991) ^ [] : [-(in(_499471, relation_dom(relation_dom_restriction(_499467, _499469)))), in(_499471, _499469), in(_499471, relation_dom(_499467))]]], (2867 ^ _399991) ^ [_500126, _500128] : [relation(_500126), -(subset(relation_dom_restriction(_500126, _500128), _500126))], (2873 ^ _399991) ^ [_500340, _500342] : [empty(_500342), -(_500342 = _500340), empty(_500340)], (2883 ^ _399991) ^ [_500651, _500653, _500655] : [-(subset(set_union2(_500655, _500651), _500653)), subset(_500655, _500653), subset(_500651, _500653)], (2893 ^ _399991) ^ [_500980, _500982, _500984] : [singleton(_500984) = unordered_pair(_500982, _500980), -(_500984 = _500982)], (2899 ^ _399991) ^ [_501206, _501208] : [relation(_501206), -(relation_dom(relation_dom_restriction(_501206, _501208)) = set_intersection2(relation_dom(_501206), _501208))], (2905 ^ _399991) ^ [_501434, _501436] : [in(_501436, _501434), -(subset(_501436, union(_501434)))], (2911 ^ _399991) ^ [_501648, _501650] : [relation(_501648), -(relation_dom_restriction(_501648, _501650) = relation_composition(identity_relation(_501650), _501648))], (2917 ^ _399991) ^ [_501872, _501874] : [relation(_501872), -(subset(relation_rng(relation_dom_restriction(_501872, _501874)), relation_rng(_501872)))], (2923 ^ _399991) ^ [_502065] : [-(union(powerset(_502065)) = _502065)], (2961 ^ _399991) ^ [_503586, _503588, _503590] : [singleton(_503590) = unordered_pair(_503588, _503586), -(_503588 = _503586)], (2926 ^ _399991) ^ [_502306] : [-(in(_502306, 2924 ^ [_502306]))], (2928 ^ _399991) ^ [_502418, _502420, _502422] : [-(in(_502418, 2924 ^ [_502422])), in(_502420, 2924 ^ [_502422]), subset(_502418, _502420)], (2938 ^ _399991) ^ [_502733, _502735] : [in(_502733, 2924 ^ [_502735]), 2942 ^ _399991 : [(2943 ^ _399991) ^ [] : [-(in(2941 ^ [_502733, _502735], 2924 ^ [_502735]))], (2945 ^ _399991) ^ [_503045] : [subset(_503045, _502733), -(in(_503045, 2941 ^ [_502733, _502735]))]]], (2951 ^ _399991) ^ [_503252, _503254] : [subset(_503252, 2924 ^ [_503254]), -(are_equipotent(_503252, 2924 ^ [_503254])), -(in(_503252, 2924 ^ [_503254]))]], input).
% 0.39/1.37 ncf('1',plain,[2988 : in(ordered_pair(2966 ^ [], 2967 ^ []), 2968 ^ []), 2978 : in(2966 ^ [], relation_dom(2968 ^ [])), 2978 : 2967 ^ [] = apply(2968 ^ [], 2966 ^ [])],start(2974 ^ 0)).
% 0.39/1.37 ncf('1.1',plain,[-(in(ordered_pair(2966 ^ [], 2967 ^ []), 2968 ^ [])), 1156 : 2967 ^ [] = apply(2968 ^ [], 2966 ^ []), 1156 : in(2966 ^ [], relation_dom(2968 ^ [])), 1152 : relation(2968 ^ []), 1152 : function(2968 ^ [])],extension(1144 ^ 3,bind([[_441276, _441568, _441570], [2968 ^ [], 2967 ^ [], 2966 ^ []]]))).
% 0.39/1.37 ncf('1.1.1',plain,[-(2967 ^ [] = apply(2968 ^ [], 2966 ^ []))],extension(2986 ^ 8)).
% 0.39/1.37 ncf('1.1.2',plain,[-(in(2966 ^ [], relation_dom(2968 ^ [])))],extension(2984 ^ 6)).
% 0.39/1.37 ncf('1.1.3',plain,[-(relation(2968 ^ []))],extension(2970 ^ 4)).
% 0.39/1.37 ncf('1.1.4',plain,[-(function(2968 ^ []))],extension(2972 ^ 4)).
% 0.39/1.37 ncf('1.2',plain,[-(in(2966 ^ [], relation_dom(2968 ^ []))), relation(2968 ^ []), in(ordered_pair(2966 ^ [], 2967 ^ []), 2968 ^ [])],extension(2324 ^ 3,bind([[_481544, _481546, _481548], [2968 ^ [], 2967 ^ [], 2966 ^ []]]))).
% 0.39/1.37 ncf('1.2.1',plain,[-(relation(2968 ^ []))],extension(2970 ^ 4)).
% 0.39/1.37 ncf('1.2.2',plain,[-(in(ordered_pair(2966 ^ [], 2967 ^ []), 2968 ^ []))],extension(2976 ^ 4)).
% 0.39/1.37 ncf('1.3',plain,[-(2967 ^ [] = apply(2968 ^ [], 2966 ^ [])), 1162 : in(ordered_pair(2966 ^ [], 2967 ^ []), 2968 ^ []), 1162 : in(2966 ^ [], relation_dom(2968 ^ [])), 1152 : relation(2968 ^ []), 1152 : function(2968 ^ [])],extension(1144 ^ 3,bind([[_441276, _441568, _441570], [2968 ^ [], 2967 ^ [], 2966 ^ []]]))).
% 0.39/1.37 ncf('1.3.1',plain,[-(in(ordered_pair(2966 ^ [], 2967 ^ []), 2968 ^ []))],extension(2976 ^ 8)).
% 0.39/1.37 ncf('1.3.2',plain,[-(in(2966 ^ [], relation_dom(2968 ^ [])))],lemmata('x')).
% 0.39/1.37 ncf('1.3.3',plain,[-(relation(2968 ^ []))],extension(2970 ^ 4)).
% 0.39/1.37 ncf('1.3.4',plain,[-(function(2968 ^ []))],extension(2972 ^ 4)).
% 0.39/1.37 %-----------------------------------------------------
% 0.39/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------