%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM617+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n020.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 11:45:10 EDT 2023
% Result : Theorem 0.39s 1.38s
% Output : Proof 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM617+3 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n020.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 17:06:47 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.39/1.38
% 0.39/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.39/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/1.38 %-----------------------------------------------------
% 0.39/1.38 ncf(matrix, plain, [(2760 ^ _374570) ^ [] : [aElementOf0(xx, szNzAzT0)], (126 ^ _374570) ^ [_378591, _378593] : [_378593 = _378591, -(szmzazxdt0(_378593) = szmzazxdt0(_378591))], (132 ^ _374570) ^ [_378809, _378811] : [_378811 = _378809, -(slbdtrb0(_378811) = slbdtrb0(_378809))], (138 ^ _374570) ^ [_379055, _379057, _379059, _379061] : [-(sdtexdt0(_379061, _379057) = sdtexdt0(_379059, _379055)), _379061 = _379059, _379057 = _379055], (148 ^ _374570) ^ [_379414, _379416, _379418, _379420] : [-(sdtpldt0(_379420, _379416) = sdtpldt0(_379418, _379414)), _379420 = _379418, _379416 = _379414], (158 ^ _374570) ^ [_379745, _379747] : [_379747 = _379745, -(szszuzczcdt0(_379747) = szszuzczcdt0(_379745))], (164 ^ _374570) ^ [_379991, _379993, _379995, _379997] : [-(sdtlcdtrc0(_379997, _379993) = sdtlcdtrc0(_379995, _379991)), _379997 = _379995, _379993 = _379991], (174 ^ _374570) ^ [_380350, _380352, _380354, _380356] : [-(sdtmndt0(_380356, _380352) = sdtmndt0(_380354, _380350)), _380356 = _380354, _380352 = _380350], (184 ^ _374570) ^ [_380681, _380683] : [_380683 = _380681, -(sbrdtbr0(_380683) = sbrdtbr0(_380681))], (190 ^ _374570) ^ [_380927, _380929, _380931, _380933] : [-(slbdtsldtrb0(_380933, _380929) = slbdtsldtrb0(_380931, _380927)), _380933 = _380931, _380929 = _380927], (200 ^ _374570) ^ [_381258, _381260] : [_381260 = _381258, -(szDzozmdt0(_381260) = szDzozmdt0(_381258))], (206 ^ _374570) ^ [_381504, _381506, _381508, _381510] : [-(sdtlbdtrb0(_381510, _381506) = sdtlbdtrb0(_381508, _381504)), _381510 = _381508, _381506 = _381504], (216 ^ _374570) ^ [_381863, _381865, _381867, _381869] : [-(sdtlpdtrp0(_381869, _381865) = sdtlpdtrp0(_381867, _381863)), _381869 = _381867, _381865 = _381863], (226 ^ _374570) ^ [_382194, _382196] : [_382196 = _382194, -(szDzizrdt0(_382196) = szDzizrdt0(_382194))], (232 ^ _374570) ^ [_382392, _382394] : [_382394 = _382392, -(szmzizndt0(_382394) = szmzizndt0(_382392))], (2 ^ _374570) ^ [_374714] : [-(_374714 = _374714)], (4 ^ _374570) ^ [_374821, _374823] : [_374823 = _374821, -(_374821 = _374823)], (10 ^ _374570) ^ [_375025, _375027, _375029] : [-(_375029 = _375025), _375029 = _375027, _375027 = _375025], (20 ^ _374570) ^ [_375338, _375340] : [-(isFinite0(_375338)), _375340 = _375338, isFinite0(_375340)], (30 ^ _374570) ^ [_375661, _375663, _375665, _375667] : [-(iLess0(_375665, _375661)), iLess0(_375667, _375663), _375667 = _375665, _375663 = _375661], (44 ^ _374570) ^ [_376077, _376079] : [-(aFunction0(_376077)), _376079 = _376077, aFunction0(_376079)], (54 ^ _374570) ^ [_376372, _376374] : [-(isCountable0(_376372)), _376374 = _376372, isCountable0(_376374)], (64 ^ _374570) ^ [_376667, _376669] : [-(aSet0(_376667)), _376669 = _376667, aSet0(_376669)], (74 ^ _374570) ^ [_376990, _376992, _376994, _376996] : [-(sdtlseqdt0(_376994, _376990)), sdtlseqdt0(_376996, _376992), _376996 = _376994, _376992 = _376990], (88 ^ _374570) ^ [_377434, _377436, _377438, _377440] : [-(aSubsetOf0(_377438, _377434)), aSubsetOf0(_377440, _377436), _377440 = _377438, _377436 = _377434], (102 ^ _374570) ^ [_377850, _377852] : [-(aElement0(_377850)), _377852 = _377850, aElement0(_377852)], (112 ^ _374570) ^ [_378153, _378155, _378157, _378159] : [-(aElementOf0(_378157, _378153)), aElementOf0(_378159, _378155), _378159 = _378157, _378155 = _378153], (238 ^ _374570) ^ [_382682] : [aSet0(_382682), true___, -(true___)], (248 ^ _374570) ^ [_382937] : [aElement0(_382937), true___, -(true___)], (258 ^ _374570) ^ [_383192] : [aSet0(_383192), 261 ^ _374570 : [(262 ^ _374570) ^ [_383322] : [aElementOf0(_383322, _383192), -(aElement0(_383322))]]], (268 ^ _374570) ^ [_383523] : [aSet0(_383523), isFinite0(_383523), true___, -(true___)], (282 ^ _374570) ^ [_383893] : [_383893 = slcrc0, 285 ^ _374570 : [(286 ^ _374570) ^ [] : [-(aSet0(_383893))], (288 ^ _374570) ^ [_384074] : [aElementOf0(_384074, _383893)]]], (290 ^ _374570) ^ [_384142] : [-(_384142 = slcrc0), aSet0(_384142), -(aElementOf0(295 ^ [_384142], _384142))], (301 ^ _374570) ^ [] : [-(isFinite0(slcrc0))], (303 ^ _374570) ^ [_384524] : [aSet0(_384524), isCountable0(_384524), true___, -(true___)], (317 ^ _374570) ^ [_384865] : [isFinite0(_384865), aSet0(_384865), isCountable0(_384865)], (327 ^ _374570) ^ [_385135] : [_385135 = slcrc0, aSet0(_385135), isCountable0(_385135)], (337 ^ _374570) ^ [_385407] : [aSet0(_385407), 340 ^ _374570 : [(341 ^ _374570) ^ [_385583] : [aSubsetOf0(_385583, _385407), 344 ^ _374570 : [(345 ^ _374570) ^ [] : [-(aSet0(_385583))], (347 ^ _374570) ^ [_385792] : [aElementOf0(_385792, _385583), -(aElementOf0(_385792, _385407))]]], (353 ^ _374570) ^ [_385971] : [-(aSubsetOf0(_385971, _385407)), aSet0(_385971), 359 ^ _374570 : [(360 ^ _374570) ^ [] : [-(aElementOf0(358 ^ [_385407, _385971], _385971))], (362 ^ _374570) ^ [] : [aElementOf0(358 ^ [_385407, _385971], _385407)]]]]], (366 ^ _374570) ^ [_386408] : [aSet0(_386408), isFinite0(_386408), 373 ^ _374570 : [(374 ^ _374570) ^ [_386621] : [aSubsetOf0(_386621, _386408), -(isFinite0(_386621))]]], (380 ^ _374570) ^ [_386824] : [aSet0(_386824), -(aSubsetOf0(_386824, _386824))], (386 ^ _374570) ^ [_387026, _387028] : [aSet0(_387028), aSet0(_387026), -(_387028 = _387026), aSubsetOf0(_387028, _387026), aSubsetOf0(_387026, _387028)], (404 ^ _374570) ^ [_387515, _387517, _387519] : [aSet0(_387519), aSet0(_387517), aSet0(_387515), -(aSubsetOf0(_387519, _387515)), aSubsetOf0(_387519, _387517), aSubsetOf0(_387517, _387515)], (426 ^ _374570) ^ [_388101, _388103] : [aSet0(_388103), aElement0(_388101), 433 ^ _374570 : [(464 ^ _374570) ^ [_389362] : [-(_389362 = sdtpldt0(_388103, _388101)), aSet0(_389362), 472 ^ _374570 : [(473 ^ _374570) ^ [] : [-(aElementOf0(469 ^ [_388101, _388103, _389362], _389362))], (475 ^ _374570) ^ [] : [aElement0(469 ^ [_388101, _388103, _389362]), 478 ^ _374570 : [(479 ^ _374570) ^ [] : [aElementOf0(469 ^ [_388101, _388103, _389362], _388103)], (481 ^ _374570) ^ [] : [469 ^ [_388101, _388103, _389362] = _388101]]]], 482 ^ _374570 : [(491 ^ _374570) ^ [] : [aElementOf0(469 ^ [_388101, _388103, _389362], _389362)], (483 ^ _374570) ^ [] : [-(aElement0(469 ^ [_388101, _388103, _389362]))], (485 ^ _374570) ^ [] : [-(aElementOf0(469 ^ [_388101, _388103, _389362], _388103)), -(469 ^ [_388101, _388103, _389362] = _388101)]]], (434 ^ _374570) ^ [_388382] : [_388382 = sdtpldt0(_388103, _388101), 437 ^ _374570 : [(438 ^ _374570) ^ [] : [-(aSet0(_388382))], (440 ^ _374570) ^ [_388645] : [aElementOf0(_388645, _388382), 443 ^ _374570 : [(444 ^ _374570) ^ [] : [-(aElement0(_388645))], (446 ^ _374570) ^ [] : [-(aElementOf0(_388645, _388103)), -(_388645 = _388101)]]], (452 ^ _374570) ^ [_389000] : [-(aElementOf0(_389000, _388382)), aElement0(_389000), 457 ^ _374570 : [(458 ^ _374570) ^ [] : [aElementOf0(_389000, _388103)], (460 ^ _374570) ^ [] : [_389000 = _388101]]]]]]], (495 ^ _374570) ^ [_390399, _390401] : [aSet0(_390401), aElement0(_390399), 502 ^ _374570 : [(533 ^ _374570) ^ [_391667] : [-(_391667 = sdtmndt0(_390401, _390399)), aSet0(_391667), 553 ^ _374570 : [(554 ^ _374570) ^ [] : [-(aElement0(538 ^ [_390399, _390401, _391667]))], (556 ^ _374570) ^ [] : [-(aElementOf0(538 ^ [_390399, _390401, _391667], _390401))], (558 ^ _374570) ^ [] : [538 ^ [_390399, _390401, _391667] = _390399], (560 ^ _374570) ^ [] : [aElementOf0(538 ^ [_390399, _390401, _391667], _391667)]], 541 ^ _374570 : [(542 ^ _374570) ^ [] : [-(aElementOf0(538 ^ [_390399, _390401, _391667], _391667))], (544 ^ _374570) ^ [] : [aElement0(538 ^ [_390399, _390401, _391667]), aElementOf0(538 ^ [_390399, _390401, _391667], _390401), -(538 ^ [_390399, _390401, _391667] = _390399)]]], (503 ^ _374570) ^ [_390682] : [_390682 = sdtmndt0(_390401, _390399), 506 ^ _374570 : [(507 ^ _374570) ^ [] : [-(aSet0(_390682))], (509 ^ _374570) ^ [_390947] : [aElementOf0(_390947, _390682), 512 ^ _374570 : [(513 ^ _374570) ^ [] : [-(aElement0(_390947))], (515 ^ _374570) ^ [] : [-(aElementOf0(_390947, _390401))], (517 ^ _374570) ^ [] : [_390947 = _390399]]], (519 ^ _374570) ^ [_391283] : [-(aElementOf0(_391283, _390682)), aElement0(_391283), aElementOf0(_391283, _390401), -(_391283 = _390399)]]]]], (564 ^ _374570) ^ [_392697] : [aSet0(_392697), 567 ^ _374570 : [(568 ^ _374570) ^ [_392834] : [aElementOf0(_392834, _392697), -(sdtpldt0(sdtmndt0(_392697, _392834), _392834) = _392697)]]], (574 ^ _374570) ^ [_393063, _393065] : [aElement0(_393065), aSet0(_393063), -(aElementOf0(_393065, _393063)), -(sdtmndt0(sdtpldt0(_393063, _393065), _393065) = _393063)], (588 ^ _374570) ^ [_393450] : [aElement0(_393450), 591 ^ _374570 : [(592 ^ _374570) ^ [_393587] : [-(isCountable0(sdtpldt0(_393587, _393450))), aSet0(_393587), isCountable0(_393587)]]], (602 ^ _374570) ^ [_393879] : [aElement0(_393879), 605 ^ _374570 : [(606 ^ _374570) ^ [_394016] : [-(isCountable0(sdtmndt0(_394016, _393879))), aSet0(_394016), isCountable0(_394016)]]], (616 ^ _374570) ^ [_394308] : [aElement0(_394308), 619 ^ _374570 : [(620 ^ _374570) ^ [_394445] : [-(isFinite0(sdtpldt0(_394445, _394308))), aSet0(_394445), isFinite0(_394445)]]], (630 ^ _374570) ^ [_394737] : [aElement0(_394737), 633 ^ _374570 : [(634 ^ _374570) ^ [_394874] : [-(isFinite0(sdtmndt0(_394874, _394737))), aSet0(_394874), isFinite0(_394874)]]], (644 ^ _374570) ^ [] : [-(aSet0(szNzAzT0))], (646 ^ _374570) ^ [] : [-(isCountable0(szNzAzT0))], (648 ^ _374570) ^ [] : [-(aElementOf0(sz00, szNzAzT0))], (650 ^ _374570) ^ [_395327] : [aElementOf0(_395327, szNzAzT0), 653 ^ _374570 : [(654 ^ _374570) ^ [] : [-(aElementOf0(szszuzczcdt0(_395327), szNzAzT0))], (656 ^ _374570) ^ [] : [szszuzczcdt0(_395327) = sz00]]], (658 ^ _374570) ^ [_395613, _395615] : [aElementOf0(_395615, szNzAzT0), aElementOf0(_395613, szNzAzT0), szszuzczcdt0(_395615) = szszuzczcdt0(_395613), -(_395615 = _395613)], (672 ^ _374570) ^ [_395997] : [aElementOf0(_395997, szNzAzT0), -(_395997 = sz00), 680 ^ _374570 : [(681 ^ _374570) ^ [] : [-(aElementOf0(679 ^ [_395997], szNzAzT0))], (683 ^ _374570) ^ [] : [-(_395997 = szszuzczcdt0(679 ^ [_395997]))]]], (685 ^ _374570) ^ [_396414] : [aElementOf0(_396414, szNzAzT0), _396414 = szszuzczcdt0(_396414)], (691 ^ _374570) ^ [_396623, _396625] : [aElementOf0(_396625, szNzAzT0), aElementOf0(_396623, szNzAzT0), sdtlseqdt0(_396625, _396623), true___, -(true___)], (709 ^ _374570) ^ [_397073] : [aElementOf0(_397073, szNzAzT0), -(sdtlseqdt0(sz00, _397073))], (715 ^ _374570) ^ [_397263] : [aElementOf0(_397263, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_397263), sz00)], (721 ^ _374570) ^ [_397472, _397474] : [aElementOf0(_397474, szNzAzT0), aElementOf0(_397472, szNzAzT0), 728 ^ _374570 : [(729 ^ _374570) ^ [] : [sdtlseqdt0(_397474, _397472), -(sdtlseqdt0(szszuzczcdt0(_397474), szszuzczcdt0(_397472)))], (735 ^ _374570) ^ [] : [sdtlseqdt0(szszuzczcdt0(_397474), szszuzczcdt0(_397472)), -(sdtlseqdt0(_397474, _397472))]]], (741 ^ _374570) ^ [_398021] : [aElementOf0(_398021, szNzAzT0), -(sdtlseqdt0(_398021, szszuzczcdt0(_398021)))], (747 ^ _374570) ^ [_398215] : [aElementOf0(_398215, szNzAzT0), -(sdtlseqdt0(_398215, _398215))], (753 ^ _374570) ^ [_398419, _398421] : [aElementOf0(_398421, szNzAzT0), aElementOf0(_398419, szNzAzT0), -(_398421 = _398419), sdtlseqdt0(_398421, _398419), sdtlseqdt0(_398419, _398421)], (771 ^ _374570) ^ [_398912, _398914, _398916] : [aElementOf0(_398916, szNzAzT0), aElementOf0(_398914, szNzAzT0), aElementOf0(_398912, szNzAzT0), -(sdtlseqdt0(_398916, _398912)), sdtlseqdt0(_398916, _398914), sdtlseqdt0(_398914, _398912)], (793 ^ _374570) ^ [_399504, _399506] : [aElementOf0(_399506, szNzAzT0), aElementOf0(_399504, szNzAzT0), -(sdtlseqdt0(_399506, _399504)), -(sdtlseqdt0(szszuzczcdt0(_399504), _399506))], (807 ^ _374570) ^ [_399899, _399901] : [aElementOf0(_399901, szNzAzT0), aElementOf0(_399899, szNzAzT0), iLess0(_399901, _399899), true___, -(true___)], (825 ^ _374570) ^ [_400349] : [aElementOf0(_400349, szNzAzT0), -(iLess0(_400349, szszuzczcdt0(_400349)))], (831 ^ _374570) ^ [_400543] : [aSet0(_400543), -(aElement0(sbrdtbr0(_400543)))], (837 ^ _374570) ^ [_400733] : [aSet0(_400733), 840 ^ _374570 : [(841 ^ _374570) ^ [] : [aElementOf0(sbrdtbr0(_400733), szNzAzT0), -(isFinite0(_400733))], (847 ^ _374570) ^ [] : [isFinite0(_400733), -(aElementOf0(sbrdtbr0(_400733), szNzAzT0))]]], (853 ^ _374570) ^ [_401164] : [aSet0(_401164), 856 ^ _374570 : [(857 ^ _374570) ^ [] : [sbrdtbr0(_401164) = sz00, -(_401164 = slcrc0)], (863 ^ _374570) ^ [] : [_401164 = slcrc0, -(sbrdtbr0(_401164) = sz00)]]], (869 ^ _374570) ^ [_401598] : [aSet0(_401598), isFinite0(_401598), 876 ^ _374570 : [(877 ^ _374570) ^ [_401828] : [aElement0(_401828), -(aElementOf0(_401828, _401598)), -(sbrdtbr0(sdtpldt0(_401598, _401828)) = szszuzczcdt0(sbrdtbr0(_401598)))]]], (887 ^ _374570) ^ [_402141] : [aSet0(_402141), 890 ^ _374570 : [(891 ^ _374570) ^ [_402286] : [-(szszuzczcdt0(sbrdtbr0(sdtmndt0(_402141, _402286))) = sbrdtbr0(_402141)), isFinite0(_402141), aElementOf0(_402286, _402141)]]], (901 ^ _374570) ^ [_402594] : [aSet0(_402594), 904 ^ _374570 : [(905 ^ _374570) ^ [_402734] : [-(sdtlseqdt0(sbrdtbr0(_402734), sbrdtbr0(_402594))), isFinite0(_402594), aSubsetOf0(_402734, _402594)]]], (915 ^ _374570) ^ [_403046, _403048] : [aSet0(_403048), aElementOf0(_403046, szNzAzT0), 931 ^ _374570 : [(932 ^ _374570) ^ [] : [-(aSubsetOf0(930 ^ [_403046, _403048], _403048))], (934 ^ _374570) ^ [] : [-(sbrdtbr0(930 ^ [_403046, _403048]) = _403046)]], isFinite0(_403048), sdtlseqdt0(_403046, sbrdtbr0(_403048))], (936 ^ _374570) ^ [_403662] : [aSubsetOf0(_403662, szNzAzT0), -(_403662 = slcrc0), 943 ^ _374570 : [(944 ^ _374570) ^ [_403931] : [_403931 = szmzizndt0(_403662), 947 ^ _374570 : [(948 ^ _374570) ^ [] : [-(aElementOf0(_403931, _403662))], (950 ^ _374570) ^ [_404146] : [aElementOf0(_404146, _403662), -(sdtlseqdt0(_403931, _404146))]]], (956 ^ _374570) ^ [_404325] : [-(_404325 = szmzizndt0(_403662)), aElementOf0(_404325, _403662), 962 ^ _374570 : [(963 ^ _374570) ^ [] : [-(aElementOf0(961 ^ [_403662, _404325], _403662))], (965 ^ _374570) ^ [] : [sdtlseqdt0(_404325, 961 ^ [_403662, _404325])]]]]], (969 ^ _374570) ^ [_404770] : [aSubsetOf0(_404770, szNzAzT0), isFinite0(_404770), -(_404770 = slcrc0), 980 ^ _374570 : [(981 ^ _374570) ^ [_405122] : [_405122 = szmzazxdt0(_404770), 984 ^ _374570 : [(985 ^ _374570) ^ [] : [-(aElementOf0(_405122, _404770))], (987 ^ _374570) ^ [_405337] : [aElementOf0(_405337, _404770), -(sdtlseqdt0(_405337, _405122))]]], (993 ^ _374570) ^ [_405516] : [-(_405516 = szmzazxdt0(_404770)), aElementOf0(_405516, _404770), 999 ^ _374570 : [(1000 ^ _374570) ^ [] : [-(aElementOf0(998 ^ [_404770, _405516], _404770))], (1002 ^ _374570) ^ [] : [sdtlseqdt0(998 ^ [_404770, _405516], _405516)]]]]], (1006 ^ _374570) ^ [_405977, _405979] : [-(szmzizndt0(_405979) = szmzizndt0(_405977)), aElementOf0(szmzizndt0(_405979), _405977), aElementOf0(szmzizndt0(_405977), _405979), aSubsetOf0(_405979, szNzAzT0), aSubsetOf0(_405977, szNzAzT0), -(_405979 = slcrc0), -(_405977 = slcrc0)], (1032 ^ _374570) ^ [_406644] : [aElementOf0(_406644, szNzAzT0), 1035 ^ _374570 : [(1060 ^ _374570) ^ [_407613] : [-(_407613 = slbdtrb0(_406644)), aSet0(_407613), 1076 ^ _374570 : [(1077 ^ _374570) ^ [] : [-(aElementOf0(1065 ^ [_406644, _407613], szNzAzT0))], (1079 ^ _374570) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(1065 ^ [_406644, _407613]), _406644))], (1081 ^ _374570) ^ [] : [aElementOf0(1065 ^ [_406644, _407613], _407613)]], 1068 ^ _374570 : [(1069 ^ _374570) ^ [] : [-(aElementOf0(1065 ^ [_406644, _407613], _407613))], (1071 ^ _374570) ^ [] : [aElementOf0(1065 ^ [_406644, _407613], szNzAzT0), sdtlseqdt0(szszuzczcdt0(1065 ^ [_406644, _407613]), _406644)]]], (1036 ^ _374570) ^ [_406832] : [_406832 = slbdtrb0(_406644), 1039 ^ _374570 : [(1040 ^ _374570) ^ [] : [-(aSet0(_406832))], (1042 ^ _374570) ^ [_407082] : [aElementOf0(_407082, _406832), 1045 ^ _374570 : [(1046 ^ _374570) ^ [] : [-(aElementOf0(_407082, szNzAzT0))], (1048 ^ _374570) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(_407082), _406644))]]], (1050 ^ _374570) ^ [_407335] : [-(aElementOf0(_407335, _406832)), aElementOf0(_407335, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_407335), _406644)]]]]], (1085 ^ _374570) ^ [_408416] : [aElementOf0(_408416, szNzAzT0), -(isFinite0(slbdtrb0(_408416)))], (1091 ^ _374570) ^ [] : [-(slbdtrb0(sz00) = slcrc0)], (1093 ^ _374570) ^ [_408675, _408677] : [aElementOf0(_408677, szNzAzT0), aElementOf0(_408675, szNzAzT0), 1100 ^ _374570 : [(1111 ^ _374570) ^ [] : [1112 ^ _374570 : [(1113 ^ _374570) ^ [] : [aElementOf0(_408677, slbdtrb0(_408675))], (1115 ^ _374570) ^ [] : [_408677 = _408675]], -(aElementOf0(_408677, slbdtrb0(szszuzczcdt0(_408675))))], (1101 ^ _374570) ^ [] : [aElementOf0(_408677, slbdtrb0(szszuzczcdt0(_408675))), -(aElementOf0(_408677, slbdtrb0(_408675))), -(_408677 = _408675)]]], (1119 ^ _374570) ^ [_409402, _409404] : [aElementOf0(_409404, szNzAzT0), aElementOf0(_409402, szNzAzT0), 1126 ^ _374570 : [(1127 ^ _374570) ^ [] : [sdtlseqdt0(_409404, _409402), -(aSubsetOf0(slbdtrb0(_409404), slbdtrb0(_409402)))], (1133 ^ _374570) ^ [] : [aSubsetOf0(slbdtrb0(_409404), slbdtrb0(_409402)), -(sdtlseqdt0(_409404, _409402))]]], (1139 ^ _374570) ^ [_409951] : [1147 ^ _374570 : [(1148 ^ _374570) ^ [] : [-(aElementOf0(1146 ^ [_409951], szNzAzT0))], (1150 ^ _374570) ^ [] : [-(aSubsetOf0(_409951, slbdtrb0(1146 ^ [_409951])))]], aSubsetOf0(_409951, szNzAzT0), isFinite0(_409951)], (1152 ^ _374570) ^ [_410365] : [aElementOf0(_410365, szNzAzT0), -(sbrdtbr0(slbdtrb0(_410365)) = _410365)], (1158 ^ _374570) ^ [_410577, _410579] : [aSet0(_410579), aElementOf0(_410577, szNzAzT0), 1165 ^ _374570 : [(1190 ^ _374570) ^ [_411670] : [-(_411670 = slbdtsldtrb0(_410579, _410577)), aSet0(_411670), 1206 ^ _374570 : [(1207 ^ _374570) ^ [] : [-(aSubsetOf0(1195 ^ [_410577, _410579, _411670], _410579))], (1209 ^ _374570) ^ [] : [-(sbrdtbr0(1195 ^ [_410577, _410579, _411670]) = _410577)], (1211 ^ _374570) ^ [] : [aElementOf0(1195 ^ [_410577, _410579, _411670], _411670)]], 1198 ^ _374570 : [(1199 ^ _374570) ^ [] : [-(aElementOf0(1195 ^ [_410577, _410579, _411670], _411670))], (1201 ^ _374570) ^ [] : [aSubsetOf0(1195 ^ [_410577, _410579, _411670], _410579), sbrdtbr0(1195 ^ [_410577, _410579, _411670]) = _410577]]], (1166 ^ _374570) ^ [_410857] : [_410857 = slbdtsldtrb0(_410579, _410577), 1169 ^ _374570 : [(1170 ^ _374570) ^ [] : [-(aSet0(_410857))], (1172 ^ _374570) ^ [_411117] : [aElementOf0(_411117, _410857), 1175 ^ _374570 : [(1176 ^ _374570) ^ [] : [-(aSubsetOf0(_411117, _410579))], (1178 ^ _374570) ^ [] : [-(sbrdtbr0(_411117) = _410577)]]], (1180 ^ _374570) ^ [_411380] : [-(aElementOf0(_411380, _410857)), aSubsetOf0(_411380, _410579), sbrdtbr0(_411380) = _410577]]]]], (1215 ^ _374570) ^ [_412519] : [aSet0(_412519), isFinite0(_412519), 1222 ^ _374570 : [(1223 ^ _374570) ^ [_412735] : [aElementOf0(_412735, szNzAzT0), -(isFinite0(slbdtsldtrb0(_412519, _412735)))]]], (1229 ^ _374570) ^ [_412944] : [aSet0(_412944), -(isFinite0(_412944)), 1236 ^ _374570 : [(1237 ^ _374570) ^ [_413166] : [aElementOf0(_413166, szNzAzT0), slbdtsldtrb0(_412944, _413166) = slcrc0]]], (1243 ^ _374570) ^ [_413378] : [aSet0(_413378), isCountable0(_413378), 1250 ^ _374570 : [(1251 ^ _374570) ^ [_413602] : [-(isCountable0(slbdtsldtrb0(_413378, _413602))), aElementOf0(_413602, szNzAzT0), -(_413602 = sz00)]]], (1261 ^ _374570) ^ [_413903] : [aElementOf0(_413903, szNzAzT0), 1264 ^ _374570 : [(1265 ^ _374570) ^ [_414090, _414092] : [aSet0(_414092), aSet0(_414090), -(_413903 = sz00), -(aSubsetOf0(_414092, _414090)), aSubsetOf0(slbdtsldtrb0(_414092, _413903), slbdtsldtrb0(_414090, _413903)), -(slbdtsldtrb0(_414092, _413903) = slcrc0)]]], (1287 ^ _374570) ^ [_414709, _414711] : [aSet0(_414711), aElementOf0(_414709, szNzAzT0), 1294 ^ _374570 : [(1295 ^ _374570) ^ [_414960] : [1303 ^ _374570 : [(1304 ^ _374570) ^ [] : [-(aSubsetOf0(1302 ^ [_414709, _414711, _414960], _414711))], (1306 ^ _374570) ^ [] : [-(isFinite0(1302 ^ [_414709, _414711, _414960]))], (1308 ^ _374570) ^ [] : [-(aSubsetOf0(_414960, slbdtsldtrb0(1302 ^ [_414709, _414711, _414960], _414709)))]], aSubsetOf0(_414960, slbdtsldtrb0(_414711, _414709)), isFinite0(_414960)]]], (1310 ^ _374570) ^ [_415522] : [aFunction0(_415522), true___, -(true___)], (1320 ^ _374570) ^ [_415777] : [aFunction0(_415777), -(aSet0(szDzozmdt0(_415777)))], (1326 ^ _374570) ^ [_415967] : [aFunction0(_415967), 1329 ^ _374570 : [(1330 ^ _374570) ^ [_416102] : [aElementOf0(_416102, szDzozmdt0(_415967)), -(aElement0(sdtlpdtrp0(_415967, _416102)))]]], (1336 ^ _374570) ^ [_416327, _416329] : [aFunction0(_416329), aElement0(_416327), 1343 ^ _374570 : [(1368 ^ _374570) ^ [_417436] : [-(_417436 = sdtlbdtrb0(_416329, _416327)), aSet0(_417436), 1384 ^ _374570 : [(1385 ^ _374570) ^ [] : [-(aElementOf0(1373 ^ [_416327, _416329, _417436], szDzozmdt0(_416329)))], (1387 ^ _374570) ^ [] : [-(sdtlpdtrp0(_416329, 1373 ^ [_416327, _416329, _417436]) = _416327)], (1389 ^ _374570) ^ [] : [aElementOf0(1373 ^ [_416327, _416329, _417436], _417436)]], 1376 ^ _374570 : [(1377 ^ _374570) ^ [] : [-(aElementOf0(1373 ^ [_416327, _416329, _417436], _417436))], (1379 ^ _374570) ^ [] : [aElementOf0(1373 ^ [_416327, _416329, _417436], szDzozmdt0(_416329)), sdtlpdtrp0(_416329, 1373 ^ [_416327, _416329, _417436]) = _416327]]], (1344 ^ _374570) ^ [_416608] : [_416608 = sdtlbdtrb0(_416329, _416327), 1347 ^ _374570 : [(1348 ^ _374570) ^ [] : [-(aSet0(_416608))], (1350 ^ _374570) ^ [_416871] : [aElementOf0(_416871, _416608), 1353 ^ _374570 : [(1354 ^ _374570) ^ [] : [-(aElementOf0(_416871, szDzozmdt0(_416329)))], (1356 ^ _374570) ^ [] : [-(sdtlpdtrp0(_416329, _416871) = _416327)]]], (1358 ^ _374570) ^ [_417140] : [-(aElementOf0(_417140, _416608)), aElementOf0(_417140, szDzozmdt0(_416329)), sdtlpdtrp0(_416329, _417140) = _416327]]]]], (1393 ^ _374570) ^ [_418311, _418313] : [-(aSubsetOf0(sdtlbdtrb0(_418313, _418311), szDzozmdt0(_418313))), aFunction0(_418313), aElement0(_418311)], (1403 ^ _374570) ^ [_418602] : [aFunction0(_418602), 1406 ^ _374570 : [(1407 ^ _374570) ^ [_418779] : [aSubsetOf0(_418779, szDzozmdt0(_418602)), 1410 ^ _374570 : [(1436 ^ _374570) ^ [_419966] : [-(_419966 = sdtlcdtrc0(_418602, _418779)), aSet0(_419966), 1453 ^ _374570 : [(1454 ^ _374570) ^ [] : [-(aElementOf0(1452 ^ [_418602, _418779, _419966], _418779))], (1456 ^ _374570) ^ [] : [-(sdtlpdtrp0(_418602, 1452 ^ [_418602, _418779, _419966]) = 1441 ^ [_418602, _418779, _419966])], (1458 ^ _374570) ^ [] : [aElementOf0(1441 ^ [_418602, _418779, _419966], _419966)]], 1444 ^ _374570 : [(1445 ^ _374570) ^ [] : [-(aElementOf0(1441 ^ [_418602, _418779, _419966], _419966))], (1447 ^ _374570) ^ [_420359] : [aElementOf0(_420359, _418779), sdtlpdtrp0(_418602, _420359) = 1441 ^ [_418602, _418779, _419966]]]], (1411 ^ _374570) ^ [_418984] : [_418984 = sdtlcdtrc0(_418602, _418779), 1414 ^ _374570 : [(1415 ^ _374570) ^ [] : [-(aSet0(_418984))], (1417 ^ _374570) ^ [_419250] : [aElementOf0(_419250, _418984), 1421 ^ _374570 : [(1422 ^ _374570) ^ [] : [-(aElementOf0(1420 ^ [_418602, _418779, _418984, _419250], _418779))], (1424 ^ _374570) ^ [] : [-(sdtlpdtrp0(_418602, 1420 ^ [_418602, _418779, _418984, _419250]) = _419250)]]], (1426 ^ _374570) ^ [_419604] : [-(aElementOf0(_419604, _418984)), 1427 ^ _374570 : [(1428 ^ _374570) ^ [_419709] : [aElementOf0(_419709, _418779), sdtlpdtrp0(_418602, _419709) = _419604]]]]]]]]], (1462 ^ _374570) ^ [_420970] : [aFunction0(_420970), 1465 ^ _374570 : [(1466 ^ _374570) ^ [_421111] : [aElementOf0(_421111, szDzozmdt0(_420970)), -(aElementOf0(sdtlpdtrp0(_420970, _421111), sdtlcdtrc0(_420970, szDzozmdt0(_420970))))]]], (1472 ^ _374570) ^ [_421334] : [aFunction0(_421334), 1475 ^ _374570 : [(1476 ^ _374570) ^ [_421511] : [aSubsetOf0(_421511, szDzozmdt0(_421334)), 1479 ^ _374570 : [(1480 ^ _374570) ^ [_421716] : [_421716 = sdtexdt0(_421334, _421511), 1483 ^ _374570 : [(1484 ^ _374570) ^ [] : [-(aFunction0(_421716))], (1486 ^ _374570) ^ [] : [-(szDzozmdt0(_421716) = _421511)], (1488 ^ _374570) ^ [_422023] : [aElementOf0(_422023, _421511), -(sdtlpdtrp0(_421716, _422023) = sdtlpdtrp0(_421334, _422023))]]], (1494 ^ _374570) ^ [_422224] : [-(_422224 = sdtexdt0(_421334, _421511)), aFunction0(_422224), szDzozmdt0(_422224) = _421511, 1504 ^ _374570 : [(1505 ^ _374570) ^ [] : [-(aElementOf0(1503 ^ [_421334, _421511, _422224], _421511))], (1507 ^ _374570) ^ [] : [sdtlpdtrp0(_422224, 1503 ^ [_421334, _421511, _422224]) = sdtlpdtrp0(_421334, 1503 ^ [_421334, _421511, _422224])]]]]]]], (1511 ^ _374570) ^ [_422818] : [aFunction0(_422818), 1514 ^ _374570 : [(1515 ^ _374570) ^ [_423006] : [aSubsetOf0(_423006, szDzozmdt0(_422818)), isCountable0(_423006), 1526 ^ _374570 : [(1527 ^ _374570) ^ [] : [-(aElementOf0(1524 ^ [_422818, _423006], szDzozmdt0(_422818)))], (1529 ^ _374570) ^ [] : [-(aElementOf0(1525 ^ [_422818, _423006], szDzozmdt0(_422818)))], (1531 ^ _374570) ^ [] : [1524 ^ [_422818, _423006] = 1525 ^ [_422818, _423006]], (1533 ^ _374570) ^ [] : [-(sdtlpdtrp0(_422818, 1524 ^ [_422818, _423006]) = sdtlpdtrp0(_422818, 1525 ^ [_422818, _423006]))]], -(isCountable0(sdtlcdtrc0(_422818, _423006)))]]], (1537 ^ _374570) ^ [_423878] : [aFunction0(_423878), 1548 ^ _374570 : [(1549 ^ _374570) ^ [] : [-(aElement0(szDzizrdt0(_423878)))], (1551 ^ _374570) ^ [] : [-(isCountable0(sdtlbdtrb0(_423878, szDzizrdt0(_423878))))]], isCountable0(szDzozmdt0(_423878)), isFinite0(sdtlcdtrc0(_423878, szDzozmdt0(_423878)))], (1553 ^ _374570) ^ [] : [-(aSet0(xT))], (1555 ^ _374570) ^ [] : [-(isFinite0(xT))], (1557 ^ _374570) ^ [] : [-(aElementOf0(xK, szNzAzT0))], (1559 ^ _374570) ^ [] : [-(aSet0(xS))], (1567 ^ _374570) ^ [] : [-(aSubsetOf0(xS, szNzAzT0))], (1569 ^ _374570) ^ [] : [-(isCountable0(xS))], (1561 ^ _374570) ^ [_424563] : [aElementOf0(_424563, xS), -(aElementOf0(_424563, szNzAzT0))], (1571 ^ _374570) ^ [] : [-(aFunction0(xc))], (1573 ^ _374570) ^ [_424940] : [aElementOf0(_424940, szDzozmdt0(xc)), 1576 ^ _374570 : [(1577 ^ _374570) ^ [] : [-(aSet0(_424940))], (1585 ^ _374570) ^ [] : [-(aSubsetOf0(_424940, xS))], (1587 ^ _374570) ^ [] : [-(sbrdtbr0(_424940) = xK)], (1579 ^ _374570) ^ [_425175] : [aElementOf0(_425175, _424940), -(aElementOf0(_425175, xS))]]], (1589 ^ _374570) ^ [_425462] : [-(aElementOf0(_425462, szDzozmdt0(xc))), sbrdtbr0(_425462) = xK, 1592 ^ _374570 : [(1602 ^ _374570) ^ [] : [aSubsetOf0(_425462, xS)], (1593 ^ _374570) ^ [] : [aSet0(_425462), 1597 ^ _374570 : [(1598 ^ _374570) ^ [] : [-(aElementOf0(1596 ^ [_425462], _425462))], (1600 ^ _374570) ^ [] : [aElementOf0(1596 ^ [_425462], xS)]]]]], (1608 ^ _374570) ^ [] : [-(szDzozmdt0(xc) = slbdtsldtrb0(xS, xK))], (1610 ^ _374570) ^ [] : [-(aSet0(sdtlcdtrc0(xc, szDzozmdt0(xc))))], (1637 ^ _374570) ^ [] : [-(aSubsetOf0(sdtlcdtrc0(xc, szDzozmdt0(xc)), xT))], (1631 ^ _374570) ^ [_426815] : [aElementOf0(_426815, sdtlcdtrc0(xc, szDzozmdt0(xc))), -(aElementOf0(_426815, xT))], (1612 ^ _374570) ^ [_426168] : [aElementOf0(_426168, sdtlcdtrc0(xc, szDzozmdt0(xc))), 1616 ^ _374570 : [(1617 ^ _374570) ^ [] : [-(aElementOf0(1615 ^ [_426168], szDzozmdt0(xc)))], (1619 ^ _374570) ^ [] : [-(sdtlpdtrp0(xc, 1615 ^ [_426168]) = _426168)]]], (1621 ^ _374570) ^ [_426468] : [-(aElementOf0(_426468, sdtlcdtrc0(xc, szDzozmdt0(xc)))), 1622 ^ _374570 : [(1623 ^ _374570) ^ [_426561] : [aElementOf0(_426561, szDzozmdt0(xc)), sdtlpdtrp0(xc, _426561) = _426468]]], (1639 ^ _374570) ^ [_427054] : [aElementOf0(_427054, szNzAzT0), 1642 ^ _374570 : [(1643 ^ _374570) ^ [_427517] : [isCountable0(_427517), 1646 ^ _374570 : [(1656 ^ _374570) ^ [] : [aSubsetOf0(_427517, szNzAzT0)], (1647 ^ _374570) ^ [] : [aSet0(_427517), 1651 ^ _374570 : [(1652 ^ _374570) ^ [] : [-(aElementOf0(1650 ^ [_427054, _427517], _427517))], (1654 ^ _374570) ^ [] : [aElementOf0(1650 ^ [_427054, _427517], szNzAzT0)]]]], 1659 ^ _374570 : [(1660 ^ _374570) ^ [_428341] : [iLess0(_427054, xK), 1736 ^ _374570 : [(1737 ^ _374570) ^ [] : [-(aElementOf0(1735 ^ [_427054, _427517, _428341], xT))], (1740 ^ _374570) ^ [] : [-(aSet0(1738 ^ [_427054, _427517, _428341]))], (1742 ^ _374570) ^ [_431895] : [aElementOf0(_431895, 1738 ^ [_427054, _427517, _428341]), -(aElementOf0(_431895, _427517))], (1748 ^ _374570) ^ [] : [-(aSubsetOf0(1738 ^ [_427054, _427517, _428341], _427517))], (1750 ^ _374570) ^ [] : [-(isCountable0(1738 ^ [_427054, _427517, _428341]))], (1752 ^ _374570) ^ [_432260] : [-(sdtlpdtrp0(_428341, _432260) = 1735 ^ [_427054, _427517, _428341]), 1753 ^ _374570 : [(1769 ^ _374570) ^ [] : [aElementOf0(_432260, slbdtsldtrb0(1738 ^ [_427054, _427517, _428341], _427054))], (1754 ^ _374570) ^ [] : [sbrdtbr0(_432260) = _427054, 1755 ^ _374570 : [(1765 ^ _374570) ^ [] : [aSubsetOf0(_432260, 1738 ^ [_427054, _427517, _428341])], (1756 ^ _374570) ^ [] : [aSet0(_432260), 1760 ^ _374570 : [(1761 ^ _374570) ^ [] : [-(aElementOf0(1759 ^ [_427054, _427517, _428341, _432260], _432260))], (1763 ^ _374570) ^ [] : [aElementOf0(1759 ^ [_427054, _427517, _428341, _432260], 1738 ^ [_427054, _427517, _428341])]]]]]]]], aFunction0(_428341), 1668 ^ _374570 : [(1702 ^ _374570) ^ [] : [szDzozmdt0(_428341) = slbdtsldtrb0(_427517, _427054)], (1669 ^ _374570) ^ [] : [1687 ^ _374570 : [(1700 ^ _374570) ^ [] : [aElementOf0(1667 ^ [_427054, _427517, _428341], szDzozmdt0(_428341))], (1688 ^ _374570) ^ [] : [-(aSet0(1667 ^ [_427054, _427517, _428341]))], (1696 ^ _374570) ^ [] : [-(aSubsetOf0(1667 ^ [_427054, _427517, _428341], _427517))], (1698 ^ _374570) ^ [] : [-(sbrdtbr0(1667 ^ [_427054, _427517, _428341]) = _427054)], (1690 ^ _374570) ^ [_429703] : [aElementOf0(_429703, 1667 ^ [_427054, _427517, _428341]), -(aElementOf0(_429703, _427517))]], 1670 ^ _374570 : [(1671 ^ _374570) ^ [] : [-(aElementOf0(1667 ^ [_427054, _427517, _428341], szDzozmdt0(_428341)))], (1673 ^ _374570) ^ [] : [sbrdtbr0(1667 ^ [_427054, _427517, _428341]) = _427054, 1674 ^ _374570 : [(1684 ^ _374570) ^ [] : [aSubsetOf0(1667 ^ [_427054, _427517, _428341], _427517)], (1675 ^ _374570) ^ [] : [aSet0(1667 ^ [_427054, _427517, _428341]), 1679 ^ _374570 : [(1680 ^ _374570) ^ [] : [-(aElementOf0(1678 ^ [_427054, _427517, _428341], 1667 ^ [_427054, _427517, _428341]))], (1682 ^ _374570) ^ [] : [aElementOf0(1678 ^ [_427054, _427517, _428341], _427517)]]]]]]]], 1703 ^ _374570 : [(1726 ^ _374570) ^ [] : [-(aElementOf0(1724 ^ [_427054, _427517, _428341], sdtlcdtrc0(_428341, szDzozmdt0(_428341))))], (1728 ^ _374570) ^ [] : [aElementOf0(1724 ^ [_427054, _427517, _428341], xT)], (1730 ^ _374570) ^ [] : [aSubsetOf0(sdtlcdtrc0(_428341, szDzozmdt0(_428341)), xT)], (1704 ^ _374570) ^ [] : [-(aSet0(sdtlcdtrc0(_428341, szDzozmdt0(_428341))))], (1706 ^ _374570) ^ [_430300] : [aElementOf0(_430300, sdtlcdtrc0(_428341, szDzozmdt0(_428341))), 1710 ^ _374570 : [(1711 ^ _374570) ^ [] : [-(aElementOf0(1709 ^ [_427054, _427517, _428341, _430300], szDzozmdt0(_428341)))], (1713 ^ _374570) ^ [] : [-(sdtlpdtrp0(_428341, 1709 ^ [_427054, _427517, _428341, _430300]) = _430300)]]], (1715 ^ _374570) ^ [_430670] : [-(aElementOf0(_430670, sdtlcdtrc0(_428341, szDzozmdt0(_428341)))), 1716 ^ _374570 : [(1717 ^ _374570) ^ [_430782] : [aElementOf0(_430782, szDzozmdt0(_428341)), sdtlpdtrp0(_428341, _430782) = _430670]]]]]]]]], (1773 ^ _374570) ^ [] : [xK = sz00], (1775 ^ _374570) ^ [] : [xK = sz00], (1777 ^ _374570) ^ [] : [-(aElementOf0(xk, szNzAzT0))], (1779 ^ _374570) ^ [] : [-(szszuzczcdt0(xk) = xK)], (1781 ^ _374570) ^ [] : [-(aFunction0(xN))], (1783 ^ _374570) ^ [] : [-(szDzozmdt0(xN) = szNzAzT0)], (1785 ^ _374570) ^ [] : [-(sdtlpdtrp0(xN, sz00) = xS)], (1787 ^ _374570) ^ [_433488] : [aElementOf0(_433488, szNzAzT0), isCountable0(sdtlpdtrp0(xN, _433488)), 1794 ^ _374570 : [(1804 ^ _374570) ^ [] : [aSubsetOf0(sdtlpdtrp0(xN, _433488), szNzAzT0)], (1795 ^ _374570) ^ [] : [aSet0(sdtlpdtrp0(xN, _433488)), 1799 ^ _374570 : [(1800 ^ _374570) ^ [] : [-(aElementOf0(1798 ^ [_433488], sdtlpdtrp0(xN, _433488)))], (1802 ^ _374570) ^ [] : [aElementOf0(1798 ^ [_433488], szNzAzT0)]]]], 1807 ^ _374570 : [(1808 ^ _374570) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _433488)), sdtlpdtrp0(xN, _433488)))], (1810 ^ _374570) ^ [_434356] : [aElementOf0(_434356, sdtlpdtrp0(xN, _433488)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _433488)), _434356))], (1816 ^ _374570) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _433488), szmzizndt0(sdtlpdtrp0(xN, _433488)))))], (1842 ^ _374570) ^ [] : [-(aSet0(sdtlpdtrp0(xN, szszuzczcdt0(_433488))))], (1850 ^ _374570) ^ [] : [-(aSubsetOf0(sdtlpdtrp0(xN, szszuzczcdt0(_433488)), sdtmndt0(sdtlpdtrp0(xN, _433488), szmzizndt0(sdtlpdtrp0(xN, _433488)))))], (1852 ^ _374570) ^ [] : [-(isCountable0(sdtlpdtrp0(xN, szszuzczcdt0(_433488))))], (1844 ^ _374570) ^ [_435508] : [aElementOf0(_435508, sdtlpdtrp0(xN, szszuzczcdt0(_433488))), -(aElementOf0(_435508, sdtmndt0(sdtlpdtrp0(xN, _433488), szmzizndt0(sdtlpdtrp0(xN, _433488)))))], (1818 ^ _374570) ^ [_434673] : [aElementOf0(_434673, sdtmndt0(sdtlpdtrp0(xN, _433488), szmzizndt0(sdtlpdtrp0(xN, _433488)))), 1821 ^ _374570 : [(1822 ^ _374570) ^ [] : [-(aElement0(_434673))], (1824 ^ _374570) ^ [] : [-(aElementOf0(_434673, sdtlpdtrp0(xN, _433488)))], (1826 ^ _374570) ^ [] : [_434673 = szmzizndt0(sdtlpdtrp0(xN, _433488))]]], (1828 ^ _374570) ^ [_435023] : [-(aElementOf0(_435023, sdtmndt0(sdtlpdtrp0(xN, _433488), szmzizndt0(sdtlpdtrp0(xN, _433488))))), aElement0(_435023), aElementOf0(_435023, sdtlpdtrp0(xN, _433488)), -(_435023 = szmzizndt0(sdtlpdtrp0(xN, _433488)))]]], (1854 ^ _374570) ^ [_435905] : [aElementOf0(_435905, szNzAzT0), 1857 ^ _374570 : [(1858 ^ _374570) ^ [] : [-(aSet0(sdtlpdtrp0(xN, _435905)))], (1866 ^ _374570) ^ [] : [-(aSubsetOf0(sdtlpdtrp0(xN, _435905), szNzAzT0))], (1868 ^ _374570) ^ [] : [-(isCountable0(sdtlpdtrp0(xN, _435905)))], (1860 ^ _374570) ^ [_436152] : [aElementOf0(_436152, sdtlpdtrp0(xN, _435905)), -(aElementOf0(_436152, szNzAzT0))]]], (1870 ^ _374570) ^ [_436496, _436498] : [aElementOf0(_436498, szNzAzT0), aElementOf0(_436496, szNzAzT0), sdtlseqdt0(_436496, _436498), 1881 ^ _374570 : [(1888 ^ _374570) ^ [] : [-(aSubsetOf0(sdtlpdtrp0(xN, _436498), sdtlpdtrp0(xN, _436496)))], (1882 ^ _374570) ^ [_436845] : [aElementOf0(_436845, sdtlpdtrp0(xN, _436498)), -(aElementOf0(_436845, sdtlpdtrp0(xN, _436496)))]]], (1890 ^ _374570) ^ [_437142, _437144] : [aElementOf0(_437144, szNzAzT0), aElementOf0(_437142, szNzAzT0), -(_437144 = _437142), 1901 ^ _374570 : [(1902 ^ _374570) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _437144)), sdtlpdtrp0(xN, _437144)))], (1904 ^ _374570) ^ [_437633] : [aElementOf0(_437633, sdtlpdtrp0(xN, _437144)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _437144)), _437633))], (1919 ^ _374570) ^ [] : [szmzizndt0(sdtlpdtrp0(xN, _437144)) = szmzizndt0(sdtlpdtrp0(xN, _437142))], (1910 ^ _374570) ^ [] : [aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _437144)), sdtlpdtrp0(xN, _437142)), 1914 ^ _374570 : [(1915 ^ _374570) ^ [] : [-(aElementOf0(1913 ^ [_437142, _437144], sdtlpdtrp0(xN, _437142)))], (1917 ^ _374570) ^ [] : [sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _437144)), 1913 ^ [_437142, _437144])]]]]], (1921 ^ _374570) ^ [_438233] : [aElementOf0(_438233, szNzAzT0), 1924 ^ _374570 : [(1925 ^ _374570) ^ [_438698] : [aSet0(_438698), 1930 ^ _374570 : [(1931 ^ _374570) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _438233)), sdtlpdtrp0(xN, _438233)))], (1933 ^ _374570) ^ [_439285] : [aElementOf0(_439285, sdtlpdtrp0(xN, _438233)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _438233)), _439285))], (1976 ^ _374570) ^ [] : [aElementOf0(_438698, slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _438233), szmzizndt0(sdtlpdtrp0(xN, _438233))), xk))], (1965 ^ _374570) ^ [] : [1967 ^ _374570 : [(1968 ^ _374570) ^ [] : [-(aElementOf0(1966 ^ [_438233, _438698], _438698))], (1970 ^ _374570) ^ [] : [aElementOf0(1966 ^ [_438233, _438698], sdtmndt0(sdtlpdtrp0(xN, _438233), szmzizndt0(sdtlpdtrp0(xN, _438233))))], (1972 ^ _374570) ^ [] : [aSubsetOf0(_438698, sdtmndt0(sdtlpdtrp0(xN, _438233), szmzizndt0(sdtlpdtrp0(xN, _438233))))]], sbrdtbr0(_438698) = xk], (1939 ^ _374570) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _438233), szmzizndt0(sdtlpdtrp0(xN, _438233)))))], (1941 ^ _374570) ^ [_439614] : [aElementOf0(_439614, sdtmndt0(sdtlpdtrp0(xN, _438233), szmzizndt0(sdtlpdtrp0(xN, _438233)))), 1944 ^ _374570 : [(1945 ^ _374570) ^ [] : [-(aElement0(_439614))], (1947 ^ _374570) ^ [] : [-(aElementOf0(_439614, sdtlpdtrp0(xN, _438233)))], (1949 ^ _374570) ^ [] : [_439614 = szmzizndt0(sdtlpdtrp0(xN, _438233))]]], (1951 ^ _374570) ^ [_439976] : [-(aElementOf0(_439976, sdtmndt0(sdtlpdtrp0(xN, _438233), szmzizndt0(sdtlpdtrp0(xN, _438233))))), aElement0(_439976), aElementOf0(_439976, sdtlpdtrp0(xN, _438233)), -(_439976 = szmzizndt0(sdtlpdtrp0(xN, _438233)))]], 1977 ^ _374570 : [(1978 ^ _374570) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _438233)), sdtlpdtrp0(xN, _438233)))], (1980 ^ _374570) ^ [_440945] : [aElementOf0(_440945, sdtlpdtrp0(xN, _438233)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _438233)), _440945))], (1986 ^ _374570) ^ [] : [-(aSet0(sdtpldt0(_438698, szmzizndt0(sdtlpdtrp0(xN, _438233)))))], (2018 ^ _374570) ^ [] : [-(aSubsetOf0(sdtpldt0(_438698, szmzizndt0(sdtlpdtrp0(xN, _438233))), xS))], (2020 ^ _374570) ^ [] : [-(sbrdtbr0(sdtpldt0(_438698, szmzizndt0(sdtlpdtrp0(xN, _438233)))) = xK)], (2022 ^ _374570) ^ [] : [-(aElementOf0(sdtpldt0(_438698, szmzizndt0(sdtlpdtrp0(xN, _438233))), slbdtsldtrb0(xS, xK)))], (2012 ^ _374570) ^ [_442037] : [aElementOf0(_442037, sdtpldt0(_438698, szmzizndt0(sdtlpdtrp0(xN, _438233)))), -(aElementOf0(_442037, xS))], (1988 ^ _374570) ^ [_441269] : [aElementOf0(_441269, sdtpldt0(_438698, szmzizndt0(sdtlpdtrp0(xN, _438233)))), 1991 ^ _374570 : [(1992 ^ _374570) ^ [] : [-(aElement0(_441269))], (1994 ^ _374570) ^ [] : [-(aElementOf0(_441269, _438698)), -(_441269 = szmzizndt0(sdtlpdtrp0(xN, _438233)))]]], (2000 ^ _374570) ^ [_441636] : [-(aElementOf0(_441636, sdtpldt0(_438698, szmzizndt0(sdtlpdtrp0(xN, _438233))))), aElement0(_441636), 2005 ^ _374570 : [(2006 ^ _374570) ^ [] : [aElementOf0(_441636, _438698)], (2008 ^ _374570) ^ [] : [_441636 = szmzizndt0(sdtlpdtrp0(xN, _438233))]]]]]]], (2024 ^ _374570) ^ [] : [-(aFunction0(xC))], (2026 ^ _374570) ^ [] : [-(szDzozmdt0(xC) = szNzAzT0)], (2028 ^ _374570) ^ [_442605] : [aElementOf0(_442605, szNzAzT0), 2031 ^ _374570 : [(2032 ^ _374570) ^ [] : [-(aFunction0(sdtlpdtrp0(xC, _442605)))], (2034 ^ _374570) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _442605)), sdtlpdtrp0(xN, _442605)))], (2036 ^ _374570) ^ [_443449] : [aElementOf0(_443449, sdtlpdtrp0(xN, _442605)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _442605)), _443449))], (2042 ^ _374570) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _442605), szmzizndt0(sdtlpdtrp0(xN, _442605)))))], (2044 ^ _374570) ^ [_443766] : [aElementOf0(_443766, sdtmndt0(sdtlpdtrp0(xN, _442605), szmzizndt0(sdtlpdtrp0(xN, _442605)))), 2047 ^ _374570 : [(2048 ^ _374570) ^ [] : [-(aElement0(_443766))], (2050 ^ _374570) ^ [] : [-(aElementOf0(_443766, sdtlpdtrp0(xN, _442605)))], (2052 ^ _374570) ^ [] : [_443766 = szmzizndt0(sdtlpdtrp0(xN, _442605))]]], (2054 ^ _374570) ^ [_444116] : [-(aElementOf0(_444116, sdtmndt0(sdtlpdtrp0(xN, _442605), szmzizndt0(sdtlpdtrp0(xN, _442605))))), aElement0(_444116), aElementOf0(_444116, sdtlpdtrp0(xN, _442605)), -(_444116 = szmzizndt0(sdtlpdtrp0(xN, _442605)))], (2068 ^ _374570) ^ [_444553] : [aElementOf0(_444553, szDzozmdt0(sdtlpdtrp0(xC, _442605))), 2071 ^ _374570 : [(2072 ^ _374570) ^ [] : [-(aSet0(_444553))], (2080 ^ _374570) ^ [] : [-(aSubsetOf0(_444553, sdtmndt0(sdtlpdtrp0(xN, _442605), szmzizndt0(sdtlpdtrp0(xN, _442605)))))], (2082 ^ _374570) ^ [] : [-(sbrdtbr0(_444553) = xk)], (2074 ^ _374570) ^ [_444828] : [aElementOf0(_444828, _444553), -(aElementOf0(_444828, sdtmndt0(sdtlpdtrp0(xN, _442605), szmzizndt0(sdtlpdtrp0(xN, _442605)))))]]], (2084 ^ _374570) ^ [_445160] : [-(aElementOf0(_445160, szDzozmdt0(sdtlpdtrp0(xC, _442605)))), sbrdtbr0(_445160) = xk, 2087 ^ _374570 : [(2097 ^ _374570) ^ [] : [aSubsetOf0(_445160, sdtmndt0(sdtlpdtrp0(xN, _442605), szmzizndt0(sdtlpdtrp0(xN, _442605))))], (2088 ^ _374570) ^ [] : [aSet0(_445160), 2092 ^ _374570 : [(2093 ^ _374570) ^ [] : [-(aElementOf0(2091 ^ [_442605, _445160], _445160))], (2095 ^ _374570) ^ [] : [aElementOf0(2091 ^ [_442605, _445160], sdtmndt0(sdtlpdtrp0(xN, _442605), szmzizndt0(sdtlpdtrp0(xN, _442605))))]]]]], (2103 ^ _374570) ^ [] : [-(szDzozmdt0(sdtlpdtrp0(xC, _442605)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _442605), szmzizndt0(sdtlpdtrp0(xN, _442605))), xk))], (2105 ^ _374570) ^ [_445887] : [2157 ^ _374570 : [(2158 ^ _374570) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _442605)), sdtlpdtrp0(xN, _442605)))], (2160 ^ _374570) ^ [_448075] : [aElementOf0(_448075, sdtlpdtrp0(xN, _442605)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _442605)), _448075))], (2190 ^ _374570) ^ [] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _442605), _445887) = sdtlpdtrp0(xc, sdtpldt0(_445887, szmzizndt0(sdtlpdtrp0(xN, _442605)))))], (2166 ^ _374570) ^ [_448326] : [aElementOf0(_448326, sdtpldt0(_445887, szmzizndt0(sdtlpdtrp0(xN, _442605)))), 2169 ^ _374570 : [(2170 ^ _374570) ^ [] : [-(aElement0(_448326))], (2172 ^ _374570) ^ [] : [-(aElementOf0(_448326, _445887)), -(_448326 = szmzizndt0(sdtlpdtrp0(xN, _442605)))]]], (2178 ^ _374570) ^ [_448693] : [-(aElementOf0(_448693, sdtpldt0(_445887, szmzizndt0(sdtlpdtrp0(xN, _442605))))), aElement0(_448693), 2183 ^ _374570 : [(2184 ^ _374570) ^ [] : [aElementOf0(_448693, _445887)], (2186 ^ _374570) ^ [] : [_448693 = szmzizndt0(sdtlpdtrp0(xN, _442605))]]]], aSet0(_445887), 2110 ^ _374570 : [(2111 ^ _374570) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _442605)), sdtlpdtrp0(xN, _442605)))], (2113 ^ _374570) ^ [_446415] : [aElementOf0(_446415, sdtlpdtrp0(xN, _442605)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _442605)), _446415))], (2156 ^ _374570) ^ [] : [aElementOf0(_445887, slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _442605), szmzizndt0(sdtlpdtrp0(xN, _442605))), xk))], (2145 ^ _374570) ^ [] : [2147 ^ _374570 : [(2148 ^ _374570) ^ [] : [-(aElementOf0(2146 ^ [_442605, _445887], _445887))], (2150 ^ _374570) ^ [] : [aElementOf0(2146 ^ [_442605, _445887], sdtmndt0(sdtlpdtrp0(xN, _442605), szmzizndt0(sdtlpdtrp0(xN, _442605))))], (2152 ^ _374570) ^ [] : [aSubsetOf0(_445887, sdtmndt0(sdtlpdtrp0(xN, _442605), szmzizndt0(sdtlpdtrp0(xN, _442605))))]], sbrdtbr0(_445887) = xk], (2119 ^ _374570) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _442605), szmzizndt0(sdtlpdtrp0(xN, _442605)))))], (2121 ^ _374570) ^ [_446744] : [aElementOf0(_446744, sdtmndt0(sdtlpdtrp0(xN, _442605), szmzizndt0(sdtlpdtrp0(xN, _442605)))), 2124 ^ _374570 : [(2125 ^ _374570) ^ [] : [-(aElement0(_446744))], (2127 ^ _374570) ^ [] : [-(aElementOf0(_446744, sdtlpdtrp0(xN, _442605)))], (2129 ^ _374570) ^ [] : [_446744 = szmzizndt0(sdtlpdtrp0(xN, _442605))]]], (2131 ^ _374570) ^ [_447106] : [-(aElementOf0(_447106, sdtmndt0(sdtlpdtrp0(xN, _442605), szmzizndt0(sdtlpdtrp0(xN, _442605))))), aElement0(_447106), aElementOf0(_447106, sdtlpdtrp0(xN, _442605)), -(_447106 = szmzizndt0(sdtlpdtrp0(xN, _442605)))]]]]], (2192 ^ _374570) ^ [_449195] : [aElementOf0(_449195, szNzAzT0), 2195 ^ _374570 : [(2196 ^ _374570) ^ [] : [-(aSet0(sdtlcdtrc0(sdtlpdtrp0(xC, _449195), szDzozmdt0(sdtlpdtrp0(xC, _449195)))))], (2223 ^ _374570) ^ [] : [-(aSubsetOf0(sdtlcdtrc0(sdtlpdtrp0(xC, _449195), szDzozmdt0(sdtlpdtrp0(xC, _449195))), xT))], (2217 ^ _374570) ^ [_450316] : [aElementOf0(_450316, sdtlcdtrc0(sdtlpdtrp0(xC, _449195), szDzozmdt0(sdtlpdtrp0(xC, _449195)))), -(aElementOf0(_450316, xT))], (2198 ^ _374570) ^ [_449545] : [aElementOf0(_449545, sdtlcdtrc0(sdtlpdtrp0(xC, _449195), szDzozmdt0(sdtlpdtrp0(xC, _449195)))), 2202 ^ _374570 : [(2203 ^ _374570) ^ [] : [-(aElementOf0(2201 ^ [_449195, _449545], szDzozmdt0(sdtlpdtrp0(xC, _449195))))], (2205 ^ _374570) ^ [] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _449195), 2201 ^ [_449195, _449545]) = _449545)]]], (2207 ^ _374570) ^ [_449909] : [-(aElementOf0(_449909, sdtlcdtrc0(sdtlpdtrp0(xC, _449195), szDzozmdt0(sdtlpdtrp0(xC, _449195))))), 2208 ^ _374570 : [(2209 ^ _374570) ^ [_450025] : [aElementOf0(_450025, szDzozmdt0(sdtlpdtrp0(xC, _449195))), sdtlpdtrp0(sdtlpdtrp0(xC, _449195), _450025) = _449909]]]]], (2225 ^ _374570) ^ [_450604] : [aElementOf0(_450604, szNzAzT0), 2228 ^ _374570 : [(2229 ^ _374570) ^ [_451103] : [isCountable0(_451103), 2232 ^ _374570 : [(2233 ^ _374570) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _450604)), sdtlpdtrp0(xN, _450604)))], (2235 ^ _374570) ^ [_451680] : [aElementOf0(_451680, sdtlpdtrp0(xN, _450604)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _450604)), _451680))], (2276 ^ _374570) ^ [] : [aSubsetOf0(_451103, sdtmndt0(sdtlpdtrp0(xN, _450604), szmzizndt0(sdtlpdtrp0(xN, _450604))))], (2267 ^ _374570) ^ [] : [aSet0(_451103), 2271 ^ _374570 : [(2272 ^ _374570) ^ [] : [-(aElementOf0(2270 ^ [_450604, _451103], _451103))], (2274 ^ _374570) ^ [] : [aElementOf0(2270 ^ [_450604, _451103], sdtmndt0(sdtlpdtrp0(xN, _450604), szmzizndt0(sdtlpdtrp0(xN, _450604))))]]], (2241 ^ _374570) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _450604), szmzizndt0(sdtlpdtrp0(xN, _450604)))))], (2243 ^ _374570) ^ [_452009] : [aElementOf0(_452009, sdtmndt0(sdtlpdtrp0(xN, _450604), szmzizndt0(sdtlpdtrp0(xN, _450604)))), 2246 ^ _374570 : [(2247 ^ _374570) ^ [] : [-(aElement0(_452009))], (2249 ^ _374570) ^ [] : [-(aElementOf0(_452009, sdtlpdtrp0(xN, _450604)))], (2251 ^ _374570) ^ [] : [_452009 = szmzizndt0(sdtlpdtrp0(xN, _450604))]]], (2253 ^ _374570) ^ [_452371] : [-(aElementOf0(_452371, sdtmndt0(sdtlpdtrp0(xN, _450604), szmzizndt0(sdtlpdtrp0(xN, _450604))))), aElement0(_452371), aElementOf0(_452371, sdtlpdtrp0(xN, _450604)), -(_452371 = szmzizndt0(sdtlpdtrp0(xN, _450604)))]], 2279 ^ _374570 : [(2280 ^ _374570) ^ [_453204] : [aSet0(_453204), 2285 ^ _374570 : [(2297 ^ _374570) ^ [] : [aElementOf0(_453204, slbdtsldtrb0(_451103, xk))], (2286 ^ _374570) ^ [] : [2288 ^ _374570 : [(2289 ^ _374570) ^ [] : [-(aElementOf0(2287 ^ [_450604, _451103, _453204], _453204))], (2291 ^ _374570) ^ [] : [aElementOf0(2287 ^ [_450604, _451103, _453204], _451103)], (2293 ^ _374570) ^ [] : [aSubsetOf0(_453204, _451103)]], sbrdtbr0(_453204) = xk]], 2298 ^ _374570 : [(2299 ^ _374570) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _450604)), sdtlpdtrp0(xN, _450604)))], (2301 ^ _374570) ^ [_454099] : [aElementOf0(_454099, sdtlpdtrp0(xN, _450604)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _450604)), _454099))], (2307 ^ _374570) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _450604), szmzizndt0(sdtlpdtrp0(xN, _450604)))))], (2339 ^ _374570) ^ [] : [-(aSubsetOf0(_453204, sdtmndt0(sdtlpdtrp0(xN, _450604), szmzizndt0(sdtlpdtrp0(xN, _450604)))))], (2341 ^ _374570) ^ [] : [-(aElementOf0(_453204, slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _450604), szmzizndt0(sdtlpdtrp0(xN, _450604))), xk)))], (2333 ^ _374570) ^ [_455259] : [aElementOf0(_455259, _453204), -(aElementOf0(_455259, sdtmndt0(sdtlpdtrp0(xN, _450604), szmzizndt0(sdtlpdtrp0(xN, _450604)))))], (2309 ^ _374570) ^ [_454436] : [aElementOf0(_454436, sdtmndt0(sdtlpdtrp0(xN, _450604), szmzizndt0(sdtlpdtrp0(xN, _450604)))), 2312 ^ _374570 : [(2313 ^ _374570) ^ [] : [-(aElement0(_454436))], (2315 ^ _374570) ^ [] : [-(aElementOf0(_454436, sdtlpdtrp0(xN, _450604)))], (2317 ^ _374570) ^ [] : [_454436 = szmzizndt0(sdtlpdtrp0(xN, _450604))]]], (2319 ^ _374570) ^ [_454810] : [-(aElementOf0(_454810, sdtmndt0(sdtlpdtrp0(xN, _450604), szmzizndt0(sdtlpdtrp0(xN, _450604))))), aElement0(_454810), aElementOf0(_454810, sdtlpdtrp0(xN, _450604)), -(_454810 = szmzizndt0(sdtlpdtrp0(xN, _450604)))]]]]]]], (2343 ^ _374570) ^ [_455673] : [aElementOf0(_455673, szNzAzT0), 2347 ^ _374570 : [(2348 ^ _374570) ^ [] : [-(aElementOf0(2346 ^ [_455673], xT))], (2351 ^ _374570) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _455673)), sdtlpdtrp0(xN, _455673)))], (2353 ^ _374570) ^ [_456715] : [aElementOf0(_456715, sdtlpdtrp0(xN, _455673)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _455673)), _456715))], (2359 ^ _374570) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _455673), szmzizndt0(sdtlpdtrp0(xN, _455673)))))], (2361 ^ _374570) ^ [_457032] : [aElementOf0(_457032, sdtmndt0(sdtlpdtrp0(xN, _455673), szmzizndt0(sdtlpdtrp0(xN, _455673)))), 2364 ^ _374570 : [(2365 ^ _374570) ^ [] : [-(aElement0(_457032))], (2367 ^ _374570) ^ [] : [-(aElementOf0(_457032, sdtlpdtrp0(xN, _455673)))], (2369 ^ _374570) ^ [] : [_457032 = szmzizndt0(sdtlpdtrp0(xN, _455673))]]], (2371 ^ _374570) ^ [_457382] : [-(aElementOf0(_457382, sdtmndt0(sdtlpdtrp0(xN, _455673), szmzizndt0(sdtlpdtrp0(xN, _455673))))), aElement0(_457382), aElementOf0(_457382, sdtlpdtrp0(xN, _455673)), -(_457382 = szmzizndt0(sdtlpdtrp0(xN, _455673)))], (2385 ^ _374570) ^ [] : [-(aSet0(2349 ^ [_455673]))], (2387 ^ _374570) ^ [_457867] : [aElementOf0(_457867, 2349 ^ [_455673]), -(aElementOf0(_457867, sdtmndt0(sdtlpdtrp0(xN, _455673), szmzizndt0(sdtlpdtrp0(xN, _455673)))))], (2393 ^ _374570) ^ [] : [-(aSubsetOf0(2349 ^ [_455673], sdtmndt0(sdtlpdtrp0(xN, _455673), szmzizndt0(sdtlpdtrp0(xN, _455673)))))], (2395 ^ _374570) ^ [] : [-(isCountable0(2349 ^ [_455673]))], (2397 ^ _374570) ^ [_458225] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _455673), _458225) = 2346 ^ [_455673]), aSet0(_458225), 2402 ^ _374570 : [(2414 ^ _374570) ^ [] : [aElementOf0(_458225, slbdtsldtrb0(2349 ^ [_455673], xk))], (2403 ^ _374570) ^ [] : [2405 ^ _374570 : [(2406 ^ _374570) ^ [] : [-(aElementOf0(2404 ^ [_455673, _458225], _458225))], (2408 ^ _374570) ^ [] : [aElementOf0(2404 ^ [_455673, _458225], 2349 ^ [_455673])], (2410 ^ _374570) ^ [] : [aSubsetOf0(_458225, 2349 ^ [_455673])]], sbrdtbr0(_458225) = xk]]]]], (2418 ^ _374570) ^ [_458985] : [aElementOf0(_458985, szNzAzT0), 2422 ^ _374570 : [(2423 ^ _374570) ^ [] : [-(aElementOf0(2421 ^ [_458985], xT))], (2425 ^ _374570) ^ [_459376] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _458985), _459376) = 2421 ^ [_458985]), aSet0(_459376), 2430 ^ _374570 : [(2442 ^ _374570) ^ [] : [aElementOf0(_459376, slbdtsldtrb0(sdtlpdtrp0(xN, szszuzczcdt0(_458985)), xk))], (2431 ^ _374570) ^ [] : [2433 ^ _374570 : [(2434 ^ _374570) ^ [] : [-(aElementOf0(2432 ^ [_458985, _459376], _459376))], (2436 ^ _374570) ^ [] : [aElementOf0(2432 ^ [_458985, _459376], sdtlpdtrp0(xN, szszuzczcdt0(_458985)))], (2438 ^ _374570) ^ [] : [aSubsetOf0(_459376, sdtlpdtrp0(xN, szszuzczcdt0(_458985)))]], sbrdtbr0(_459376) = xk]]]]], (2446 ^ _374570) ^ [] : [-(aFunction0(xe))], (2448 ^ _374570) ^ [] : [-(szDzozmdt0(xe) = szNzAzT0)], (2450 ^ _374570) ^ [_460224] : [aElementOf0(_460224, szNzAzT0), 2453 ^ _374570 : [(2454 ^ _374570) ^ [] : [-(aElementOf0(sdtlpdtrp0(xe, _460224), sdtlpdtrp0(xN, _460224)))], (2462 ^ _374570) ^ [] : [-(sdtlpdtrp0(xe, _460224) = szmzizndt0(sdtlpdtrp0(xN, _460224)))], (2456 ^ _374570) ^ [_460479] : [aElementOf0(_460479, sdtlpdtrp0(xN, _460224)), -(sdtlseqdt0(sdtlpdtrp0(xe, _460224), _460479))]]], (2464 ^ _374570) ^ [] : [-(aFunction0(xd))], (2466 ^ _374570) ^ [] : [-(szDzozmdt0(xd) = szNzAzT0)], (2468 ^ _374570) ^ [_460860] : [aElementOf0(_460860, szNzAzT0), 2471 ^ _374570 : [(2472 ^ _374570) ^ [_461056] : [-(sdtlpdtrp0(xd, _460860) = sdtlpdtrp0(sdtlpdtrp0(xC, _460860), _461056)), aSet0(_461056), 2477 ^ _374570 : [(2489 ^ _374570) ^ [] : [aElementOf0(_461056, slbdtsldtrb0(sdtlpdtrp0(xN, szszuzczcdt0(_460860)), xk))], (2478 ^ _374570) ^ [] : [2480 ^ _374570 : [(2481 ^ _374570) ^ [] : [-(aElementOf0(2479 ^ [_460860, _461056], _461056))], (2483 ^ _374570) ^ [] : [aElementOf0(2479 ^ [_460860, _461056], sdtlpdtrp0(xN, szszuzczcdt0(_460860)))], (2485 ^ _374570) ^ [] : [aSubsetOf0(_461056, sdtlpdtrp0(xN, szszuzczcdt0(_460860)))]], sbrdtbr0(_461056) = xk]]]]], (2493 ^ _374570) ^ [] : [-(aSet0(sdtlcdtrc0(xd, szDzozmdt0(xd))))], (2520 ^ _374570) ^ [] : [-(aSubsetOf0(sdtlcdtrc0(xd, szDzozmdt0(xd)), xT))], (2514 ^ _374570) ^ [_462545] : [aElementOf0(_462545, sdtlcdtrc0(xd, szDzozmdt0(xd))), -(aElementOf0(_462545, xT))], (2495 ^ _374570) ^ [_461898] : [aElementOf0(_461898, sdtlcdtrc0(xd, szDzozmdt0(xd))), 2499 ^ _374570 : [(2500 ^ _374570) ^ [] : [-(aElementOf0(2498 ^ [_461898], szDzozmdt0(xd)))], (2502 ^ _374570) ^ [] : [-(sdtlpdtrp0(xd, 2498 ^ [_461898]) = _461898)]]], (2504 ^ _374570) ^ [_462198] : [-(aElementOf0(_462198, sdtlcdtrc0(xd, szDzozmdt0(xd)))), 2505 ^ _374570 : [(2506 ^ _374570) ^ [_462291] : [aElementOf0(_462291, szDzozmdt0(xd)), sdtlpdtrp0(xd, _462291) = _462198]]], (2522 ^ _374570) ^ [] : [-(aElementOf0(szDzizrdt0(xd), xT))], (2524 ^ _374570) ^ [] : [-(aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd))))], (2526 ^ _374570) ^ [_462911] : [aElementOf0(_462911, sdtlbdtrb0(xd, szDzizrdt0(xd))), 2529 ^ _374570 : [(2530 ^ _374570) ^ [] : [-(aElementOf0(_462911, szDzozmdt0(xd)))], (2532 ^ _374570) ^ [] : [-(sdtlpdtrp0(xd, _462911) = szDzizrdt0(xd))]]], (2534 ^ _374570) ^ [_463146] : [-(aElementOf0(_463146, sdtlbdtrb0(xd, szDzizrdt0(xd)))), aElementOf0(_463146, szDzozmdt0(xd)), sdtlpdtrp0(xd, _463146) = szDzizrdt0(xd)], (2544 ^ _374570) ^ [] : [-(aSet0(xO))], (2546 ^ _374570) ^ [] : [-(aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd))))], (2548 ^ _374570) ^ [_463588] : [aElementOf0(_463588, sdtlbdtrb0(xd, szDzizrdt0(xd))), 2551 ^ _374570 : [(2552 ^ _374570) ^ [] : [-(aElementOf0(_463588, szDzozmdt0(xd)))], (2554 ^ _374570) ^ [] : [-(sdtlpdtrp0(xd, _463588) = szDzizrdt0(xd))]]], (2556 ^ _374570) ^ [_463823] : [-(aElementOf0(_463823, sdtlbdtrb0(xd, szDzizrdt0(xd)))), aElementOf0(_463823, szDzozmdt0(xd)), sdtlpdtrp0(xd, _463823) = szDzizrdt0(xd)], (2585 ^ _374570) ^ [] : [-(xO = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))], (2566 ^ _374570) ^ [_464135] : [aElementOf0(_464135, xO), 2570 ^ _374570 : [(2571 ^ _374570) ^ [] : [-(aElementOf0(2569 ^ [_464135], sdtlbdtrb0(xd, szDzizrdt0(xd))))], (2573 ^ _374570) ^ [] : [-(sdtlpdtrp0(xe, 2569 ^ [_464135]) = _464135)]]], (2575 ^ _374570) ^ [_464435] : [-(aElementOf0(_464435, xO)), 2576 ^ _374570 : [(2577 ^ _374570) ^ [_464528] : [aElementOf0(_464528, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlpdtrp0(xe, _464528) = _464435]]], (2587 ^ _374570) ^ [] : [-(aSet0(xO))], (2589 ^ _374570) ^ [] : [-(isCountable0(xO))], (2591 ^ _374570) ^ [_464933] : [2601 ^ _374570 : [(2602 ^ _374570) ^ [] : [-(aElementOf0(2600 ^ [_464933], szNzAzT0))], (2604 ^ _374570) ^ [] : [-(sdtlpdtrp0(xd, 2600 ^ [_464933]) = szDzizrdt0(xd))], (2606 ^ _374570) ^ [] : [-(aElementOf0(2600 ^ [_464933], sdtlbdtrb0(xd, szDzizrdt0(xd))))], (2608 ^ _374570) ^ [] : [-(sdtlpdtrp0(xe, 2600 ^ [_464933]) = _464933)]], 2592 ^ _374570 : [(2599 ^ _374570) ^ [] : [aElementOf0(_464933, xO)], (2593 ^ _374570) ^ [_465081] : [aElementOf0(_465081, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlpdtrp0(xe, _465081) = _464933]]], (2616 ^ _374570) ^ [] : [-(aSubsetOf0(xO, xS))], (2610 ^ _374570) ^ [_465688] : [aElementOf0(_465688, xO), -(aElementOf0(_465688, xS))], (2618 ^ _374570) ^ [] : [-(aSet0(xQ))], (2626 ^ _374570) ^ [] : [-(aSubsetOf0(xQ, xO))], (2628 ^ _374570) ^ [] : [-(sbrdtbr0(xQ) = xK)], (2630 ^ _374570) ^ [] : [-(aElementOf0(xQ, slbdtsldtrb0(xO, xK)))], (2620 ^ _374570) ^ [_465986] : [aElementOf0(_465986, xQ), -(aElementOf0(_465986, xO))], (2639 ^ _374570) ^ [] : [-(aElementOf0(2637 ^ [], xQ))], (2641 ^ _374570) ^ [] : [xQ = slcrc0], (2632 ^ _374570) ^ [_466347] : [aElementOf0(_466347, xQ), -(aElementOf0(_466347, xO))], (2649 ^ _374570) ^ [] : [-(aSubsetOf0(xQ, szNzAzT0))], (2643 ^ _374570) ^ [_466685] : [aElementOf0(_466685, xQ), -(aElementOf0(_466685, szNzAzT0))], (2651 ^ _374570) ^ [_466930] : [aElementOf0(_466930, xQ), -(aElementOf0(_466930, xS))], (2657 ^ _374570) ^ [] : [-(aSubsetOf0(xQ, xS))], (2665 ^ _374570) ^ [] : [-(aSubsetOf0(xQ, xS))], (2667 ^ _374570) ^ [] : [-(aElementOf0(xQ, szDzozmdt0(xc)))], (2659 ^ _374570) ^ [_467173] : [aElementOf0(_467173, xQ), -(aElementOf0(_467173, xS))], (2669 ^ _374570) ^ [] : [-(aElementOf0(xp, xQ))], (2677 ^ _374570) ^ [] : [-(xp = szmzizndt0(xQ))], (2671 ^ _374570) ^ [_467532] : [aElementOf0(_467532, xQ), -(sdtlseqdt0(xp, _467532))], (2713 ^ _374570) ^ [] : [-(aElementOf0(xp, xQ))], (2716 ^ _374570) ^ [] : [-(aElementOf0(2714 ^ [], sdtlbdtrb0(xd, szDzizrdt0(xd))))], (2718 ^ _374570) ^ [] : [-(sdtlpdtrp0(xe, 2714 ^ []) = xp)], (2726 ^ _374570) ^ [] : [-(aSubsetOf0(xP, xQ))], (2720 ^ _374570) ^ [_468980] : [aElementOf0(_468980, xP), -(aElementOf0(_468980, xQ))], (2736 ^ _374570) ^ [] : [-(sbrdtbr0(xP) = xk)], (2738 ^ _374570) ^ [] : [-(aElementOf0(xP, slbdtsldtrb0(xO, xk)))], (2740 ^ _374570) ^ [] : [-(aElementOf0(xn, szDzozmdt0(xd)))], (2742 ^ _374570) ^ [] : [-(sdtlpdtrp0(xd, xn) = szDzizrdt0(xd))], (2744 ^ _374570) ^ [] : [-(aElementOf0(xn, sdtlbdtrb0(xd, szDzizrdt0(xd))))], (2746 ^ _374570) ^ [] : [-(aElementOf0(xn, szNzAzT0))], (2748 ^ _374570) ^ [] : [-(sdtlpdtrp0(xe, xn) = xp)], (2750 ^ _374570) ^ [] : [-(sdtlpdtrp0(xd, xn) = szDzizrdt0(xd))], (2752 ^ _374570) ^ [] : [-(aElement0(xx))], (2754 ^ _374570) ^ [] : [-(aElementOf0(xx, xQ))], (2756 ^ _374570) ^ [] : [xx = szmzizndt0(xQ)], (2758 ^ _374570) ^ [] : [-(aElementOf0(xx, xP))], (2734 ^ _374570) ^ [] : [-(aSubsetOf0(xP, xO))], (2728 ^ _374570) ^ [_469225] : [aElementOf0(_469225, xP), -(aElementOf0(_469225, xO))], (2679 ^ _374570) ^ [] : [-(aSet0(xP))], (2681 ^ _374570) ^ [_467832] : [aElementOf0(_467832, xQ), -(sdtlseqdt0(szmzizndt0(xQ), _467832))], (2711 ^ _374570) ^ [] : [-(xP = sdtmndt0(xQ, szmzizndt0(xQ)))], (2687 ^ _374570) ^ [_468051] : [aElementOf0(_468051, xP), 2690 ^ _374570 : [(2691 ^ _374570) ^ [] : [-(aElement0(_468051))], (2693 ^ _374570) ^ [] : [-(aElementOf0(_468051, xQ))], (2695 ^ _374570) ^ [] : [_468051 = szmzizndt0(xQ)]]], (2697 ^ _374570) ^ [_468351] : [-(aElementOf0(_468351, xP)), aElement0(_468351), aElementOf0(_468351, xQ), -(_468351 = szmzizndt0(xQ))]], input).
% 0.39/1.38 ncf('1',plain,[aElementOf0(xx, szNzAzT0)],start(2760 ^ 0)).
% 0.39/1.38 ncf('1.1',plain,[-(aElementOf0(xx, szNzAzT0)), 347 : aElementOf0(xx, xQ), 347 : aSubsetOf0(xQ, szNzAzT0), 341 : aSet0(szNzAzT0)],extension(337 ^ 1,bind([[_385407, _385583, _385792], [szNzAzT0, xQ, xx]]))).
% 0.39/1.38 ncf('1.1.1',plain,[-(aElementOf0(xx, xQ))],extension(2754 ^ 6)).
% 0.39/1.38 ncf('1.1.2',plain,[-(aSubsetOf0(xQ, szNzAzT0))],extension(2649 ^ 4)).
% 0.39/1.38 ncf('1.1.3',plain,[-(aSet0(szNzAzT0))],extension(644 ^ 2)).
% 0.39/1.38 %-----------------------------------------------------
% 0.39/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------