%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM607+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n025.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:08 EDT 2023
% Result : Theorem 0.56s 1.37s
% Output : Proof 0.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : NUM607+3 : TPTP v8.1.2. Released v4.0.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n025.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:40:48 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.56/1.37
% 0.56/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.56/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.56/1.37 %-----------------------------------------------------
% 0.56/1.37 ncf(matrix, plain, [(2652 ^ _362047) ^ [] : [-(aElementOf0(2650 ^ [], xQ))], (2654 ^ _362047) ^ [] : [aElementOf0(2650 ^ [], xS)], (2656 ^ _362047) ^ [] : [aSubsetOf0(xQ, xS)], (2659 ^ _362047) ^ [] : [-(aElementOf0(2657 ^ [], xQ))], (2661 ^ _362047) ^ [] : [aElementOf0(2657 ^ [], xS)], (2663 ^ _362047) ^ [] : [aSubsetOf0(xQ, xS)], (2665 ^ _362047) ^ [] : [aElementOf0(xQ, szDzozmdt0(xc))], (126 ^ _362047) ^ [_366068, _366070] : [_366070 = _366068, -(szmzazxdt0(_366070) = szmzazxdt0(_366068))], (132 ^ _362047) ^ [_366286, _366288] : [_366288 = _366286, -(slbdtrb0(_366288) = slbdtrb0(_366286))], (138 ^ _362047) ^ [_366532, _366534, _366536, _366538] : [-(sdtexdt0(_366538, _366534) = sdtexdt0(_366536, _366532)), _366538 = _366536, _366534 = _366532], (148 ^ _362047) ^ [_366891, _366893, _366895, _366897] : [-(sdtpldt0(_366897, _366893) = sdtpldt0(_366895, _366891)), _366897 = _366895, _366893 = _366891], (158 ^ _362047) ^ [_367250, _367252, _367254, _367256] : [-(sdtmndt0(_367256, _367252) = sdtmndt0(_367254, _367250)), _367256 = _367254, _367252 = _367250], (168 ^ _362047) ^ [_367581, _367583] : [_367583 = _367581, -(szmzizndt0(_367583) = szmzizndt0(_367581))], (174 ^ _362047) ^ [_367799, _367801] : [_367801 = _367799, -(szszuzczcdt0(_367801) = szszuzczcdt0(_367799))], (180 ^ _362047) ^ [_368045, _368047, _368049, _368051] : [-(sdtlcdtrc0(_368051, _368047) = sdtlcdtrc0(_368049, _368045)), _368051 = _368049, _368047 = _368045], (190 ^ _362047) ^ [_368404, _368406, _368408, _368410] : [-(sdtlbdtrb0(_368410, _368406) = sdtlbdtrb0(_368408, _368404)), _368410 = _368408, _368406 = _368404], (200 ^ _362047) ^ [_368735, _368737] : [_368737 = _368735, -(szDzizrdt0(_368737) = szDzizrdt0(_368735))], (206 ^ _362047) ^ [_368981, _368983, _368985, _368987] : [-(sdtlpdtrp0(_368987, _368983) = sdtlpdtrp0(_368985, _368981)), _368987 = _368985, _368983 = _368981], (216 ^ _362047) ^ [_369312, _369314] : [_369314 = _369312, -(sbrdtbr0(_369314) = sbrdtbr0(_369312))], (232 ^ _362047) ^ [_369869, _369871] : [_369871 = _369869, -(szDzozmdt0(_369871) = szDzozmdt0(_369869))], (222 ^ _362047) ^ [_369558, _369560, _369562, _369564] : [-(slbdtsldtrb0(_369564, _369560) = slbdtsldtrb0(_369562, _369558)), _369564 = _369562, _369560 = _369558], (2 ^ _362047) ^ [_362191] : [-(_362191 = _362191)], (4 ^ _362047) ^ [_362298, _362300] : [_362300 = _362298, -(_362298 = _362300)], (10 ^ _362047) ^ [_362502, _362504, _362506] : [-(_362506 = _362502), _362506 = _362504, _362504 = _362502], (20 ^ _362047) ^ [_362815, _362817] : [-(isFinite0(_362815)), _362817 = _362815, isFinite0(_362817)], (30 ^ _362047) ^ [_363138, _363140, _363142, _363144] : [-(iLess0(_363142, _363138)), iLess0(_363144, _363140), _363144 = _363142, _363140 = _363138], (44 ^ _362047) ^ [_363554, _363556] : [-(aElement0(_363554)), _363556 = _363554, aElement0(_363556)], (54 ^ _362047) ^ [_363877, _363879, _363881, _363883] : [-(sdtlseqdt0(_363881, _363877)), sdtlseqdt0(_363883, _363879), _363883 = _363881, _363879 = _363877], (68 ^ _362047) ^ [_364293, _364295] : [-(aFunction0(_364293)), _364295 = _364293, aFunction0(_364295)], (78 ^ _362047) ^ [_364588, _364590] : [-(isCountable0(_364588)), _364590 = _364588, isCountable0(_364590)], (88 ^ _362047) ^ [_364883, _364885] : [-(aSet0(_364883)), _364885 = _364883, aSet0(_364885)], (98 ^ _362047) ^ [_365206, _365208, _365210, _365212] : [-(aSubsetOf0(_365210, _365206)), aSubsetOf0(_365212, _365208), _365212 = _365210, _365208 = _365206], (112 ^ _362047) ^ [_365630, _365632, _365634, _365636] : [-(aElementOf0(_365634, _365630)), aElementOf0(_365636, _365632), _365636 = _365634, _365632 = _365630], (238 ^ _362047) ^ [_370159] : [aSet0(_370159), true___, -(true___)], (248 ^ _362047) ^ [_370414] : [aElement0(_370414), true___, -(true___)], (258 ^ _362047) ^ [_370669] : [aSet0(_370669), 261 ^ _362047 : [(262 ^ _362047) ^ [_370799] : [aElementOf0(_370799, _370669), -(aElement0(_370799))]]], (268 ^ _362047) ^ [_371000] : [aSet0(_371000), isFinite0(_371000), true___, -(true___)], (282 ^ _362047) ^ [_371370] : [_371370 = slcrc0, 285 ^ _362047 : [(286 ^ _362047) ^ [] : [-(aSet0(_371370))], (288 ^ _362047) ^ [_371551] : [aElementOf0(_371551, _371370)]]], (290 ^ _362047) ^ [_371619] : [-(_371619 = slcrc0), aSet0(_371619), -(aElementOf0(295 ^ [_371619], _371619))], (301 ^ _362047) ^ [] : [-(isFinite0(slcrc0))], (303 ^ _362047) ^ [_372001] : [aSet0(_372001), isCountable0(_372001), true___, -(true___)], (317 ^ _362047) ^ [_372342] : [isFinite0(_372342), aSet0(_372342), isCountable0(_372342)], (327 ^ _362047) ^ [_372612] : [_372612 = slcrc0, aSet0(_372612), isCountable0(_372612)], (337 ^ _362047) ^ [_372884] : [aSet0(_372884), 340 ^ _362047 : [(341 ^ _362047) ^ [_373060] : [aSubsetOf0(_373060, _372884), 344 ^ _362047 : [(345 ^ _362047) ^ [] : [-(aSet0(_373060))], (347 ^ _362047) ^ [_373269] : [aElementOf0(_373269, _373060), -(aElementOf0(_373269, _372884))]]], (353 ^ _362047) ^ [_373448] : [-(aSubsetOf0(_373448, _372884)), aSet0(_373448), 359 ^ _362047 : [(360 ^ _362047) ^ [] : [-(aElementOf0(358 ^ [_372884, _373448], _373448))], (362 ^ _362047) ^ [] : [aElementOf0(358 ^ [_372884, _373448], _372884)]]]]], (366 ^ _362047) ^ [_373885] : [aSet0(_373885), isFinite0(_373885), 373 ^ _362047 : [(374 ^ _362047) ^ [_374098] : [aSubsetOf0(_374098, _373885), -(isFinite0(_374098))]]], (380 ^ _362047) ^ [_374301] : [aSet0(_374301), -(aSubsetOf0(_374301, _374301))], (386 ^ _362047) ^ [_374503, _374505] : [aSet0(_374505), aSet0(_374503), -(_374505 = _374503), aSubsetOf0(_374505, _374503), aSubsetOf0(_374503, _374505)], (404 ^ _362047) ^ [_374992, _374994, _374996] : [aSet0(_374996), aSet0(_374994), aSet0(_374992), -(aSubsetOf0(_374996, _374992)), aSubsetOf0(_374996, _374994), aSubsetOf0(_374994, _374992)], (426 ^ _362047) ^ [_375578, _375580] : [aSet0(_375580), aElement0(_375578), 433 ^ _362047 : [(464 ^ _362047) ^ [_376839] : [-(_376839 = sdtpldt0(_375580, _375578)), aSet0(_376839), 472 ^ _362047 : [(473 ^ _362047) ^ [] : [-(aElementOf0(469 ^ [_375578, _375580, _376839], _376839))], (475 ^ _362047) ^ [] : [aElement0(469 ^ [_375578, _375580, _376839]), 478 ^ _362047 : [(479 ^ _362047) ^ [] : [aElementOf0(469 ^ [_375578, _375580, _376839], _375580)], (481 ^ _362047) ^ [] : [469 ^ [_375578, _375580, _376839] = _375578]]]], 482 ^ _362047 : [(491 ^ _362047) ^ [] : [aElementOf0(469 ^ [_375578, _375580, _376839], _376839)], (483 ^ _362047) ^ [] : [-(aElement0(469 ^ [_375578, _375580, _376839]))], (485 ^ _362047) ^ [] : [-(aElementOf0(469 ^ [_375578, _375580, _376839], _375580)), -(469 ^ [_375578, _375580, _376839] = _375578)]]], (434 ^ _362047) ^ [_375859] : [_375859 = sdtpldt0(_375580, _375578), 437 ^ _362047 : [(438 ^ _362047) ^ [] : [-(aSet0(_375859))], (440 ^ _362047) ^ [_376122] : [aElementOf0(_376122, _375859), 443 ^ _362047 : [(444 ^ _362047) ^ [] : [-(aElement0(_376122))], (446 ^ _362047) ^ [] : [-(aElementOf0(_376122, _375580)), -(_376122 = _375578)]]], (452 ^ _362047) ^ [_376477] : [-(aElementOf0(_376477, _375859)), aElement0(_376477), 457 ^ _362047 : [(458 ^ _362047) ^ [] : [aElementOf0(_376477, _375580)], (460 ^ _362047) ^ [] : [_376477 = _375578]]]]]]], (495 ^ _362047) ^ [_377876, _377878] : [aSet0(_377878), aElement0(_377876), 502 ^ _362047 : [(533 ^ _362047) ^ [_379144] : [-(_379144 = sdtmndt0(_377878, _377876)), aSet0(_379144), 553 ^ _362047 : [(554 ^ _362047) ^ [] : [-(aElement0(538 ^ [_377876, _377878, _379144]))], (556 ^ _362047) ^ [] : [-(aElementOf0(538 ^ [_377876, _377878, _379144], _377878))], (558 ^ _362047) ^ [] : [538 ^ [_377876, _377878, _379144] = _377876], (560 ^ _362047) ^ [] : [aElementOf0(538 ^ [_377876, _377878, _379144], _379144)]], 541 ^ _362047 : [(542 ^ _362047) ^ [] : [-(aElementOf0(538 ^ [_377876, _377878, _379144], _379144))], (544 ^ _362047) ^ [] : [aElement0(538 ^ [_377876, _377878, _379144]), aElementOf0(538 ^ [_377876, _377878, _379144], _377878), -(538 ^ [_377876, _377878, _379144] = _377876)]]], (503 ^ _362047) ^ [_378159] : [_378159 = sdtmndt0(_377878, _377876), 506 ^ _362047 : [(507 ^ _362047) ^ [] : [-(aSet0(_378159))], (509 ^ _362047) ^ [_378424] : [aElementOf0(_378424, _378159), 512 ^ _362047 : [(513 ^ _362047) ^ [] : [-(aElement0(_378424))], (515 ^ _362047) ^ [] : [-(aElementOf0(_378424, _377878))], (517 ^ _362047) ^ [] : [_378424 = _377876]]], (519 ^ _362047) ^ [_378760] : [-(aElementOf0(_378760, _378159)), aElement0(_378760), aElementOf0(_378760, _377878), -(_378760 = _377876)]]]]], (564 ^ _362047) ^ [_380174] : [aSet0(_380174), 567 ^ _362047 : [(568 ^ _362047) ^ [_380311] : [aElementOf0(_380311, _380174), -(sdtpldt0(sdtmndt0(_380174, _380311), _380311) = _380174)]]], (574 ^ _362047) ^ [_380540, _380542] : [aElement0(_380542), aSet0(_380540), -(aElementOf0(_380542, _380540)), -(sdtmndt0(sdtpldt0(_380540, _380542), _380542) = _380540)], (588 ^ _362047) ^ [_380927] : [aElement0(_380927), 591 ^ _362047 : [(592 ^ _362047) ^ [_381064] : [-(isCountable0(sdtpldt0(_381064, _380927))), aSet0(_381064), isCountable0(_381064)]]], (602 ^ _362047) ^ [_381356] : [aElement0(_381356), 605 ^ _362047 : [(606 ^ _362047) ^ [_381493] : [-(isCountable0(sdtmndt0(_381493, _381356))), aSet0(_381493), isCountable0(_381493)]]], (616 ^ _362047) ^ [_381785] : [aElement0(_381785), 619 ^ _362047 : [(620 ^ _362047) ^ [_381922] : [-(isFinite0(sdtpldt0(_381922, _381785))), aSet0(_381922), isFinite0(_381922)]]], (630 ^ _362047) ^ [_382214] : [aElement0(_382214), 633 ^ _362047 : [(634 ^ _362047) ^ [_382351] : [-(isFinite0(sdtmndt0(_382351, _382214))), aSet0(_382351), isFinite0(_382351)]]], (644 ^ _362047) ^ [] : [-(aSet0(szNzAzT0))], (646 ^ _362047) ^ [] : [-(isCountable0(szNzAzT0))], (648 ^ _362047) ^ [] : [-(aElementOf0(sz00, szNzAzT0))], (650 ^ _362047) ^ [_382804] : [aElementOf0(_382804, szNzAzT0), 653 ^ _362047 : [(654 ^ _362047) ^ [] : [-(aElementOf0(szszuzczcdt0(_382804), szNzAzT0))], (656 ^ _362047) ^ [] : [szszuzczcdt0(_382804) = sz00]]], (658 ^ _362047) ^ [_383090, _383092] : [aElementOf0(_383092, szNzAzT0), aElementOf0(_383090, szNzAzT0), szszuzczcdt0(_383092) = szszuzczcdt0(_383090), -(_383092 = _383090)], (672 ^ _362047) ^ [_383474] : [aElementOf0(_383474, szNzAzT0), -(_383474 = sz00), 680 ^ _362047 : [(681 ^ _362047) ^ [] : [-(aElementOf0(679 ^ [_383474], szNzAzT0))], (683 ^ _362047) ^ [] : [-(_383474 = szszuzczcdt0(679 ^ [_383474]))]]], (685 ^ _362047) ^ [_383891] : [aElementOf0(_383891, szNzAzT0), _383891 = szszuzczcdt0(_383891)], (691 ^ _362047) ^ [_384100, _384102] : [aElementOf0(_384102, szNzAzT0), aElementOf0(_384100, szNzAzT0), sdtlseqdt0(_384102, _384100), true___, -(true___)], (709 ^ _362047) ^ [_384550] : [aElementOf0(_384550, szNzAzT0), -(sdtlseqdt0(sz00, _384550))], (715 ^ _362047) ^ [_384740] : [aElementOf0(_384740, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_384740), sz00)], (721 ^ _362047) ^ [_384949, _384951] : [aElementOf0(_384951, szNzAzT0), aElementOf0(_384949, szNzAzT0), 728 ^ _362047 : [(729 ^ _362047) ^ [] : [sdtlseqdt0(_384951, _384949), -(sdtlseqdt0(szszuzczcdt0(_384951), szszuzczcdt0(_384949)))], (735 ^ _362047) ^ [] : [sdtlseqdt0(szszuzczcdt0(_384951), szszuzczcdt0(_384949)), -(sdtlseqdt0(_384951, _384949))]]], (741 ^ _362047) ^ [_385498] : [aElementOf0(_385498, szNzAzT0), -(sdtlseqdt0(_385498, szszuzczcdt0(_385498)))], (747 ^ _362047) ^ [_385692] : [aElementOf0(_385692, szNzAzT0), -(sdtlseqdt0(_385692, _385692))], (753 ^ _362047) ^ [_385896, _385898] : [aElementOf0(_385898, szNzAzT0), aElementOf0(_385896, szNzAzT0), -(_385898 = _385896), sdtlseqdt0(_385898, _385896), sdtlseqdt0(_385896, _385898)], (771 ^ _362047) ^ [_386389, _386391, _386393] : [aElementOf0(_386393, szNzAzT0), aElementOf0(_386391, szNzAzT0), aElementOf0(_386389, szNzAzT0), -(sdtlseqdt0(_386393, _386389)), sdtlseqdt0(_386393, _386391), sdtlseqdt0(_386391, _386389)], (793 ^ _362047) ^ [_386981, _386983] : [aElementOf0(_386983, szNzAzT0), aElementOf0(_386981, szNzAzT0), -(sdtlseqdt0(_386983, _386981)), -(sdtlseqdt0(szszuzczcdt0(_386981), _386983))], (807 ^ _362047) ^ [_387376, _387378] : [aElementOf0(_387378, szNzAzT0), aElementOf0(_387376, szNzAzT0), iLess0(_387378, _387376), true___, -(true___)], (825 ^ _362047) ^ [_387826] : [aElementOf0(_387826, szNzAzT0), -(iLess0(_387826, szszuzczcdt0(_387826)))], (831 ^ _362047) ^ [_388020] : [aSet0(_388020), -(aElement0(sbrdtbr0(_388020)))], (837 ^ _362047) ^ [_388210] : [aSet0(_388210), 840 ^ _362047 : [(841 ^ _362047) ^ [] : [aElementOf0(sbrdtbr0(_388210), szNzAzT0), -(isFinite0(_388210))], (847 ^ _362047) ^ [] : [isFinite0(_388210), -(aElementOf0(sbrdtbr0(_388210), szNzAzT0))]]], (853 ^ _362047) ^ [_388641] : [aSet0(_388641), 856 ^ _362047 : [(857 ^ _362047) ^ [] : [sbrdtbr0(_388641) = sz00, -(_388641 = slcrc0)], (863 ^ _362047) ^ [] : [_388641 = slcrc0, -(sbrdtbr0(_388641) = sz00)]]], (869 ^ _362047) ^ [_389075] : [aSet0(_389075), isFinite0(_389075), 876 ^ _362047 : [(877 ^ _362047) ^ [_389305] : [aElement0(_389305), -(aElementOf0(_389305, _389075)), -(sbrdtbr0(sdtpldt0(_389075, _389305)) = szszuzczcdt0(sbrdtbr0(_389075)))]]], (887 ^ _362047) ^ [_389618] : [aSet0(_389618), 890 ^ _362047 : [(891 ^ _362047) ^ [_389763] : [-(szszuzczcdt0(sbrdtbr0(sdtmndt0(_389618, _389763))) = sbrdtbr0(_389618)), isFinite0(_389618), aElementOf0(_389763, _389618)]]], (901 ^ _362047) ^ [_390071] : [aSet0(_390071), 904 ^ _362047 : [(905 ^ _362047) ^ [_390211] : [-(sdtlseqdt0(sbrdtbr0(_390211), sbrdtbr0(_390071))), isFinite0(_390071), aSubsetOf0(_390211, _390071)]]], (915 ^ _362047) ^ [_390523, _390525] : [aSet0(_390525), aElementOf0(_390523, szNzAzT0), 931 ^ _362047 : [(932 ^ _362047) ^ [] : [-(aSubsetOf0(930 ^ [_390523, _390525], _390525))], (934 ^ _362047) ^ [] : [-(sbrdtbr0(930 ^ [_390523, _390525]) = _390523)]], isFinite0(_390525), sdtlseqdt0(_390523, sbrdtbr0(_390525))], (936 ^ _362047) ^ [_391139] : [aSubsetOf0(_391139, szNzAzT0), -(_391139 = slcrc0), 943 ^ _362047 : [(944 ^ _362047) ^ [_391408] : [_391408 = szmzizndt0(_391139), 947 ^ _362047 : [(948 ^ _362047) ^ [] : [-(aElementOf0(_391408, _391139))], (950 ^ _362047) ^ [_391623] : [aElementOf0(_391623, _391139), -(sdtlseqdt0(_391408, _391623))]]], (956 ^ _362047) ^ [_391802] : [-(_391802 = szmzizndt0(_391139)), aElementOf0(_391802, _391139), 962 ^ _362047 : [(963 ^ _362047) ^ [] : [-(aElementOf0(961 ^ [_391139, _391802], _391139))], (965 ^ _362047) ^ [] : [sdtlseqdt0(_391802, 961 ^ [_391139, _391802])]]]]], (969 ^ _362047) ^ [_392247] : [aSubsetOf0(_392247, szNzAzT0), isFinite0(_392247), -(_392247 = slcrc0), 980 ^ _362047 : [(981 ^ _362047) ^ [_392599] : [_392599 = szmzazxdt0(_392247), 984 ^ _362047 : [(985 ^ _362047) ^ [] : [-(aElementOf0(_392599, _392247))], (987 ^ _362047) ^ [_392814] : [aElementOf0(_392814, _392247), -(sdtlseqdt0(_392814, _392599))]]], (993 ^ _362047) ^ [_392993] : [-(_392993 = szmzazxdt0(_392247)), aElementOf0(_392993, _392247), 999 ^ _362047 : [(1000 ^ _362047) ^ [] : [-(aElementOf0(998 ^ [_392247, _392993], _392247))], (1002 ^ _362047) ^ [] : [sdtlseqdt0(998 ^ [_392247, _392993], _392993)]]]]], (1006 ^ _362047) ^ [_393454, _393456] : [-(szmzizndt0(_393456) = szmzizndt0(_393454)), aElementOf0(szmzizndt0(_393456), _393454), aElementOf0(szmzizndt0(_393454), _393456), aSubsetOf0(_393456, szNzAzT0), aSubsetOf0(_393454, szNzAzT0), -(_393456 = slcrc0), -(_393454 = slcrc0)], (1032 ^ _362047) ^ [_394121] : [aElementOf0(_394121, szNzAzT0), 1035 ^ _362047 : [(1060 ^ _362047) ^ [_395090] : [-(_395090 = slbdtrb0(_394121)), aSet0(_395090), 1076 ^ _362047 : [(1077 ^ _362047) ^ [] : [-(aElementOf0(1065 ^ [_394121, _395090], szNzAzT0))], (1079 ^ _362047) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(1065 ^ [_394121, _395090]), _394121))], (1081 ^ _362047) ^ [] : [aElementOf0(1065 ^ [_394121, _395090], _395090)]], 1068 ^ _362047 : [(1069 ^ _362047) ^ [] : [-(aElementOf0(1065 ^ [_394121, _395090], _395090))], (1071 ^ _362047) ^ [] : [aElementOf0(1065 ^ [_394121, _395090], szNzAzT0), sdtlseqdt0(szszuzczcdt0(1065 ^ [_394121, _395090]), _394121)]]], (1036 ^ _362047) ^ [_394309] : [_394309 = slbdtrb0(_394121), 1039 ^ _362047 : [(1040 ^ _362047) ^ [] : [-(aSet0(_394309))], (1042 ^ _362047) ^ [_394559] : [aElementOf0(_394559, _394309), 1045 ^ _362047 : [(1046 ^ _362047) ^ [] : [-(aElementOf0(_394559, szNzAzT0))], (1048 ^ _362047) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(_394559), _394121))]]], (1050 ^ _362047) ^ [_394812] : [-(aElementOf0(_394812, _394309)), aElementOf0(_394812, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_394812), _394121)]]]]], (1085 ^ _362047) ^ [_395893] : [aElementOf0(_395893, szNzAzT0), -(isFinite0(slbdtrb0(_395893)))], (1091 ^ _362047) ^ [] : [-(slbdtrb0(sz00) = slcrc0)], (1093 ^ _362047) ^ [_396152, _396154] : [aElementOf0(_396154, szNzAzT0), aElementOf0(_396152, szNzAzT0), 1100 ^ _362047 : [(1111 ^ _362047) ^ [] : [1112 ^ _362047 : [(1113 ^ _362047) ^ [] : [aElementOf0(_396154, slbdtrb0(_396152))], (1115 ^ _362047) ^ [] : [_396154 = _396152]], -(aElementOf0(_396154, slbdtrb0(szszuzczcdt0(_396152))))], (1101 ^ _362047) ^ [] : [aElementOf0(_396154, slbdtrb0(szszuzczcdt0(_396152))), -(aElementOf0(_396154, slbdtrb0(_396152))), -(_396154 = _396152)]]], (1119 ^ _362047) ^ [_396879, _396881] : [aElementOf0(_396881, szNzAzT0), aElementOf0(_396879, szNzAzT0), 1126 ^ _362047 : [(1127 ^ _362047) ^ [] : [sdtlseqdt0(_396881, _396879), -(aSubsetOf0(slbdtrb0(_396881), slbdtrb0(_396879)))], (1133 ^ _362047) ^ [] : [aSubsetOf0(slbdtrb0(_396881), slbdtrb0(_396879)), -(sdtlseqdt0(_396881, _396879))]]], (1139 ^ _362047) ^ [_397428] : [1147 ^ _362047 : [(1148 ^ _362047) ^ [] : [-(aElementOf0(1146 ^ [_397428], szNzAzT0))], (1150 ^ _362047) ^ [] : [-(aSubsetOf0(_397428, slbdtrb0(1146 ^ [_397428])))]], aSubsetOf0(_397428, szNzAzT0), isFinite0(_397428)], (1152 ^ _362047) ^ [_397842] : [aElementOf0(_397842, szNzAzT0), -(sbrdtbr0(slbdtrb0(_397842)) = _397842)], (1158 ^ _362047) ^ [_398054, _398056] : [aSet0(_398056), aElementOf0(_398054, szNzAzT0), 1165 ^ _362047 : [(1190 ^ _362047) ^ [_399147] : [-(_399147 = slbdtsldtrb0(_398056, _398054)), aSet0(_399147), 1206 ^ _362047 : [(1207 ^ _362047) ^ [] : [-(aSubsetOf0(1195 ^ [_398054, _398056, _399147], _398056))], (1209 ^ _362047) ^ [] : [-(sbrdtbr0(1195 ^ [_398054, _398056, _399147]) = _398054)], (1211 ^ _362047) ^ [] : [aElementOf0(1195 ^ [_398054, _398056, _399147], _399147)]], 1198 ^ _362047 : [(1199 ^ _362047) ^ [] : [-(aElementOf0(1195 ^ [_398054, _398056, _399147], _399147))], (1201 ^ _362047) ^ [] : [aSubsetOf0(1195 ^ [_398054, _398056, _399147], _398056), sbrdtbr0(1195 ^ [_398054, _398056, _399147]) = _398054]]], (1166 ^ _362047) ^ [_398334] : [_398334 = slbdtsldtrb0(_398056, _398054), 1169 ^ _362047 : [(1170 ^ _362047) ^ [] : [-(aSet0(_398334))], (1172 ^ _362047) ^ [_398594] : [aElementOf0(_398594, _398334), 1175 ^ _362047 : [(1176 ^ _362047) ^ [] : [-(aSubsetOf0(_398594, _398056))], (1178 ^ _362047) ^ [] : [-(sbrdtbr0(_398594) = _398054)]]], (1180 ^ _362047) ^ [_398857] : [-(aElementOf0(_398857, _398334)), aSubsetOf0(_398857, _398056), sbrdtbr0(_398857) = _398054]]]]], (1215 ^ _362047) ^ [_399996] : [aSet0(_399996), isFinite0(_399996), 1222 ^ _362047 : [(1223 ^ _362047) ^ [_400212] : [aElementOf0(_400212, szNzAzT0), -(isFinite0(slbdtsldtrb0(_399996, _400212)))]]], (1229 ^ _362047) ^ [_400421] : [aSet0(_400421), -(isFinite0(_400421)), 1236 ^ _362047 : [(1237 ^ _362047) ^ [_400643] : [aElementOf0(_400643, szNzAzT0), slbdtsldtrb0(_400421, _400643) = slcrc0]]], (1243 ^ _362047) ^ [_400855] : [aSet0(_400855), isCountable0(_400855), 1250 ^ _362047 : [(1251 ^ _362047) ^ [_401079] : [-(isCountable0(slbdtsldtrb0(_400855, _401079))), aElementOf0(_401079, szNzAzT0), -(_401079 = sz00)]]], (1261 ^ _362047) ^ [_401380] : [aElementOf0(_401380, szNzAzT0), 1264 ^ _362047 : [(1265 ^ _362047) ^ [_401567, _401569] : [aSet0(_401569), aSet0(_401567), -(_401380 = sz00), -(aSubsetOf0(_401569, _401567)), aSubsetOf0(slbdtsldtrb0(_401569, _401380), slbdtsldtrb0(_401567, _401380)), -(slbdtsldtrb0(_401569, _401380) = slcrc0)]]], (1287 ^ _362047) ^ [_402186, _402188] : [aSet0(_402188), aElementOf0(_402186, szNzAzT0), 1294 ^ _362047 : [(1295 ^ _362047) ^ [_402437] : [1303 ^ _362047 : [(1304 ^ _362047) ^ [] : [-(aSubsetOf0(1302 ^ [_402186, _402188, _402437], _402188))], (1306 ^ _362047) ^ [] : [-(isFinite0(1302 ^ [_402186, _402188, _402437]))], (1308 ^ _362047) ^ [] : [-(aSubsetOf0(_402437, slbdtsldtrb0(1302 ^ [_402186, _402188, _402437], _402186)))]], aSubsetOf0(_402437, slbdtsldtrb0(_402188, _402186)), isFinite0(_402437)]]], (1310 ^ _362047) ^ [_402999] : [aFunction0(_402999), true___, -(true___)], (1320 ^ _362047) ^ [_403254] : [aFunction0(_403254), -(aSet0(szDzozmdt0(_403254)))], (1326 ^ _362047) ^ [_403444] : [aFunction0(_403444), 1329 ^ _362047 : [(1330 ^ _362047) ^ [_403579] : [aElementOf0(_403579, szDzozmdt0(_403444)), -(aElement0(sdtlpdtrp0(_403444, _403579)))]]], (1336 ^ _362047) ^ [_403804, _403806] : [aFunction0(_403806), aElement0(_403804), 1343 ^ _362047 : [(1368 ^ _362047) ^ [_404913] : [-(_404913 = sdtlbdtrb0(_403806, _403804)), aSet0(_404913), 1384 ^ _362047 : [(1385 ^ _362047) ^ [] : [-(aElementOf0(1373 ^ [_403804, _403806, _404913], szDzozmdt0(_403806)))], (1387 ^ _362047) ^ [] : [-(sdtlpdtrp0(_403806, 1373 ^ [_403804, _403806, _404913]) = _403804)], (1389 ^ _362047) ^ [] : [aElementOf0(1373 ^ [_403804, _403806, _404913], _404913)]], 1376 ^ _362047 : [(1377 ^ _362047) ^ [] : [-(aElementOf0(1373 ^ [_403804, _403806, _404913], _404913))], (1379 ^ _362047) ^ [] : [aElementOf0(1373 ^ [_403804, _403806, _404913], szDzozmdt0(_403806)), sdtlpdtrp0(_403806, 1373 ^ [_403804, _403806, _404913]) = _403804]]], (1344 ^ _362047) ^ [_404085] : [_404085 = sdtlbdtrb0(_403806, _403804), 1347 ^ _362047 : [(1348 ^ _362047) ^ [] : [-(aSet0(_404085))], (1350 ^ _362047) ^ [_404348] : [aElementOf0(_404348, _404085), 1353 ^ _362047 : [(1354 ^ _362047) ^ [] : [-(aElementOf0(_404348, szDzozmdt0(_403806)))], (1356 ^ _362047) ^ [] : [-(sdtlpdtrp0(_403806, _404348) = _403804)]]], (1358 ^ _362047) ^ [_404617] : [-(aElementOf0(_404617, _404085)), aElementOf0(_404617, szDzozmdt0(_403806)), sdtlpdtrp0(_403806, _404617) = _403804]]]]], (1393 ^ _362047) ^ [_405788, _405790] : [-(aSubsetOf0(sdtlbdtrb0(_405790, _405788), szDzozmdt0(_405790))), aFunction0(_405790), aElement0(_405788)], (1403 ^ _362047) ^ [_406079] : [aFunction0(_406079), 1406 ^ _362047 : [(1407 ^ _362047) ^ [_406256] : [aSubsetOf0(_406256, szDzozmdt0(_406079)), 1410 ^ _362047 : [(1436 ^ _362047) ^ [_407443] : [-(_407443 = sdtlcdtrc0(_406079, _406256)), aSet0(_407443), 1453 ^ _362047 : [(1454 ^ _362047) ^ [] : [-(aElementOf0(1452 ^ [_406079, _406256, _407443], _406256))], (1456 ^ _362047) ^ [] : [-(sdtlpdtrp0(_406079, 1452 ^ [_406079, _406256, _407443]) = 1441 ^ [_406079, _406256, _407443])], (1458 ^ _362047) ^ [] : [aElementOf0(1441 ^ [_406079, _406256, _407443], _407443)]], 1444 ^ _362047 : [(1445 ^ _362047) ^ [] : [-(aElementOf0(1441 ^ [_406079, _406256, _407443], _407443))], (1447 ^ _362047) ^ [_407836] : [aElementOf0(_407836, _406256), sdtlpdtrp0(_406079, _407836) = 1441 ^ [_406079, _406256, _407443]]]], (1411 ^ _362047) ^ [_406461] : [_406461 = sdtlcdtrc0(_406079, _406256), 1414 ^ _362047 : [(1415 ^ _362047) ^ [] : [-(aSet0(_406461))], (1417 ^ _362047) ^ [_406727] : [aElementOf0(_406727, _406461), 1421 ^ _362047 : [(1422 ^ _362047) ^ [] : [-(aElementOf0(1420 ^ [_406079, _406256, _406461, _406727], _406256))], (1424 ^ _362047) ^ [] : [-(sdtlpdtrp0(_406079, 1420 ^ [_406079, _406256, _406461, _406727]) = _406727)]]], (1426 ^ _362047) ^ [_407081] : [-(aElementOf0(_407081, _406461)), 1427 ^ _362047 : [(1428 ^ _362047) ^ [_407186] : [aElementOf0(_407186, _406256), sdtlpdtrp0(_406079, _407186) = _407081]]]]]]]]], (1462 ^ _362047) ^ [_408447] : [aFunction0(_408447), 1465 ^ _362047 : [(1466 ^ _362047) ^ [_408588] : [aElementOf0(_408588, szDzozmdt0(_408447)), -(aElementOf0(sdtlpdtrp0(_408447, _408588), sdtlcdtrc0(_408447, szDzozmdt0(_408447))))]]], (1472 ^ _362047) ^ [_408811] : [aFunction0(_408811), 1475 ^ _362047 : [(1476 ^ _362047) ^ [_408988] : [aSubsetOf0(_408988, szDzozmdt0(_408811)), 1479 ^ _362047 : [(1480 ^ _362047) ^ [_409193] : [_409193 = sdtexdt0(_408811, _408988), 1483 ^ _362047 : [(1484 ^ _362047) ^ [] : [-(aFunction0(_409193))], (1486 ^ _362047) ^ [] : [-(szDzozmdt0(_409193) = _408988)], (1488 ^ _362047) ^ [_409500] : [aElementOf0(_409500, _408988), -(sdtlpdtrp0(_409193, _409500) = sdtlpdtrp0(_408811, _409500))]]], (1494 ^ _362047) ^ [_409701] : [-(_409701 = sdtexdt0(_408811, _408988)), aFunction0(_409701), szDzozmdt0(_409701) = _408988, 1504 ^ _362047 : [(1505 ^ _362047) ^ [] : [-(aElementOf0(1503 ^ [_408811, _408988, _409701], _408988))], (1507 ^ _362047) ^ [] : [sdtlpdtrp0(_409701, 1503 ^ [_408811, _408988, _409701]) = sdtlpdtrp0(_408811, 1503 ^ [_408811, _408988, _409701])]]]]]]], (1511 ^ _362047) ^ [_410295] : [aFunction0(_410295), 1514 ^ _362047 : [(1515 ^ _362047) ^ [_410483] : [aSubsetOf0(_410483, szDzozmdt0(_410295)), isCountable0(_410483), 1526 ^ _362047 : [(1527 ^ _362047) ^ [] : [-(aElementOf0(1524 ^ [_410295, _410483], szDzozmdt0(_410295)))], (1529 ^ _362047) ^ [] : [-(aElementOf0(1525 ^ [_410295, _410483], szDzozmdt0(_410295)))], (1531 ^ _362047) ^ [] : [1524 ^ [_410295, _410483] = 1525 ^ [_410295, _410483]], (1533 ^ _362047) ^ [] : [-(sdtlpdtrp0(_410295, 1524 ^ [_410295, _410483]) = sdtlpdtrp0(_410295, 1525 ^ [_410295, _410483]))]], -(isCountable0(sdtlcdtrc0(_410295, _410483)))]]], (1537 ^ _362047) ^ [_411355] : [aFunction0(_411355), 1548 ^ _362047 : [(1549 ^ _362047) ^ [] : [-(aElement0(szDzizrdt0(_411355)))], (1551 ^ _362047) ^ [] : [-(isCountable0(sdtlbdtrb0(_411355, szDzizrdt0(_411355))))]], isCountable0(szDzozmdt0(_411355)), isFinite0(sdtlcdtrc0(_411355, szDzozmdt0(_411355)))], (1553 ^ _362047) ^ [] : [-(aSet0(xT))], (1555 ^ _362047) ^ [] : [-(isFinite0(xT))], (1557 ^ _362047) ^ [] : [-(aElementOf0(xK, szNzAzT0))], (1559 ^ _362047) ^ [] : [-(aSet0(xS))], (1567 ^ _362047) ^ [] : [-(aSubsetOf0(xS, szNzAzT0))], (1569 ^ _362047) ^ [] : [-(isCountable0(xS))], (1561 ^ _362047) ^ [_412040] : [aElementOf0(_412040, xS), -(aElementOf0(_412040, szNzAzT0))], (1571 ^ _362047) ^ [] : [-(aFunction0(xc))], (1573 ^ _362047) ^ [_412417] : [aElementOf0(_412417, szDzozmdt0(xc)), 1576 ^ _362047 : [(1577 ^ _362047) ^ [] : [-(aSet0(_412417))], (1585 ^ _362047) ^ [] : [-(aSubsetOf0(_412417, xS))], (1587 ^ _362047) ^ [] : [-(sbrdtbr0(_412417) = xK)], (1579 ^ _362047) ^ [_412652] : [aElementOf0(_412652, _412417), -(aElementOf0(_412652, xS))]]], (1589 ^ _362047) ^ [_412939] : [-(aElementOf0(_412939, szDzozmdt0(xc))), sbrdtbr0(_412939) = xK, 1592 ^ _362047 : [(1602 ^ _362047) ^ [] : [aSubsetOf0(_412939, xS)], (1593 ^ _362047) ^ [] : [aSet0(_412939), 1597 ^ _362047 : [(1598 ^ _362047) ^ [] : [-(aElementOf0(1596 ^ [_412939], _412939))], (1600 ^ _362047) ^ [] : [aElementOf0(1596 ^ [_412939], xS)]]]]], (1608 ^ _362047) ^ [] : [-(szDzozmdt0(xc) = slbdtsldtrb0(xS, xK))], (1610 ^ _362047) ^ [] : [-(aSet0(sdtlcdtrc0(xc, szDzozmdt0(xc))))], (1637 ^ _362047) ^ [] : [-(aSubsetOf0(sdtlcdtrc0(xc, szDzozmdt0(xc)), xT))], (1631 ^ _362047) ^ [_414292] : [aElementOf0(_414292, sdtlcdtrc0(xc, szDzozmdt0(xc))), -(aElementOf0(_414292, xT))], (1612 ^ _362047) ^ [_413645] : [aElementOf0(_413645, sdtlcdtrc0(xc, szDzozmdt0(xc))), 1616 ^ _362047 : [(1617 ^ _362047) ^ [] : [-(aElementOf0(1615 ^ [_413645], szDzozmdt0(xc)))], (1619 ^ _362047) ^ [] : [-(sdtlpdtrp0(xc, 1615 ^ [_413645]) = _413645)]]], (1621 ^ _362047) ^ [_413945] : [-(aElementOf0(_413945, sdtlcdtrc0(xc, szDzozmdt0(xc)))), 1622 ^ _362047 : [(1623 ^ _362047) ^ [_414038] : [aElementOf0(_414038, szDzozmdt0(xc)), sdtlpdtrp0(xc, _414038) = _413945]]], (1639 ^ _362047) ^ [_414531] : [aElementOf0(_414531, szNzAzT0), 1642 ^ _362047 : [(1643 ^ _362047) ^ [_414994] : [isCountable0(_414994), 1646 ^ _362047 : [(1656 ^ _362047) ^ [] : [aSubsetOf0(_414994, szNzAzT0)], (1647 ^ _362047) ^ [] : [aSet0(_414994), 1651 ^ _362047 : [(1652 ^ _362047) ^ [] : [-(aElementOf0(1650 ^ [_414531, _414994], _414994))], (1654 ^ _362047) ^ [] : [aElementOf0(1650 ^ [_414531, _414994], szNzAzT0)]]]], 1659 ^ _362047 : [(1660 ^ _362047) ^ [_415818] : [iLess0(_414531, xK), 1736 ^ _362047 : [(1737 ^ _362047) ^ [] : [-(aElementOf0(1735 ^ [_414531, _414994, _415818], xT))], (1740 ^ _362047) ^ [] : [-(aSet0(1738 ^ [_414531, _414994, _415818]))], (1742 ^ _362047) ^ [_419372] : [aElementOf0(_419372, 1738 ^ [_414531, _414994, _415818]), -(aElementOf0(_419372, _414994))], (1748 ^ _362047) ^ [] : [-(aSubsetOf0(1738 ^ [_414531, _414994, _415818], _414994))], (1750 ^ _362047) ^ [] : [-(isCountable0(1738 ^ [_414531, _414994, _415818]))], (1752 ^ _362047) ^ [_419737] : [-(sdtlpdtrp0(_415818, _419737) = 1735 ^ [_414531, _414994, _415818]), 1753 ^ _362047 : [(1769 ^ _362047) ^ [] : [aElementOf0(_419737, slbdtsldtrb0(1738 ^ [_414531, _414994, _415818], _414531))], (1754 ^ _362047) ^ [] : [sbrdtbr0(_419737) = _414531, 1755 ^ _362047 : [(1765 ^ _362047) ^ [] : [aSubsetOf0(_419737, 1738 ^ [_414531, _414994, _415818])], (1756 ^ _362047) ^ [] : [aSet0(_419737), 1760 ^ _362047 : [(1761 ^ _362047) ^ [] : [-(aElementOf0(1759 ^ [_414531, _414994, _415818, _419737], _419737))], (1763 ^ _362047) ^ [] : [aElementOf0(1759 ^ [_414531, _414994, _415818, _419737], 1738 ^ [_414531, _414994, _415818])]]]]]]]], aFunction0(_415818), 1668 ^ _362047 : [(1702 ^ _362047) ^ [] : [szDzozmdt0(_415818) = slbdtsldtrb0(_414994, _414531)], (1669 ^ _362047) ^ [] : [1687 ^ _362047 : [(1700 ^ _362047) ^ [] : [aElementOf0(1667 ^ [_414531, _414994, _415818], szDzozmdt0(_415818))], (1688 ^ _362047) ^ [] : [-(aSet0(1667 ^ [_414531, _414994, _415818]))], (1696 ^ _362047) ^ [] : [-(aSubsetOf0(1667 ^ [_414531, _414994, _415818], _414994))], (1698 ^ _362047) ^ [] : [-(sbrdtbr0(1667 ^ [_414531, _414994, _415818]) = _414531)], (1690 ^ _362047) ^ [_417180] : [aElementOf0(_417180, 1667 ^ [_414531, _414994, _415818]), -(aElementOf0(_417180, _414994))]], 1670 ^ _362047 : [(1671 ^ _362047) ^ [] : [-(aElementOf0(1667 ^ [_414531, _414994, _415818], szDzozmdt0(_415818)))], (1673 ^ _362047) ^ [] : [sbrdtbr0(1667 ^ [_414531, _414994, _415818]) = _414531, 1674 ^ _362047 : [(1684 ^ _362047) ^ [] : [aSubsetOf0(1667 ^ [_414531, _414994, _415818], _414994)], (1675 ^ _362047) ^ [] : [aSet0(1667 ^ [_414531, _414994, _415818]), 1679 ^ _362047 : [(1680 ^ _362047) ^ [] : [-(aElementOf0(1678 ^ [_414531, _414994, _415818], 1667 ^ [_414531, _414994, _415818]))], (1682 ^ _362047) ^ [] : [aElementOf0(1678 ^ [_414531, _414994, _415818], _414994)]]]]]]]], 1703 ^ _362047 : [(1726 ^ _362047) ^ [] : [-(aElementOf0(1724 ^ [_414531, _414994, _415818], sdtlcdtrc0(_415818, szDzozmdt0(_415818))))], (1728 ^ _362047) ^ [] : [aElementOf0(1724 ^ [_414531, _414994, _415818], xT)], (1730 ^ _362047) ^ [] : [aSubsetOf0(sdtlcdtrc0(_415818, szDzozmdt0(_415818)), xT)], (1704 ^ _362047) ^ [] : [-(aSet0(sdtlcdtrc0(_415818, szDzozmdt0(_415818))))], (1706 ^ _362047) ^ [_417777] : [aElementOf0(_417777, sdtlcdtrc0(_415818, szDzozmdt0(_415818))), 1710 ^ _362047 : [(1711 ^ _362047) ^ [] : [-(aElementOf0(1709 ^ [_414531, _414994, _415818, _417777], szDzozmdt0(_415818)))], (1713 ^ _362047) ^ [] : [-(sdtlpdtrp0(_415818, 1709 ^ [_414531, _414994, _415818, _417777]) = _417777)]]], (1715 ^ _362047) ^ [_418147] : [-(aElementOf0(_418147, sdtlcdtrc0(_415818, szDzozmdt0(_415818)))), 1716 ^ _362047 : [(1717 ^ _362047) ^ [_418259] : [aElementOf0(_418259, szDzozmdt0(_415818)), sdtlpdtrp0(_415818, _418259) = _418147]]]]]]]]], (1773 ^ _362047) ^ [] : [xK = sz00], (1775 ^ _362047) ^ [] : [xK = sz00], (1777 ^ _362047) ^ [] : [-(aElementOf0(xk, szNzAzT0))], (1779 ^ _362047) ^ [] : [-(szszuzczcdt0(xk) = xK)], (1781 ^ _362047) ^ [] : [-(aFunction0(xN))], (1783 ^ _362047) ^ [] : [-(szDzozmdt0(xN) = szNzAzT0)], (1785 ^ _362047) ^ [] : [-(sdtlpdtrp0(xN, sz00) = xS)], (1787 ^ _362047) ^ [_420965] : [aElementOf0(_420965, szNzAzT0), isCountable0(sdtlpdtrp0(xN, _420965)), 1794 ^ _362047 : [(1804 ^ _362047) ^ [] : [aSubsetOf0(sdtlpdtrp0(xN, _420965), szNzAzT0)], (1795 ^ _362047) ^ [] : [aSet0(sdtlpdtrp0(xN, _420965)), 1799 ^ _362047 : [(1800 ^ _362047) ^ [] : [-(aElementOf0(1798 ^ [_420965], sdtlpdtrp0(xN, _420965)))], (1802 ^ _362047) ^ [] : [aElementOf0(1798 ^ [_420965], szNzAzT0)]]]], 1807 ^ _362047 : [(1808 ^ _362047) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _420965)), sdtlpdtrp0(xN, _420965)))], (1810 ^ _362047) ^ [_421833] : [aElementOf0(_421833, sdtlpdtrp0(xN, _420965)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _420965)), _421833))], (1816 ^ _362047) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _420965), szmzizndt0(sdtlpdtrp0(xN, _420965)))))], (1842 ^ _362047) ^ [] : [-(aSet0(sdtlpdtrp0(xN, szszuzczcdt0(_420965))))], (1850 ^ _362047) ^ [] : [-(aSubsetOf0(sdtlpdtrp0(xN, szszuzczcdt0(_420965)), sdtmndt0(sdtlpdtrp0(xN, _420965), szmzizndt0(sdtlpdtrp0(xN, _420965)))))], (1852 ^ _362047) ^ [] : [-(isCountable0(sdtlpdtrp0(xN, szszuzczcdt0(_420965))))], (1844 ^ _362047) ^ [_422985] : [aElementOf0(_422985, sdtlpdtrp0(xN, szszuzczcdt0(_420965))), -(aElementOf0(_422985, sdtmndt0(sdtlpdtrp0(xN, _420965), szmzizndt0(sdtlpdtrp0(xN, _420965)))))], (1818 ^ _362047) ^ [_422150] : [aElementOf0(_422150, sdtmndt0(sdtlpdtrp0(xN, _420965), szmzizndt0(sdtlpdtrp0(xN, _420965)))), 1821 ^ _362047 : [(1822 ^ _362047) ^ [] : [-(aElement0(_422150))], (1824 ^ _362047) ^ [] : [-(aElementOf0(_422150, sdtlpdtrp0(xN, _420965)))], (1826 ^ _362047) ^ [] : [_422150 = szmzizndt0(sdtlpdtrp0(xN, _420965))]]], (1828 ^ _362047) ^ [_422500] : [-(aElementOf0(_422500, sdtmndt0(sdtlpdtrp0(xN, _420965), szmzizndt0(sdtlpdtrp0(xN, _420965))))), aElement0(_422500), aElementOf0(_422500, sdtlpdtrp0(xN, _420965)), -(_422500 = szmzizndt0(sdtlpdtrp0(xN, _420965)))]]], (1854 ^ _362047) ^ [_423382] : [aElementOf0(_423382, szNzAzT0), 1857 ^ _362047 : [(1858 ^ _362047) ^ [] : [-(aSet0(sdtlpdtrp0(xN, _423382)))], (1866 ^ _362047) ^ [] : [-(aSubsetOf0(sdtlpdtrp0(xN, _423382), szNzAzT0))], (1868 ^ _362047) ^ [] : [-(isCountable0(sdtlpdtrp0(xN, _423382)))], (1860 ^ _362047) ^ [_423629] : [aElementOf0(_423629, sdtlpdtrp0(xN, _423382)), -(aElementOf0(_423629, szNzAzT0))]]], (1870 ^ _362047) ^ [_423973, _423975] : [aElementOf0(_423975, szNzAzT0), aElementOf0(_423973, szNzAzT0), sdtlseqdt0(_423973, _423975), 1881 ^ _362047 : [(1888 ^ _362047) ^ [] : [-(aSubsetOf0(sdtlpdtrp0(xN, _423975), sdtlpdtrp0(xN, _423973)))], (1882 ^ _362047) ^ [_424322] : [aElementOf0(_424322, sdtlpdtrp0(xN, _423975)), -(aElementOf0(_424322, sdtlpdtrp0(xN, _423973)))]]], (1890 ^ _362047) ^ [_424619, _424621] : [aElementOf0(_424621, szNzAzT0), aElementOf0(_424619, szNzAzT0), -(_424621 = _424619), 1901 ^ _362047 : [(1902 ^ _362047) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _424621)), sdtlpdtrp0(xN, _424621)))], (1904 ^ _362047) ^ [_425110] : [aElementOf0(_425110, sdtlpdtrp0(xN, _424621)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _424621)), _425110))], (1919 ^ _362047) ^ [] : [szmzizndt0(sdtlpdtrp0(xN, _424621)) = szmzizndt0(sdtlpdtrp0(xN, _424619))], (1910 ^ _362047) ^ [] : [aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _424621)), sdtlpdtrp0(xN, _424619)), 1914 ^ _362047 : [(1915 ^ _362047) ^ [] : [-(aElementOf0(1913 ^ [_424619, _424621], sdtlpdtrp0(xN, _424619)))], (1917 ^ _362047) ^ [] : [sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _424621)), 1913 ^ [_424619, _424621])]]]]], (1921 ^ _362047) ^ [_425710] : [aElementOf0(_425710, szNzAzT0), 1924 ^ _362047 : [(1925 ^ _362047) ^ [_426175] : [aSet0(_426175), 1930 ^ _362047 : [(1931 ^ _362047) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _425710)), sdtlpdtrp0(xN, _425710)))], (1933 ^ _362047) ^ [_426762] : [aElementOf0(_426762, sdtlpdtrp0(xN, _425710)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _425710)), _426762))], (1976 ^ _362047) ^ [] : [aElementOf0(_426175, slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _425710), szmzizndt0(sdtlpdtrp0(xN, _425710))), xk))], (1965 ^ _362047) ^ [] : [1967 ^ _362047 : [(1968 ^ _362047) ^ [] : [-(aElementOf0(1966 ^ [_425710, _426175], _426175))], (1970 ^ _362047) ^ [] : [aElementOf0(1966 ^ [_425710, _426175], sdtmndt0(sdtlpdtrp0(xN, _425710), szmzizndt0(sdtlpdtrp0(xN, _425710))))], (1972 ^ _362047) ^ [] : [aSubsetOf0(_426175, sdtmndt0(sdtlpdtrp0(xN, _425710), szmzizndt0(sdtlpdtrp0(xN, _425710))))]], sbrdtbr0(_426175) = xk], (1939 ^ _362047) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _425710), szmzizndt0(sdtlpdtrp0(xN, _425710)))))], (1941 ^ _362047) ^ [_427091] : [aElementOf0(_427091, sdtmndt0(sdtlpdtrp0(xN, _425710), szmzizndt0(sdtlpdtrp0(xN, _425710)))), 1944 ^ _362047 : [(1945 ^ _362047) ^ [] : [-(aElement0(_427091))], (1947 ^ _362047) ^ [] : [-(aElementOf0(_427091, sdtlpdtrp0(xN, _425710)))], (1949 ^ _362047) ^ [] : [_427091 = szmzizndt0(sdtlpdtrp0(xN, _425710))]]], (1951 ^ _362047) ^ [_427453] : [-(aElementOf0(_427453, sdtmndt0(sdtlpdtrp0(xN, _425710), szmzizndt0(sdtlpdtrp0(xN, _425710))))), aElement0(_427453), aElementOf0(_427453, sdtlpdtrp0(xN, _425710)), -(_427453 = szmzizndt0(sdtlpdtrp0(xN, _425710)))]], 1977 ^ _362047 : [(1978 ^ _362047) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _425710)), sdtlpdtrp0(xN, _425710)))], (1980 ^ _362047) ^ [_428422] : [aElementOf0(_428422, sdtlpdtrp0(xN, _425710)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _425710)), _428422))], (1986 ^ _362047) ^ [] : [-(aSet0(sdtpldt0(_426175, szmzizndt0(sdtlpdtrp0(xN, _425710)))))], (2018 ^ _362047) ^ [] : [-(aSubsetOf0(sdtpldt0(_426175, szmzizndt0(sdtlpdtrp0(xN, _425710))), xS))], (2020 ^ _362047) ^ [] : [-(sbrdtbr0(sdtpldt0(_426175, szmzizndt0(sdtlpdtrp0(xN, _425710)))) = xK)], (2022 ^ _362047) ^ [] : [-(aElementOf0(sdtpldt0(_426175, szmzizndt0(sdtlpdtrp0(xN, _425710))), slbdtsldtrb0(xS, xK)))], (2012 ^ _362047) ^ [_429514] : [aElementOf0(_429514, sdtpldt0(_426175, szmzizndt0(sdtlpdtrp0(xN, _425710)))), -(aElementOf0(_429514, xS))], (1988 ^ _362047) ^ [_428746] : [aElementOf0(_428746, sdtpldt0(_426175, szmzizndt0(sdtlpdtrp0(xN, _425710)))), 1991 ^ _362047 : [(1992 ^ _362047) ^ [] : [-(aElement0(_428746))], (1994 ^ _362047) ^ [] : [-(aElementOf0(_428746, _426175)), -(_428746 = szmzizndt0(sdtlpdtrp0(xN, _425710)))]]], (2000 ^ _362047) ^ [_429113] : [-(aElementOf0(_429113, sdtpldt0(_426175, szmzizndt0(sdtlpdtrp0(xN, _425710))))), aElement0(_429113), 2005 ^ _362047 : [(2006 ^ _362047) ^ [] : [aElementOf0(_429113, _426175)], (2008 ^ _362047) ^ [] : [_429113 = szmzizndt0(sdtlpdtrp0(xN, _425710))]]]]]]], (2024 ^ _362047) ^ [] : [-(aFunction0(xC))], (2026 ^ _362047) ^ [] : [-(szDzozmdt0(xC) = szNzAzT0)], (2028 ^ _362047) ^ [_430082] : [aElementOf0(_430082, szNzAzT0), 2031 ^ _362047 : [(2032 ^ _362047) ^ [] : [-(aFunction0(sdtlpdtrp0(xC, _430082)))], (2034 ^ _362047) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _430082)), sdtlpdtrp0(xN, _430082)))], (2036 ^ _362047) ^ [_430926] : [aElementOf0(_430926, sdtlpdtrp0(xN, _430082)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _430082)), _430926))], (2042 ^ _362047) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _430082), szmzizndt0(sdtlpdtrp0(xN, _430082)))))], (2044 ^ _362047) ^ [_431243] : [aElementOf0(_431243, sdtmndt0(sdtlpdtrp0(xN, _430082), szmzizndt0(sdtlpdtrp0(xN, _430082)))), 2047 ^ _362047 : [(2048 ^ _362047) ^ [] : [-(aElement0(_431243))], (2050 ^ _362047) ^ [] : [-(aElementOf0(_431243, sdtlpdtrp0(xN, _430082)))], (2052 ^ _362047) ^ [] : [_431243 = szmzizndt0(sdtlpdtrp0(xN, _430082))]]], (2054 ^ _362047) ^ [_431593] : [-(aElementOf0(_431593, sdtmndt0(sdtlpdtrp0(xN, _430082), szmzizndt0(sdtlpdtrp0(xN, _430082))))), aElement0(_431593), aElementOf0(_431593, sdtlpdtrp0(xN, _430082)), -(_431593 = szmzizndt0(sdtlpdtrp0(xN, _430082)))], (2068 ^ _362047) ^ [_432030] : [aElementOf0(_432030, szDzozmdt0(sdtlpdtrp0(xC, _430082))), 2071 ^ _362047 : [(2072 ^ _362047) ^ [] : [-(aSet0(_432030))], (2080 ^ _362047) ^ [] : [-(aSubsetOf0(_432030, sdtmndt0(sdtlpdtrp0(xN, _430082), szmzizndt0(sdtlpdtrp0(xN, _430082)))))], (2082 ^ _362047) ^ [] : [-(sbrdtbr0(_432030) = xk)], (2074 ^ _362047) ^ [_432305] : [aElementOf0(_432305, _432030), -(aElementOf0(_432305, sdtmndt0(sdtlpdtrp0(xN, _430082), szmzizndt0(sdtlpdtrp0(xN, _430082)))))]]], (2084 ^ _362047) ^ [_432637] : [-(aElementOf0(_432637, szDzozmdt0(sdtlpdtrp0(xC, _430082)))), sbrdtbr0(_432637) = xk, 2087 ^ _362047 : [(2097 ^ _362047) ^ [] : [aSubsetOf0(_432637, sdtmndt0(sdtlpdtrp0(xN, _430082), szmzizndt0(sdtlpdtrp0(xN, _430082))))], (2088 ^ _362047) ^ [] : [aSet0(_432637), 2092 ^ _362047 : [(2093 ^ _362047) ^ [] : [-(aElementOf0(2091 ^ [_430082, _432637], _432637))], (2095 ^ _362047) ^ [] : [aElementOf0(2091 ^ [_430082, _432637], sdtmndt0(sdtlpdtrp0(xN, _430082), szmzizndt0(sdtlpdtrp0(xN, _430082))))]]]]], (2103 ^ _362047) ^ [] : [-(szDzozmdt0(sdtlpdtrp0(xC, _430082)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _430082), szmzizndt0(sdtlpdtrp0(xN, _430082))), xk))], (2105 ^ _362047) ^ [_433364] : [2157 ^ _362047 : [(2158 ^ _362047) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _430082)), sdtlpdtrp0(xN, _430082)))], (2160 ^ _362047) ^ [_435552] : [aElementOf0(_435552, sdtlpdtrp0(xN, _430082)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _430082)), _435552))], (2190 ^ _362047) ^ [] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _430082), _433364) = sdtlpdtrp0(xc, sdtpldt0(_433364, szmzizndt0(sdtlpdtrp0(xN, _430082)))))], (2166 ^ _362047) ^ [_435803] : [aElementOf0(_435803, sdtpldt0(_433364, szmzizndt0(sdtlpdtrp0(xN, _430082)))), 2169 ^ _362047 : [(2170 ^ _362047) ^ [] : [-(aElement0(_435803))], (2172 ^ _362047) ^ [] : [-(aElementOf0(_435803, _433364)), -(_435803 = szmzizndt0(sdtlpdtrp0(xN, _430082)))]]], (2178 ^ _362047) ^ [_436170] : [-(aElementOf0(_436170, sdtpldt0(_433364, szmzizndt0(sdtlpdtrp0(xN, _430082))))), aElement0(_436170), 2183 ^ _362047 : [(2184 ^ _362047) ^ [] : [aElementOf0(_436170, _433364)], (2186 ^ _362047) ^ [] : [_436170 = szmzizndt0(sdtlpdtrp0(xN, _430082))]]]], aSet0(_433364), 2110 ^ _362047 : [(2111 ^ _362047) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _430082)), sdtlpdtrp0(xN, _430082)))], (2113 ^ _362047) ^ [_433892] : [aElementOf0(_433892, sdtlpdtrp0(xN, _430082)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _430082)), _433892))], (2156 ^ _362047) ^ [] : [aElementOf0(_433364, slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _430082), szmzizndt0(sdtlpdtrp0(xN, _430082))), xk))], (2145 ^ _362047) ^ [] : [2147 ^ _362047 : [(2148 ^ _362047) ^ [] : [-(aElementOf0(2146 ^ [_430082, _433364], _433364))], (2150 ^ _362047) ^ [] : [aElementOf0(2146 ^ [_430082, _433364], sdtmndt0(sdtlpdtrp0(xN, _430082), szmzizndt0(sdtlpdtrp0(xN, _430082))))], (2152 ^ _362047) ^ [] : [aSubsetOf0(_433364, sdtmndt0(sdtlpdtrp0(xN, _430082), szmzizndt0(sdtlpdtrp0(xN, _430082))))]], sbrdtbr0(_433364) = xk], (2119 ^ _362047) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _430082), szmzizndt0(sdtlpdtrp0(xN, _430082)))))], (2121 ^ _362047) ^ [_434221] : [aElementOf0(_434221, sdtmndt0(sdtlpdtrp0(xN, _430082), szmzizndt0(sdtlpdtrp0(xN, _430082)))), 2124 ^ _362047 : [(2125 ^ _362047) ^ [] : [-(aElement0(_434221))], (2127 ^ _362047) ^ [] : [-(aElementOf0(_434221, sdtlpdtrp0(xN, _430082)))], (2129 ^ _362047) ^ [] : [_434221 = szmzizndt0(sdtlpdtrp0(xN, _430082))]]], (2131 ^ _362047) ^ [_434583] : [-(aElementOf0(_434583, sdtmndt0(sdtlpdtrp0(xN, _430082), szmzizndt0(sdtlpdtrp0(xN, _430082))))), aElement0(_434583), aElementOf0(_434583, sdtlpdtrp0(xN, _430082)), -(_434583 = szmzizndt0(sdtlpdtrp0(xN, _430082)))]]]]], (2192 ^ _362047) ^ [_436672] : [aElementOf0(_436672, szNzAzT0), 2195 ^ _362047 : [(2196 ^ _362047) ^ [] : [-(aSet0(sdtlcdtrc0(sdtlpdtrp0(xC, _436672), szDzozmdt0(sdtlpdtrp0(xC, _436672)))))], (2223 ^ _362047) ^ [] : [-(aSubsetOf0(sdtlcdtrc0(sdtlpdtrp0(xC, _436672), szDzozmdt0(sdtlpdtrp0(xC, _436672))), xT))], (2217 ^ _362047) ^ [_437793] : [aElementOf0(_437793, sdtlcdtrc0(sdtlpdtrp0(xC, _436672), szDzozmdt0(sdtlpdtrp0(xC, _436672)))), -(aElementOf0(_437793, xT))], (2198 ^ _362047) ^ [_437022] : [aElementOf0(_437022, sdtlcdtrc0(sdtlpdtrp0(xC, _436672), szDzozmdt0(sdtlpdtrp0(xC, _436672)))), 2202 ^ _362047 : [(2203 ^ _362047) ^ [] : [-(aElementOf0(2201 ^ [_436672, _437022], szDzozmdt0(sdtlpdtrp0(xC, _436672))))], (2205 ^ _362047) ^ [] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _436672), 2201 ^ [_436672, _437022]) = _437022)]]], (2207 ^ _362047) ^ [_437386] : [-(aElementOf0(_437386, sdtlcdtrc0(sdtlpdtrp0(xC, _436672), szDzozmdt0(sdtlpdtrp0(xC, _436672))))), 2208 ^ _362047 : [(2209 ^ _362047) ^ [_437502] : [aElementOf0(_437502, szDzozmdt0(sdtlpdtrp0(xC, _436672))), sdtlpdtrp0(sdtlpdtrp0(xC, _436672), _437502) = _437386]]]]], (2225 ^ _362047) ^ [_438081] : [aElementOf0(_438081, szNzAzT0), 2228 ^ _362047 : [(2229 ^ _362047) ^ [_438580] : [isCountable0(_438580), 2232 ^ _362047 : [(2233 ^ _362047) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _438081)), sdtlpdtrp0(xN, _438081)))], (2235 ^ _362047) ^ [_439157] : [aElementOf0(_439157, sdtlpdtrp0(xN, _438081)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _438081)), _439157))], (2276 ^ _362047) ^ [] : [aSubsetOf0(_438580, sdtmndt0(sdtlpdtrp0(xN, _438081), szmzizndt0(sdtlpdtrp0(xN, _438081))))], (2267 ^ _362047) ^ [] : [aSet0(_438580), 2271 ^ _362047 : [(2272 ^ _362047) ^ [] : [-(aElementOf0(2270 ^ [_438081, _438580], _438580))], (2274 ^ _362047) ^ [] : [aElementOf0(2270 ^ [_438081, _438580], sdtmndt0(sdtlpdtrp0(xN, _438081), szmzizndt0(sdtlpdtrp0(xN, _438081))))]]], (2241 ^ _362047) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _438081), szmzizndt0(sdtlpdtrp0(xN, _438081)))))], (2243 ^ _362047) ^ [_439486] : [aElementOf0(_439486, sdtmndt0(sdtlpdtrp0(xN, _438081), szmzizndt0(sdtlpdtrp0(xN, _438081)))), 2246 ^ _362047 : [(2247 ^ _362047) ^ [] : [-(aElement0(_439486))], (2249 ^ _362047) ^ [] : [-(aElementOf0(_439486, sdtlpdtrp0(xN, _438081)))], (2251 ^ _362047) ^ [] : [_439486 = szmzizndt0(sdtlpdtrp0(xN, _438081))]]], (2253 ^ _362047) ^ [_439848] : [-(aElementOf0(_439848, sdtmndt0(sdtlpdtrp0(xN, _438081), szmzizndt0(sdtlpdtrp0(xN, _438081))))), aElement0(_439848), aElementOf0(_439848, sdtlpdtrp0(xN, _438081)), -(_439848 = szmzizndt0(sdtlpdtrp0(xN, _438081)))]], 2279 ^ _362047 : [(2280 ^ _362047) ^ [_440681] : [aSet0(_440681), 2285 ^ _362047 : [(2297 ^ _362047) ^ [] : [aElementOf0(_440681, slbdtsldtrb0(_438580, xk))], (2286 ^ _362047) ^ [] : [2288 ^ _362047 : [(2289 ^ _362047) ^ [] : [-(aElementOf0(2287 ^ [_438081, _438580, _440681], _440681))], (2291 ^ _362047) ^ [] : [aElementOf0(2287 ^ [_438081, _438580, _440681], _438580)], (2293 ^ _362047) ^ [] : [aSubsetOf0(_440681, _438580)]], sbrdtbr0(_440681) = xk]], 2298 ^ _362047 : [(2299 ^ _362047) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _438081)), sdtlpdtrp0(xN, _438081)))], (2301 ^ _362047) ^ [_441576] : [aElementOf0(_441576, sdtlpdtrp0(xN, _438081)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _438081)), _441576))], (2307 ^ _362047) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _438081), szmzizndt0(sdtlpdtrp0(xN, _438081)))))], (2339 ^ _362047) ^ [] : [-(aSubsetOf0(_440681, sdtmndt0(sdtlpdtrp0(xN, _438081), szmzizndt0(sdtlpdtrp0(xN, _438081)))))], (2341 ^ _362047) ^ [] : [-(aElementOf0(_440681, slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _438081), szmzizndt0(sdtlpdtrp0(xN, _438081))), xk)))], (2333 ^ _362047) ^ [_442736] : [aElementOf0(_442736, _440681), -(aElementOf0(_442736, sdtmndt0(sdtlpdtrp0(xN, _438081), szmzizndt0(sdtlpdtrp0(xN, _438081)))))], (2309 ^ _362047) ^ [_441913] : [aElementOf0(_441913, sdtmndt0(sdtlpdtrp0(xN, _438081), szmzizndt0(sdtlpdtrp0(xN, _438081)))), 2312 ^ _362047 : [(2313 ^ _362047) ^ [] : [-(aElement0(_441913))], (2315 ^ _362047) ^ [] : [-(aElementOf0(_441913, sdtlpdtrp0(xN, _438081)))], (2317 ^ _362047) ^ [] : [_441913 = szmzizndt0(sdtlpdtrp0(xN, _438081))]]], (2319 ^ _362047) ^ [_442287] : [-(aElementOf0(_442287, sdtmndt0(sdtlpdtrp0(xN, _438081), szmzizndt0(sdtlpdtrp0(xN, _438081))))), aElement0(_442287), aElementOf0(_442287, sdtlpdtrp0(xN, _438081)), -(_442287 = szmzizndt0(sdtlpdtrp0(xN, _438081)))]]]]]]], (2343 ^ _362047) ^ [_443150] : [aElementOf0(_443150, szNzAzT0), 2347 ^ _362047 : [(2348 ^ _362047) ^ [] : [-(aElementOf0(2346 ^ [_443150], xT))], (2351 ^ _362047) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _443150)), sdtlpdtrp0(xN, _443150)))], (2353 ^ _362047) ^ [_444192] : [aElementOf0(_444192, sdtlpdtrp0(xN, _443150)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _443150)), _444192))], (2359 ^ _362047) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _443150), szmzizndt0(sdtlpdtrp0(xN, _443150)))))], (2361 ^ _362047) ^ [_444509] : [aElementOf0(_444509, sdtmndt0(sdtlpdtrp0(xN, _443150), szmzizndt0(sdtlpdtrp0(xN, _443150)))), 2364 ^ _362047 : [(2365 ^ _362047) ^ [] : [-(aElement0(_444509))], (2367 ^ _362047) ^ [] : [-(aElementOf0(_444509, sdtlpdtrp0(xN, _443150)))], (2369 ^ _362047) ^ [] : [_444509 = szmzizndt0(sdtlpdtrp0(xN, _443150))]]], (2371 ^ _362047) ^ [_444859] : [-(aElementOf0(_444859, sdtmndt0(sdtlpdtrp0(xN, _443150), szmzizndt0(sdtlpdtrp0(xN, _443150))))), aElement0(_444859), aElementOf0(_444859, sdtlpdtrp0(xN, _443150)), -(_444859 = szmzizndt0(sdtlpdtrp0(xN, _443150)))], (2385 ^ _362047) ^ [] : [-(aSet0(2349 ^ [_443150]))], (2387 ^ _362047) ^ [_445344] : [aElementOf0(_445344, 2349 ^ [_443150]), -(aElementOf0(_445344, sdtmndt0(sdtlpdtrp0(xN, _443150), szmzizndt0(sdtlpdtrp0(xN, _443150)))))], (2393 ^ _362047) ^ [] : [-(aSubsetOf0(2349 ^ [_443150], sdtmndt0(sdtlpdtrp0(xN, _443150), szmzizndt0(sdtlpdtrp0(xN, _443150)))))], (2395 ^ _362047) ^ [] : [-(isCountable0(2349 ^ [_443150]))], (2397 ^ _362047) ^ [_445702] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _443150), _445702) = 2346 ^ [_443150]), aSet0(_445702), 2402 ^ _362047 : [(2414 ^ _362047) ^ [] : [aElementOf0(_445702, slbdtsldtrb0(2349 ^ [_443150], xk))], (2403 ^ _362047) ^ [] : [2405 ^ _362047 : [(2406 ^ _362047) ^ [] : [-(aElementOf0(2404 ^ [_443150, _445702], _445702))], (2408 ^ _362047) ^ [] : [aElementOf0(2404 ^ [_443150, _445702], 2349 ^ [_443150])], (2410 ^ _362047) ^ [] : [aSubsetOf0(_445702, 2349 ^ [_443150])]], sbrdtbr0(_445702) = xk]]]]], (2418 ^ _362047) ^ [_446462] : [aElementOf0(_446462, szNzAzT0), 2422 ^ _362047 : [(2423 ^ _362047) ^ [] : [-(aElementOf0(2421 ^ [_446462], xT))], (2425 ^ _362047) ^ [_446853] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _446462), _446853) = 2421 ^ [_446462]), aSet0(_446853), 2430 ^ _362047 : [(2442 ^ _362047) ^ [] : [aElementOf0(_446853, slbdtsldtrb0(sdtlpdtrp0(xN, szszuzczcdt0(_446462)), xk))], (2431 ^ _362047) ^ [] : [2433 ^ _362047 : [(2434 ^ _362047) ^ [] : [-(aElementOf0(2432 ^ [_446462, _446853], _446853))], (2436 ^ _362047) ^ [] : [aElementOf0(2432 ^ [_446462, _446853], sdtlpdtrp0(xN, szszuzczcdt0(_446462)))], (2438 ^ _362047) ^ [] : [aSubsetOf0(_446853, sdtlpdtrp0(xN, szszuzczcdt0(_446462)))]], sbrdtbr0(_446853) = xk]]]]], (2446 ^ _362047) ^ [] : [-(aFunction0(xe))], (2448 ^ _362047) ^ [] : [-(szDzozmdt0(xe) = szNzAzT0)], (2450 ^ _362047) ^ [_447701] : [aElementOf0(_447701, szNzAzT0), 2453 ^ _362047 : [(2454 ^ _362047) ^ [] : [-(aElementOf0(sdtlpdtrp0(xe, _447701), sdtlpdtrp0(xN, _447701)))], (2462 ^ _362047) ^ [] : [-(sdtlpdtrp0(xe, _447701) = szmzizndt0(sdtlpdtrp0(xN, _447701)))], (2456 ^ _362047) ^ [_447956] : [aElementOf0(_447956, sdtlpdtrp0(xN, _447701)), -(sdtlseqdt0(sdtlpdtrp0(xe, _447701), _447956))]]], (2464 ^ _362047) ^ [] : [-(aFunction0(xd))], (2466 ^ _362047) ^ [] : [-(szDzozmdt0(xd) = szNzAzT0)], (2468 ^ _362047) ^ [_448337] : [aElementOf0(_448337, szNzAzT0), 2471 ^ _362047 : [(2472 ^ _362047) ^ [_448533] : [-(sdtlpdtrp0(xd, _448337) = sdtlpdtrp0(sdtlpdtrp0(xC, _448337), _448533)), aSet0(_448533), 2477 ^ _362047 : [(2489 ^ _362047) ^ [] : [aElementOf0(_448533, slbdtsldtrb0(sdtlpdtrp0(xN, szszuzczcdt0(_448337)), xk))], (2478 ^ _362047) ^ [] : [2480 ^ _362047 : [(2481 ^ _362047) ^ [] : [-(aElementOf0(2479 ^ [_448337, _448533], _448533))], (2483 ^ _362047) ^ [] : [aElementOf0(2479 ^ [_448337, _448533], sdtlpdtrp0(xN, szszuzczcdt0(_448337)))], (2485 ^ _362047) ^ [] : [aSubsetOf0(_448533, sdtlpdtrp0(xN, szszuzczcdt0(_448337)))]], sbrdtbr0(_448533) = xk]]]]], (2493 ^ _362047) ^ [] : [-(aSet0(sdtlcdtrc0(xd, szDzozmdt0(xd))))], (2520 ^ _362047) ^ [] : [-(aSubsetOf0(sdtlcdtrc0(xd, szDzozmdt0(xd)), xT))], (2514 ^ _362047) ^ [_450022] : [aElementOf0(_450022, sdtlcdtrc0(xd, szDzozmdt0(xd))), -(aElementOf0(_450022, xT))], (2495 ^ _362047) ^ [_449375] : [aElementOf0(_449375, sdtlcdtrc0(xd, szDzozmdt0(xd))), 2499 ^ _362047 : [(2500 ^ _362047) ^ [] : [-(aElementOf0(2498 ^ [_449375], szDzozmdt0(xd)))], (2502 ^ _362047) ^ [] : [-(sdtlpdtrp0(xd, 2498 ^ [_449375]) = _449375)]]], (2504 ^ _362047) ^ [_449675] : [-(aElementOf0(_449675, sdtlcdtrc0(xd, szDzozmdt0(xd)))), 2505 ^ _362047 : [(2506 ^ _362047) ^ [_449768] : [aElementOf0(_449768, szDzozmdt0(xd)), sdtlpdtrp0(xd, _449768) = _449675]]], (2522 ^ _362047) ^ [] : [-(aElementOf0(szDzizrdt0(xd), xT))], (2524 ^ _362047) ^ [] : [-(aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd))))], (2526 ^ _362047) ^ [_450388] : [aElementOf0(_450388, sdtlbdtrb0(xd, szDzizrdt0(xd))), 2529 ^ _362047 : [(2530 ^ _362047) ^ [] : [-(aElementOf0(_450388, szDzozmdt0(xd)))], (2532 ^ _362047) ^ [] : [-(sdtlpdtrp0(xd, _450388) = szDzizrdt0(xd))]]], (2534 ^ _362047) ^ [_450623] : [-(aElementOf0(_450623, sdtlbdtrb0(xd, szDzizrdt0(xd)))), aElementOf0(_450623, szDzozmdt0(xd)), sdtlpdtrp0(xd, _450623) = szDzizrdt0(xd)], (2544 ^ _362047) ^ [] : [-(aSet0(xO))], (2546 ^ _362047) ^ [] : [-(aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd))))], (2548 ^ _362047) ^ [_451065] : [aElementOf0(_451065, sdtlbdtrb0(xd, szDzizrdt0(xd))), 2551 ^ _362047 : [(2552 ^ _362047) ^ [] : [-(aElementOf0(_451065, szDzozmdt0(xd)))], (2554 ^ _362047) ^ [] : [-(sdtlpdtrp0(xd, _451065) = szDzizrdt0(xd))]]], (2556 ^ _362047) ^ [_451300] : [-(aElementOf0(_451300, sdtlbdtrb0(xd, szDzizrdt0(xd)))), aElementOf0(_451300, szDzozmdt0(xd)), sdtlpdtrp0(xd, _451300) = szDzizrdt0(xd)], (2585 ^ _362047) ^ [] : [-(xO = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))], (2566 ^ _362047) ^ [_451612] : [aElementOf0(_451612, xO), 2570 ^ _362047 : [(2571 ^ _362047) ^ [] : [-(aElementOf0(2569 ^ [_451612], sdtlbdtrb0(xd, szDzizrdt0(xd))))], (2573 ^ _362047) ^ [] : [-(sdtlpdtrp0(xe, 2569 ^ [_451612]) = _451612)]]], (2575 ^ _362047) ^ [_451912] : [-(aElementOf0(_451912, xO)), 2576 ^ _362047 : [(2577 ^ _362047) ^ [_452005] : [aElementOf0(_452005, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlpdtrp0(xe, _452005) = _451912]]], (2587 ^ _362047) ^ [] : [-(aSet0(xO))], (2589 ^ _362047) ^ [] : [-(isCountable0(xO))], (2591 ^ _362047) ^ [_452410] : [2601 ^ _362047 : [(2602 ^ _362047) ^ [] : [-(aElementOf0(2600 ^ [_452410], szNzAzT0))], (2604 ^ _362047) ^ [] : [-(sdtlpdtrp0(xd, 2600 ^ [_452410]) = szDzizrdt0(xd))], (2606 ^ _362047) ^ [] : [-(aElementOf0(2600 ^ [_452410], sdtlbdtrb0(xd, szDzizrdt0(xd))))], (2608 ^ _362047) ^ [] : [-(sdtlpdtrp0(xe, 2600 ^ [_452410]) = _452410)]], 2592 ^ _362047 : [(2599 ^ _362047) ^ [] : [aElementOf0(_452410, xO)], (2593 ^ _362047) ^ [_452558] : [aElementOf0(_452558, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlpdtrp0(xe, _452558) = _452410]]], (2616 ^ _362047) ^ [] : [-(aSubsetOf0(xO, xS))], (2610 ^ _362047) ^ [_453165] : [aElementOf0(_453165, xO), -(aElementOf0(_453165, xS))], (2618 ^ _362047) ^ [] : [-(aSet0(xQ))], (2626 ^ _362047) ^ [] : [-(aSubsetOf0(xQ, xO))], (2628 ^ _362047) ^ [] : [-(sbrdtbr0(xQ) = xK)], (2630 ^ _362047) ^ [] : [-(aElementOf0(xQ, slbdtsldtrb0(xO, xK)))], (2620 ^ _362047) ^ [_453463] : [aElementOf0(_453463, xQ), -(aElementOf0(_453463, xO))], (2639 ^ _362047) ^ [] : [-(aElementOf0(2637 ^ [], xQ))], (2641 ^ _362047) ^ [] : [xQ = slcrc0], (2632 ^ _362047) ^ [_453824] : [aElementOf0(_453824, xQ), -(aElementOf0(_453824, xO))], (2649 ^ _362047) ^ [] : [-(aSubsetOf0(xQ, szNzAzT0))], (2643 ^ _362047) ^ [_454142] : [aElementOf0(_454142, xQ), -(aElementOf0(_454142, szNzAzT0))]], input).
% 0.56/1.37 ncf('1',plain,[aElementOf0(2650 ^ [], xS)],start(2654 ^ 0)).
% 0.56/1.37 ncf('1.1',plain,[-(aElementOf0(2650 ^ [], xS)), aElementOf0(2650 ^ [], xO)],extension(2610 ^ 1,bind([[_453165], [2650 ^ []]]))).
% 0.56/1.37 ncf('1.1.1',plain,[-(aElementOf0(2650 ^ [], xO)), 347 : aElementOf0(2650 ^ [], xQ), 347 : aSubsetOf0(xQ, xO), 341 : aSet0(xO)],extension(337 ^ 2,bind([[_372884, _373060, _373269], [xO, xQ, 2650 ^ []]]))).
% 0.56/1.37 ncf('1.1.1.1',plain,[-(aElementOf0(2650 ^ [], xQ))],extension(2652 ^ 7)).
% 0.56/1.37 ncf('1.1.1.2',plain,[-(aSubsetOf0(xQ, xO))],extension(2626 ^ 5)).
% 0.56/1.37 ncf('1.1.1.3',plain,[-(aSet0(xO))],extension(2544 ^ 3)).
% 0.56/1.37 %-----------------------------------------------------
% 0.56/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------