%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM614+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n013.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:09 EDT 2023
% Result : Theorem 101.36s 98.69s
% Output : Proof 101.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NUM614+1 : TPTP v8.1.2. Released v4.0.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n013.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 18 17:05:35 EDT 2023
% 0.13/0.33 % CPUTime :
% 101.36/98.69
% 101.36/98.69 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 101.36/98.69 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 101.36/98.69 %-----------------------------------------------------
% 101.36/98.69 ncf(matrix, plain, [(1861 ^ _229511) ^ [] : [aElementOf0(xP, slbdtsldtrb0(xO, xk))], (126 ^ _229511) ^ [_233532, _233534] : [_233534 = _233532, -(szmzazxdt0(_233534) = szmzazxdt0(_233532))], (132 ^ _229511) ^ [_233750, _233752] : [_233752 = _233750, -(slbdtrb0(_233752) = slbdtrb0(_233750))], (138 ^ _229511) ^ [_233996, _233998, _234000, _234002] : [-(sdtexdt0(_234002, _233998) = sdtexdt0(_234000, _233996)), _234002 = _234000, _233998 = _233996], (148 ^ _229511) ^ [_234355, _234357, _234359, _234361] : [-(sdtpldt0(_234361, _234357) = sdtpldt0(_234359, _234355)), _234361 = _234359, _234357 = _234355], (158 ^ _229511) ^ [_234686, _234688] : [_234688 = _234686, -(szszuzczcdt0(_234688) = szszuzczcdt0(_234686))], (164 ^ _229511) ^ [_234932, _234934, _234936, _234938] : [-(sdtlcdtrc0(_234938, _234934) = sdtlcdtrc0(_234936, _234932)), _234938 = _234936, _234934 = _234932], (174 ^ _229511) ^ [_235291, _235293, _235295, _235297] : [-(sdtlbdtrb0(_235297, _235293) = sdtlbdtrb0(_235295, _235291)), _235297 = _235295, _235293 = _235291], (184 ^ _229511) ^ [_235622, _235624] : [_235624 = _235622, -(szDzizrdt0(_235624) = szDzizrdt0(_235622))], (190 ^ _229511) ^ [_235868, _235870, _235872, _235874] : [-(sdtlpdtrp0(_235874, _235870) = sdtlpdtrp0(_235872, _235868)), _235874 = _235872, _235870 = _235868], (200 ^ _229511) ^ [_236199, _236201] : [_236201 = _236199, -(szDzozmdt0(_236201) = szDzozmdt0(_236199))], (206 ^ _229511) ^ [_236445, _236447, _236449, _236451] : [-(sdtmndt0(_236451, _236447) = sdtmndt0(_236449, _236445)), _236451 = _236449, _236447 = _236445], (216 ^ _229511) ^ [_236776, _236778] : [_236778 = _236776, -(szmzizndt0(_236778) = szmzizndt0(_236776))], (222 ^ _229511) ^ [_236994, _236996] : [_236996 = _236994, -(sbrdtbr0(_236996) = sbrdtbr0(_236994))], (228 ^ _229511) ^ [_237220, _237222, _237224, _237226] : [-(slbdtsldtrb0(_237226, _237222) = slbdtsldtrb0(_237224, _237220)), _237226 = _237224, _237222 = _237220], (2 ^ _229511) ^ [_229655] : [-(_229655 = _229655)], (4 ^ _229511) ^ [_229762, _229764] : [_229764 = _229762, -(_229762 = _229764)], (10 ^ _229511) ^ [_229966, _229968, _229970] : [-(_229970 = _229966), _229970 = _229968, _229968 = _229966], (20 ^ _229511) ^ [_230279, _230281] : [-(aElement0(_230279)), _230281 = _230279, aElement0(_230281)], (30 ^ _229511) ^ [_230574, _230576] : [-(isFinite0(_230574)), _230576 = _230574, isFinite0(_230576)], (40 ^ _229511) ^ [_230897, _230899, _230901, _230903] : [-(iLess0(_230901, _230897)), iLess0(_230903, _230899), _230903 = _230901, _230899 = _230897], (54 ^ _229511) ^ [_231341, _231343, _231345, _231347] : [-(sdtlseqdt0(_231345, _231341)), sdtlseqdt0(_231347, _231343), _231347 = _231345, _231343 = _231341], (68 ^ _229511) ^ [_231757, _231759] : [-(aFunction0(_231757)), _231759 = _231757, aFunction0(_231759)], (78 ^ _229511) ^ [_232052, _232054] : [-(isCountable0(_232052)), _232054 = _232052, isCountable0(_232054)], (88 ^ _229511) ^ [_232347, _232349] : [-(aSet0(_232347)), _232349 = _232347, aSet0(_232349)], (98 ^ _229511) ^ [_232670, _232672, _232674, _232676] : [-(aSubsetOf0(_232674, _232670)), aSubsetOf0(_232676, _232672), _232676 = _232674, _232672 = _232670], (112 ^ _229511) ^ [_233094, _233096, _233098, _233100] : [-(aElementOf0(_233098, _233094)), aElementOf0(_233100, _233096), _233100 = _233098, _233096 = _233094], (238 ^ _229511) ^ [_237623] : [aSet0(_237623), true___, -(true___)], (248 ^ _229511) ^ [_237878] : [aElement0(_237878), true___, -(true___)], (258 ^ _229511) ^ [_238133] : [aSet0(_238133), 261 ^ _229511 : [(262 ^ _229511) ^ [_238263] : [aElementOf0(_238263, _238133), -(aElement0(_238263))]]], (268 ^ _229511) ^ [_238464] : [aSet0(_238464), isFinite0(_238464), true___, -(true___)], (282 ^ _229511) ^ [_238834] : [_238834 = slcrc0, 285 ^ _229511 : [(286 ^ _229511) ^ [] : [-(aSet0(_238834))], (288 ^ _229511) ^ [_239015] : [aElementOf0(_239015, _238834)]]], (290 ^ _229511) ^ [_239083] : [-(_239083 = slcrc0), aSet0(_239083), -(aElementOf0(295 ^ [_239083], _239083))], (301 ^ _229511) ^ [] : [-(isFinite0(slcrc0))], (303 ^ _229511) ^ [_239465] : [aSet0(_239465), isCountable0(_239465), true___, -(true___)], (317 ^ _229511) ^ [_239806] : [isFinite0(_239806), aSet0(_239806), isCountable0(_239806)], (327 ^ _229511) ^ [_240076] : [_240076 = slcrc0, aSet0(_240076), isCountable0(_240076)], (337 ^ _229511) ^ [_240348] : [aSet0(_240348), 340 ^ _229511 : [(341 ^ _229511) ^ [_240524] : [aSubsetOf0(_240524, _240348), 344 ^ _229511 : [(345 ^ _229511) ^ [] : [-(aSet0(_240524))], (347 ^ _229511) ^ [_240733] : [aElementOf0(_240733, _240524), -(aElementOf0(_240733, _240348))]]], (353 ^ _229511) ^ [_240912] : [-(aSubsetOf0(_240912, _240348)), aSet0(_240912), 359 ^ _229511 : [(360 ^ _229511) ^ [] : [-(aElementOf0(358 ^ [_240348, _240912], _240912))], (362 ^ _229511) ^ [] : [aElementOf0(358 ^ [_240348, _240912], _240348)]]]]], (366 ^ _229511) ^ [_241349] : [aSet0(_241349), isFinite0(_241349), 373 ^ _229511 : [(374 ^ _229511) ^ [_241562] : [aSubsetOf0(_241562, _241349), -(isFinite0(_241562))]]], (380 ^ _229511) ^ [_241765] : [aSet0(_241765), -(aSubsetOf0(_241765, _241765))], (386 ^ _229511) ^ [_241967, _241969] : [aSet0(_241969), aSet0(_241967), -(_241969 = _241967), aSubsetOf0(_241969, _241967), aSubsetOf0(_241967, _241969)], (404 ^ _229511) ^ [_242456, _242458, _242460] : [aSet0(_242460), aSet0(_242458), aSet0(_242456), -(aSubsetOf0(_242460, _242456)), aSubsetOf0(_242460, _242458), aSubsetOf0(_242458, _242456)], (426 ^ _229511) ^ [_243042, _243044] : [aSet0(_243044), aElement0(_243042), 433 ^ _229511 : [(464 ^ _229511) ^ [_244303] : [-(_244303 = sdtpldt0(_243044, _243042)), aSet0(_244303), 472 ^ _229511 : [(473 ^ _229511) ^ [] : [-(aElementOf0(469 ^ [_243042, _243044, _244303], _244303))], (475 ^ _229511) ^ [] : [aElement0(469 ^ [_243042, _243044, _244303]), 478 ^ _229511 : [(479 ^ _229511) ^ [] : [aElementOf0(469 ^ [_243042, _243044, _244303], _243044)], (481 ^ _229511) ^ [] : [469 ^ [_243042, _243044, _244303] = _243042]]]], 482 ^ _229511 : [(491 ^ _229511) ^ [] : [aElementOf0(469 ^ [_243042, _243044, _244303], _244303)], (483 ^ _229511) ^ [] : [-(aElement0(469 ^ [_243042, _243044, _244303]))], (485 ^ _229511) ^ [] : [-(aElementOf0(469 ^ [_243042, _243044, _244303], _243044)), -(469 ^ [_243042, _243044, _244303] = _243042)]]], (434 ^ _229511) ^ [_243323] : [_243323 = sdtpldt0(_243044, _243042), 437 ^ _229511 : [(438 ^ _229511) ^ [] : [-(aSet0(_243323))], (440 ^ _229511) ^ [_243586] : [aElementOf0(_243586, _243323), 443 ^ _229511 : [(444 ^ _229511) ^ [] : [-(aElement0(_243586))], (446 ^ _229511) ^ [] : [-(aElementOf0(_243586, _243044)), -(_243586 = _243042)]]], (452 ^ _229511) ^ [_243941] : [-(aElementOf0(_243941, _243323)), aElement0(_243941), 457 ^ _229511 : [(458 ^ _229511) ^ [] : [aElementOf0(_243941, _243044)], (460 ^ _229511) ^ [] : [_243941 = _243042]]]]]]], (495 ^ _229511) ^ [_245340, _245342] : [aSet0(_245342), aElement0(_245340), 502 ^ _229511 : [(533 ^ _229511) ^ [_246608] : [-(_246608 = sdtmndt0(_245342, _245340)), aSet0(_246608), 553 ^ _229511 : [(554 ^ _229511) ^ [] : [-(aElement0(538 ^ [_245340, _245342, _246608]))], (556 ^ _229511) ^ [] : [-(aElementOf0(538 ^ [_245340, _245342, _246608], _245342))], (558 ^ _229511) ^ [] : [538 ^ [_245340, _245342, _246608] = _245340], (560 ^ _229511) ^ [] : [aElementOf0(538 ^ [_245340, _245342, _246608], _246608)]], 541 ^ _229511 : [(542 ^ _229511) ^ [] : [-(aElementOf0(538 ^ [_245340, _245342, _246608], _246608))], (544 ^ _229511) ^ [] : [aElement0(538 ^ [_245340, _245342, _246608]), aElementOf0(538 ^ [_245340, _245342, _246608], _245342), -(538 ^ [_245340, _245342, _246608] = _245340)]]], (503 ^ _229511) ^ [_245623] : [_245623 = sdtmndt0(_245342, _245340), 506 ^ _229511 : [(507 ^ _229511) ^ [] : [-(aSet0(_245623))], (509 ^ _229511) ^ [_245888] : [aElementOf0(_245888, _245623), 512 ^ _229511 : [(513 ^ _229511) ^ [] : [-(aElement0(_245888))], (515 ^ _229511) ^ [] : [-(aElementOf0(_245888, _245342))], (517 ^ _229511) ^ [] : [_245888 = _245340]]], (519 ^ _229511) ^ [_246224] : [-(aElementOf0(_246224, _245623)), aElement0(_246224), aElementOf0(_246224, _245342), -(_246224 = _245340)]]]]], (564 ^ _229511) ^ [_247638] : [aSet0(_247638), 567 ^ _229511 : [(568 ^ _229511) ^ [_247775] : [aElementOf0(_247775, _247638), -(sdtpldt0(sdtmndt0(_247638, _247775), _247775) = _247638)]]], (574 ^ _229511) ^ [_248004, _248006] : [aElement0(_248006), aSet0(_248004), -(aElementOf0(_248006, _248004)), -(sdtmndt0(sdtpldt0(_248004, _248006), _248006) = _248004)], (588 ^ _229511) ^ [_248391] : [aElement0(_248391), 591 ^ _229511 : [(592 ^ _229511) ^ [_248528] : [-(isCountable0(sdtpldt0(_248528, _248391))), aSet0(_248528), isCountable0(_248528)]]], (602 ^ _229511) ^ [_248820] : [aElement0(_248820), 605 ^ _229511 : [(606 ^ _229511) ^ [_248957] : [-(isCountable0(sdtmndt0(_248957, _248820))), aSet0(_248957), isCountable0(_248957)]]], (616 ^ _229511) ^ [_249249] : [aElement0(_249249), 619 ^ _229511 : [(620 ^ _229511) ^ [_249386] : [-(isFinite0(sdtpldt0(_249386, _249249))), aSet0(_249386), isFinite0(_249386)]]], (630 ^ _229511) ^ [_249678] : [aElement0(_249678), 633 ^ _229511 : [(634 ^ _229511) ^ [_249815] : [-(isFinite0(sdtmndt0(_249815, _249678))), aSet0(_249815), isFinite0(_249815)]]], (644 ^ _229511) ^ [] : [-(aSet0(szNzAzT0))], (646 ^ _229511) ^ [] : [-(isCountable0(szNzAzT0))], (648 ^ _229511) ^ [] : [-(aElementOf0(sz00, szNzAzT0))], (650 ^ _229511) ^ [_250268] : [aElementOf0(_250268, szNzAzT0), 653 ^ _229511 : [(654 ^ _229511) ^ [] : [-(aElementOf0(szszuzczcdt0(_250268), szNzAzT0))], (656 ^ _229511) ^ [] : [szszuzczcdt0(_250268) = sz00]]], (658 ^ _229511) ^ [_250554, _250556] : [aElementOf0(_250556, szNzAzT0), aElementOf0(_250554, szNzAzT0), szszuzczcdt0(_250556) = szszuzczcdt0(_250554), -(_250556 = _250554)], (672 ^ _229511) ^ [_250938] : [aElementOf0(_250938, szNzAzT0), -(_250938 = sz00), 680 ^ _229511 : [(681 ^ _229511) ^ [] : [-(aElementOf0(679 ^ [_250938], szNzAzT0))], (683 ^ _229511) ^ [] : [-(_250938 = szszuzczcdt0(679 ^ [_250938]))]]], (685 ^ _229511) ^ [_251355] : [aElementOf0(_251355, szNzAzT0), _251355 = szszuzczcdt0(_251355)], (691 ^ _229511) ^ [_251564, _251566] : [aElementOf0(_251566, szNzAzT0), aElementOf0(_251564, szNzAzT0), sdtlseqdt0(_251566, _251564), true___, -(true___)], (709 ^ _229511) ^ [_252014] : [aElementOf0(_252014, szNzAzT0), -(sdtlseqdt0(sz00, _252014))], (715 ^ _229511) ^ [_252204] : [aElementOf0(_252204, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_252204), sz00)], (721 ^ _229511) ^ [_252413, _252415] : [aElementOf0(_252415, szNzAzT0), aElementOf0(_252413, szNzAzT0), 728 ^ _229511 : [(729 ^ _229511) ^ [] : [sdtlseqdt0(_252415, _252413), -(sdtlseqdt0(szszuzczcdt0(_252415), szszuzczcdt0(_252413)))], (735 ^ _229511) ^ [] : [sdtlseqdt0(szszuzczcdt0(_252415), szszuzczcdt0(_252413)), -(sdtlseqdt0(_252415, _252413))]]], (741 ^ _229511) ^ [_252962] : [aElementOf0(_252962, szNzAzT0), -(sdtlseqdt0(_252962, szszuzczcdt0(_252962)))], (747 ^ _229511) ^ [_253156] : [aElementOf0(_253156, szNzAzT0), -(sdtlseqdt0(_253156, _253156))], (753 ^ _229511) ^ [_253360, _253362] : [aElementOf0(_253362, szNzAzT0), aElementOf0(_253360, szNzAzT0), -(_253362 = _253360), sdtlseqdt0(_253362, _253360), sdtlseqdt0(_253360, _253362)], (771 ^ _229511) ^ [_253853, _253855, _253857] : [aElementOf0(_253857, szNzAzT0), aElementOf0(_253855, szNzAzT0), aElementOf0(_253853, szNzAzT0), -(sdtlseqdt0(_253857, _253853)), sdtlseqdt0(_253857, _253855), sdtlseqdt0(_253855, _253853)], (793 ^ _229511) ^ [_254445, _254447] : [aElementOf0(_254447, szNzAzT0), aElementOf0(_254445, szNzAzT0), -(sdtlseqdt0(_254447, _254445)), -(sdtlseqdt0(szszuzczcdt0(_254445), _254447))], (807 ^ _229511) ^ [_254840, _254842] : [aElementOf0(_254842, szNzAzT0), aElementOf0(_254840, szNzAzT0), iLess0(_254842, _254840), true___, -(true___)], (825 ^ _229511) ^ [_255290] : [aElementOf0(_255290, szNzAzT0), -(iLess0(_255290, szszuzczcdt0(_255290)))], (831 ^ _229511) ^ [_255484] : [aSet0(_255484), -(aElement0(sbrdtbr0(_255484)))], (837 ^ _229511) ^ [_255674] : [aSet0(_255674), 840 ^ _229511 : [(841 ^ _229511) ^ [] : [aElementOf0(sbrdtbr0(_255674), szNzAzT0), -(isFinite0(_255674))], (847 ^ _229511) ^ [] : [isFinite0(_255674), -(aElementOf0(sbrdtbr0(_255674), szNzAzT0))]]], (853 ^ _229511) ^ [_256105] : [aSet0(_256105), 856 ^ _229511 : [(857 ^ _229511) ^ [] : [sbrdtbr0(_256105) = sz00, -(_256105 = slcrc0)], (863 ^ _229511) ^ [] : [_256105 = slcrc0, -(sbrdtbr0(_256105) = sz00)]]], (869 ^ _229511) ^ [_256539] : [aSet0(_256539), isFinite0(_256539), 876 ^ _229511 : [(877 ^ _229511) ^ [_256769] : [aElement0(_256769), -(aElementOf0(_256769, _256539)), -(sbrdtbr0(sdtpldt0(_256539, _256769)) = szszuzczcdt0(sbrdtbr0(_256539)))]]], (887 ^ _229511) ^ [_257082] : [aSet0(_257082), 890 ^ _229511 : [(891 ^ _229511) ^ [_257227] : [-(szszuzczcdt0(sbrdtbr0(sdtmndt0(_257082, _257227))) = sbrdtbr0(_257082)), isFinite0(_257082), aElementOf0(_257227, _257082)]]], (901 ^ _229511) ^ [_257535] : [aSet0(_257535), 904 ^ _229511 : [(905 ^ _229511) ^ [_257675] : [-(sdtlseqdt0(sbrdtbr0(_257675), sbrdtbr0(_257535))), isFinite0(_257535), aSubsetOf0(_257675, _257535)]]], (915 ^ _229511) ^ [_257987, _257989] : [aSet0(_257989), aElementOf0(_257987, szNzAzT0), 931 ^ _229511 : [(932 ^ _229511) ^ [] : [-(aSubsetOf0(930 ^ [_257987, _257989], _257989))], (934 ^ _229511) ^ [] : [-(sbrdtbr0(930 ^ [_257987, _257989]) = _257987)]], isFinite0(_257989), sdtlseqdt0(_257987, sbrdtbr0(_257989))], (936 ^ _229511) ^ [_258603] : [aSubsetOf0(_258603, szNzAzT0), -(_258603 = slcrc0), 943 ^ _229511 : [(944 ^ _229511) ^ [_258872] : [_258872 = szmzizndt0(_258603), 947 ^ _229511 : [(948 ^ _229511) ^ [] : [-(aElementOf0(_258872, _258603))], (950 ^ _229511) ^ [_259087] : [aElementOf0(_259087, _258603), -(sdtlseqdt0(_258872, _259087))]]], (956 ^ _229511) ^ [_259266] : [-(_259266 = szmzizndt0(_258603)), aElementOf0(_259266, _258603), 962 ^ _229511 : [(963 ^ _229511) ^ [] : [-(aElementOf0(961 ^ [_258603, _259266], _258603))], (965 ^ _229511) ^ [] : [sdtlseqdt0(_259266, 961 ^ [_258603, _259266])]]]]], (969 ^ _229511) ^ [_259711] : [aSubsetOf0(_259711, szNzAzT0), isFinite0(_259711), -(_259711 = slcrc0), 980 ^ _229511 : [(981 ^ _229511) ^ [_260063] : [_260063 = szmzazxdt0(_259711), 984 ^ _229511 : [(985 ^ _229511) ^ [] : [-(aElementOf0(_260063, _259711))], (987 ^ _229511) ^ [_260278] : [aElementOf0(_260278, _259711), -(sdtlseqdt0(_260278, _260063))]]], (993 ^ _229511) ^ [_260457] : [-(_260457 = szmzazxdt0(_259711)), aElementOf0(_260457, _259711), 999 ^ _229511 : [(1000 ^ _229511) ^ [] : [-(aElementOf0(998 ^ [_259711, _260457], _259711))], (1002 ^ _229511) ^ [] : [sdtlseqdt0(998 ^ [_259711, _260457], _260457)]]]]], (1006 ^ _229511) ^ [_260918, _260920] : [-(szmzizndt0(_260920) = szmzizndt0(_260918)), aElementOf0(szmzizndt0(_260920), _260918), aElementOf0(szmzizndt0(_260918), _260920), aSubsetOf0(_260920, szNzAzT0), aSubsetOf0(_260918, szNzAzT0), -(_260920 = slcrc0), -(_260918 = slcrc0)], (1032 ^ _229511) ^ [_261585] : [aElementOf0(_261585, szNzAzT0), 1035 ^ _229511 : [(1060 ^ _229511) ^ [_262554] : [-(_262554 = slbdtrb0(_261585)), aSet0(_262554), 1076 ^ _229511 : [(1077 ^ _229511) ^ [] : [-(aElementOf0(1065 ^ [_261585, _262554], szNzAzT0))], (1079 ^ _229511) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(1065 ^ [_261585, _262554]), _261585))], (1081 ^ _229511) ^ [] : [aElementOf0(1065 ^ [_261585, _262554], _262554)]], 1068 ^ _229511 : [(1069 ^ _229511) ^ [] : [-(aElementOf0(1065 ^ [_261585, _262554], _262554))], (1071 ^ _229511) ^ [] : [aElementOf0(1065 ^ [_261585, _262554], szNzAzT0), sdtlseqdt0(szszuzczcdt0(1065 ^ [_261585, _262554]), _261585)]]], (1036 ^ _229511) ^ [_261773] : [_261773 = slbdtrb0(_261585), 1039 ^ _229511 : [(1040 ^ _229511) ^ [] : [-(aSet0(_261773))], (1042 ^ _229511) ^ [_262023] : [aElementOf0(_262023, _261773), 1045 ^ _229511 : [(1046 ^ _229511) ^ [] : [-(aElementOf0(_262023, szNzAzT0))], (1048 ^ _229511) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(_262023), _261585))]]], (1050 ^ _229511) ^ [_262276] : [-(aElementOf0(_262276, _261773)), aElementOf0(_262276, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_262276), _261585)]]]]], (1085 ^ _229511) ^ [_263357] : [aElementOf0(_263357, szNzAzT0), -(isFinite0(slbdtrb0(_263357)))], (1091 ^ _229511) ^ [] : [-(slbdtrb0(sz00) = slcrc0)], (1093 ^ _229511) ^ [_263616, _263618] : [aElementOf0(_263618, szNzAzT0), aElementOf0(_263616, szNzAzT0), 1100 ^ _229511 : [(1111 ^ _229511) ^ [] : [1112 ^ _229511 : [(1113 ^ _229511) ^ [] : [aElementOf0(_263618, slbdtrb0(_263616))], (1115 ^ _229511) ^ [] : [_263618 = _263616]], -(aElementOf0(_263618, slbdtrb0(szszuzczcdt0(_263616))))], (1101 ^ _229511) ^ [] : [aElementOf0(_263618, slbdtrb0(szszuzczcdt0(_263616))), -(aElementOf0(_263618, slbdtrb0(_263616))), -(_263618 = _263616)]]], (1119 ^ _229511) ^ [_264343, _264345] : [aElementOf0(_264345, szNzAzT0), aElementOf0(_264343, szNzAzT0), 1126 ^ _229511 : [(1127 ^ _229511) ^ [] : [sdtlseqdt0(_264345, _264343), -(aSubsetOf0(slbdtrb0(_264345), slbdtrb0(_264343)))], (1133 ^ _229511) ^ [] : [aSubsetOf0(slbdtrb0(_264345), slbdtrb0(_264343)), -(sdtlseqdt0(_264345, _264343))]]], (1139 ^ _229511) ^ [_264892] : [1147 ^ _229511 : [(1148 ^ _229511) ^ [] : [-(aElementOf0(1146 ^ [_264892], szNzAzT0))], (1150 ^ _229511) ^ [] : [-(aSubsetOf0(_264892, slbdtrb0(1146 ^ [_264892])))]], aSubsetOf0(_264892, szNzAzT0), isFinite0(_264892)], (1152 ^ _229511) ^ [_265306] : [aElementOf0(_265306, szNzAzT0), -(sbrdtbr0(slbdtrb0(_265306)) = _265306)], (1158 ^ _229511) ^ [_265518, _265520] : [aSet0(_265520), aElementOf0(_265518, szNzAzT0), 1165 ^ _229511 : [(1190 ^ _229511) ^ [_266611] : [-(_266611 = slbdtsldtrb0(_265520, _265518)), aSet0(_266611), 1206 ^ _229511 : [(1207 ^ _229511) ^ [] : [-(aSubsetOf0(1195 ^ [_265518, _265520, _266611], _265520))], (1209 ^ _229511) ^ [] : [-(sbrdtbr0(1195 ^ [_265518, _265520, _266611]) = _265518)], (1211 ^ _229511) ^ [] : [aElementOf0(1195 ^ [_265518, _265520, _266611], _266611)]], 1198 ^ _229511 : [(1199 ^ _229511) ^ [] : [-(aElementOf0(1195 ^ [_265518, _265520, _266611], _266611))], (1201 ^ _229511) ^ [] : [aSubsetOf0(1195 ^ [_265518, _265520, _266611], _265520), sbrdtbr0(1195 ^ [_265518, _265520, _266611]) = _265518]]], (1166 ^ _229511) ^ [_265798] : [_265798 = slbdtsldtrb0(_265520, _265518), 1169 ^ _229511 : [(1170 ^ _229511) ^ [] : [-(aSet0(_265798))], (1172 ^ _229511) ^ [_266058] : [aElementOf0(_266058, _265798), 1175 ^ _229511 : [(1176 ^ _229511) ^ [] : [-(aSubsetOf0(_266058, _265520))], (1178 ^ _229511) ^ [] : [-(sbrdtbr0(_266058) = _265518)]]], (1180 ^ _229511) ^ [_266321] : [-(aElementOf0(_266321, _265798)), aSubsetOf0(_266321, _265520), sbrdtbr0(_266321) = _265518]]]]], (1215 ^ _229511) ^ [_267460] : [aSet0(_267460), isFinite0(_267460), 1222 ^ _229511 : [(1223 ^ _229511) ^ [_267676] : [aElementOf0(_267676, szNzAzT0), -(isFinite0(slbdtsldtrb0(_267460, _267676)))]]], (1229 ^ _229511) ^ [_267885] : [aSet0(_267885), -(isFinite0(_267885)), 1236 ^ _229511 : [(1237 ^ _229511) ^ [_268107] : [aElementOf0(_268107, szNzAzT0), slbdtsldtrb0(_267885, _268107) = slcrc0]]], (1243 ^ _229511) ^ [_268319] : [aSet0(_268319), isCountable0(_268319), 1250 ^ _229511 : [(1251 ^ _229511) ^ [_268543] : [-(isCountable0(slbdtsldtrb0(_268319, _268543))), aElementOf0(_268543, szNzAzT0), -(_268543 = sz00)]]], (1261 ^ _229511) ^ [_268844] : [aElementOf0(_268844, szNzAzT0), 1264 ^ _229511 : [(1265 ^ _229511) ^ [_269031, _269033] : [aSet0(_269033), aSet0(_269031), -(_268844 = sz00), -(aSubsetOf0(_269033, _269031)), aSubsetOf0(slbdtsldtrb0(_269033, _268844), slbdtsldtrb0(_269031, _268844)), -(slbdtsldtrb0(_269033, _268844) = slcrc0)]]], (1287 ^ _229511) ^ [_269650, _269652] : [aSet0(_269652), aElementOf0(_269650, szNzAzT0), 1294 ^ _229511 : [(1295 ^ _229511) ^ [_269901] : [1303 ^ _229511 : [(1304 ^ _229511) ^ [] : [-(aSubsetOf0(1302 ^ [_269650, _269652, _269901], _269652))], (1306 ^ _229511) ^ [] : [-(isFinite0(1302 ^ [_269650, _269652, _269901]))], (1308 ^ _229511) ^ [] : [-(aSubsetOf0(_269901, slbdtsldtrb0(1302 ^ [_269650, _269652, _269901], _269650)))]], aSubsetOf0(_269901, slbdtsldtrb0(_269652, _269650)), isFinite0(_269901)]]], (1310 ^ _229511) ^ [_270463] : [aFunction0(_270463), true___, -(true___)], (1320 ^ _229511) ^ [_270718] : [aFunction0(_270718), -(aSet0(szDzozmdt0(_270718)))], (1326 ^ _229511) ^ [_270908] : [aFunction0(_270908), 1329 ^ _229511 : [(1330 ^ _229511) ^ [_271043] : [aElementOf0(_271043, szDzozmdt0(_270908)), -(aElement0(sdtlpdtrp0(_270908, _271043)))]]], (1336 ^ _229511) ^ [_271268, _271270] : [aFunction0(_271270), aElement0(_271268), 1343 ^ _229511 : [(1368 ^ _229511) ^ [_272377] : [-(_272377 = sdtlbdtrb0(_271270, _271268)), aSet0(_272377), 1384 ^ _229511 : [(1385 ^ _229511) ^ [] : [-(aElementOf0(1373 ^ [_271268, _271270, _272377], szDzozmdt0(_271270)))], (1387 ^ _229511) ^ [] : [-(sdtlpdtrp0(_271270, 1373 ^ [_271268, _271270, _272377]) = _271268)], (1389 ^ _229511) ^ [] : [aElementOf0(1373 ^ [_271268, _271270, _272377], _272377)]], 1376 ^ _229511 : [(1377 ^ _229511) ^ [] : [-(aElementOf0(1373 ^ [_271268, _271270, _272377], _272377))], (1379 ^ _229511) ^ [] : [aElementOf0(1373 ^ [_271268, _271270, _272377], szDzozmdt0(_271270)), sdtlpdtrp0(_271270, 1373 ^ [_271268, _271270, _272377]) = _271268]]], (1344 ^ _229511) ^ [_271549] : [_271549 = sdtlbdtrb0(_271270, _271268), 1347 ^ _229511 : [(1348 ^ _229511) ^ [] : [-(aSet0(_271549))], (1350 ^ _229511) ^ [_271812] : [aElementOf0(_271812, _271549), 1353 ^ _229511 : [(1354 ^ _229511) ^ [] : [-(aElementOf0(_271812, szDzozmdt0(_271270)))], (1356 ^ _229511) ^ [] : [-(sdtlpdtrp0(_271270, _271812) = _271268)]]], (1358 ^ _229511) ^ [_272081] : [-(aElementOf0(_272081, _271549)), aElementOf0(_272081, szDzozmdt0(_271270)), sdtlpdtrp0(_271270, _272081) = _271268]]]]], (1393 ^ _229511) ^ [_273252, _273254] : [-(aSubsetOf0(sdtlbdtrb0(_273254, _273252), szDzozmdt0(_273254))), aFunction0(_273254), aElement0(_273252)], (1403 ^ _229511) ^ [_273543] : [aFunction0(_273543), 1406 ^ _229511 : [(1407 ^ _229511) ^ [_273720] : [aSubsetOf0(_273720, szDzozmdt0(_273543)), 1410 ^ _229511 : [(1436 ^ _229511) ^ [_274907] : [-(_274907 = sdtlcdtrc0(_273543, _273720)), aSet0(_274907), 1453 ^ _229511 : [(1454 ^ _229511) ^ [] : [-(aElementOf0(1452 ^ [_273543, _273720, _274907], _273720))], (1456 ^ _229511) ^ [] : [-(sdtlpdtrp0(_273543, 1452 ^ [_273543, _273720, _274907]) = 1441 ^ [_273543, _273720, _274907])], (1458 ^ _229511) ^ [] : [aElementOf0(1441 ^ [_273543, _273720, _274907], _274907)]], 1444 ^ _229511 : [(1445 ^ _229511) ^ [] : [-(aElementOf0(1441 ^ [_273543, _273720, _274907], _274907))], (1447 ^ _229511) ^ [_275300] : [aElementOf0(_275300, _273720), sdtlpdtrp0(_273543, _275300) = 1441 ^ [_273543, _273720, _274907]]]], (1411 ^ _229511) ^ [_273925] : [_273925 = sdtlcdtrc0(_273543, _273720), 1414 ^ _229511 : [(1415 ^ _229511) ^ [] : [-(aSet0(_273925))], (1417 ^ _229511) ^ [_274191] : [aElementOf0(_274191, _273925), 1421 ^ _229511 : [(1422 ^ _229511) ^ [] : [-(aElementOf0(1420 ^ [_273543, _273720, _273925, _274191], _273720))], (1424 ^ _229511) ^ [] : [-(sdtlpdtrp0(_273543, 1420 ^ [_273543, _273720, _273925, _274191]) = _274191)]]], (1426 ^ _229511) ^ [_274545] : [-(aElementOf0(_274545, _273925)), 1427 ^ _229511 : [(1428 ^ _229511) ^ [_274650] : [aElementOf0(_274650, _273720), sdtlpdtrp0(_273543, _274650) = _274545]]]]]]]]], (1462 ^ _229511) ^ [_275911] : [aFunction0(_275911), 1465 ^ _229511 : [(1466 ^ _229511) ^ [_276052] : [aElementOf0(_276052, szDzozmdt0(_275911)), -(aElementOf0(sdtlpdtrp0(_275911, _276052), sdtlcdtrc0(_275911, szDzozmdt0(_275911))))]]], (1472 ^ _229511) ^ [_276275] : [aFunction0(_276275), 1475 ^ _229511 : [(1476 ^ _229511) ^ [_276452] : [aSubsetOf0(_276452, szDzozmdt0(_276275)), 1479 ^ _229511 : [(1480 ^ _229511) ^ [_276657] : [_276657 = sdtexdt0(_276275, _276452), 1483 ^ _229511 : [(1484 ^ _229511) ^ [] : [-(aFunction0(_276657))], (1486 ^ _229511) ^ [] : [-(szDzozmdt0(_276657) = _276452)], (1488 ^ _229511) ^ [_276964] : [aElementOf0(_276964, _276452), -(sdtlpdtrp0(_276657, _276964) = sdtlpdtrp0(_276275, _276964))]]], (1494 ^ _229511) ^ [_277165] : [-(_277165 = sdtexdt0(_276275, _276452)), aFunction0(_277165), szDzozmdt0(_277165) = _276452, 1504 ^ _229511 : [(1505 ^ _229511) ^ [] : [-(aElementOf0(1503 ^ [_276275, _276452, _277165], _276452))], (1507 ^ _229511) ^ [] : [sdtlpdtrp0(_277165, 1503 ^ [_276275, _276452, _277165]) = sdtlpdtrp0(_276275, 1503 ^ [_276275, _276452, _277165])]]]]]]], (1511 ^ _229511) ^ [_277759] : [aFunction0(_277759), 1514 ^ _229511 : [(1515 ^ _229511) ^ [_277947] : [aSubsetOf0(_277947, szDzozmdt0(_277759)), isCountable0(_277947), 1526 ^ _229511 : [(1527 ^ _229511) ^ [] : [-(aElementOf0(1524 ^ [_277759, _277947], szDzozmdt0(_277759)))], (1529 ^ _229511) ^ [] : [-(aElementOf0(1525 ^ [_277759, _277947], szDzozmdt0(_277759)))], (1531 ^ _229511) ^ [] : [1524 ^ [_277759, _277947] = 1525 ^ [_277759, _277947]], (1533 ^ _229511) ^ [] : [-(sdtlpdtrp0(_277759, 1524 ^ [_277759, _277947]) = sdtlpdtrp0(_277759, 1525 ^ [_277759, _277947]))]], -(isCountable0(sdtlcdtrc0(_277759, _277947)))]]], (1537 ^ _229511) ^ [_278819] : [aFunction0(_278819), 1548 ^ _229511 : [(1549 ^ _229511) ^ [] : [-(aElement0(szDzizrdt0(_278819)))], (1551 ^ _229511) ^ [] : [-(isCountable0(sdtlbdtrb0(_278819, szDzizrdt0(_278819))))]], isCountable0(szDzozmdt0(_278819)), isFinite0(sdtlcdtrc0(_278819, szDzozmdt0(_278819)))], (1553 ^ _229511) ^ [] : [-(aSet0(xT))], (1555 ^ _229511) ^ [] : [-(isFinite0(xT))], (1557 ^ _229511) ^ [] : [-(aElementOf0(xK, szNzAzT0))], (1559 ^ _229511) ^ [] : [-(aSubsetOf0(xS, szNzAzT0))], (1561 ^ _229511) ^ [] : [-(isCountable0(xS))], (1563 ^ _229511) ^ [] : [-(aFunction0(xc))], (1565 ^ _229511) ^ [] : [-(szDzozmdt0(xc) = slbdtsldtrb0(xS, xK))], (1567 ^ _229511) ^ [] : [-(aSubsetOf0(sdtlcdtrc0(xc, szDzozmdt0(xc)), xT))], (1569 ^ _229511) ^ [_279702] : [aElementOf0(_279702, szNzAzT0), 1572 ^ _229511 : [(1573 ^ _229511) ^ [_279922] : [aSubsetOf0(_279922, szNzAzT0), isCountable0(_279922), 1580 ^ _229511 : [(1581 ^ _229511) ^ [_280219] : [aFunction0(_280219), szDzozmdt0(_280219) = slbdtsldtrb0(_279922, _279702), aSubsetOf0(sdtlcdtrc0(_280219, szDzozmdt0(_280219)), xT), iLess0(_279702, xK), 1597 ^ _229511 : [(1598 ^ _229511) ^ [] : [-(aElementOf0(1596 ^ [_279702, _279922, _280219], xT))], (1601 ^ _229511) ^ [] : [-(aSubsetOf0(1599 ^ [_279702, _279922, _280219], _279922))], (1603 ^ _229511) ^ [] : [-(isCountable0(1599 ^ [_279702, _279922, _280219]))], (1605 ^ _229511) ^ [_281094] : [aElementOf0(_281094, slbdtsldtrb0(1599 ^ [_279702, _279922, _280219], _279702)), -(sdtlpdtrp0(_280219, _281094) = 1596 ^ [_279702, _279922, _280219])]]]]]]], (1611 ^ _229511) ^ [] : [xK = sz00], (1613 ^ _229511) ^ [] : [xK = sz00], (1615 ^ _229511) ^ [] : [-(aElementOf0(xk, szNzAzT0))], (1617 ^ _229511) ^ [] : [-(szszuzczcdt0(xk) = xK)], (1619 ^ _229511) ^ [] : [-(aFunction0(xN))], (1621 ^ _229511) ^ [] : [-(szDzozmdt0(xN) = szNzAzT0)], (1623 ^ _229511) ^ [] : [-(sdtlpdtrp0(xN, sz00) = xS)], (1625 ^ _229511) ^ [_281758] : [aElementOf0(_281758, szNzAzT0), 1636 ^ _229511 : [(1637 ^ _229511) ^ [] : [-(aSubsetOf0(sdtlpdtrp0(xN, szszuzczcdt0(_281758)), sdtmndt0(sdtlpdtrp0(xN, _281758), szmzizndt0(sdtlpdtrp0(xN, _281758)))))], (1639 ^ _229511) ^ [] : [-(isCountable0(sdtlpdtrp0(xN, szszuzczcdt0(_281758))))]], aSubsetOf0(sdtlpdtrp0(xN, _281758), szNzAzT0), isCountable0(sdtlpdtrp0(xN, _281758))], (1641 ^ _229511) ^ [_282247] : [aElementOf0(_282247, szNzAzT0), 1644 ^ _229511 : [(1645 ^ _229511) ^ [] : [-(aSubsetOf0(sdtlpdtrp0(xN, _282247), szNzAzT0))], (1647 ^ _229511) ^ [] : [-(isCountable0(sdtlpdtrp0(xN, _282247)))]]], (1649 ^ _229511) ^ [_282534, _282536] : [aElementOf0(_282536, szNzAzT0), aElementOf0(_282534, szNzAzT0), sdtlseqdt0(_282534, _282536), -(aSubsetOf0(sdtlpdtrp0(xN, _282536), sdtlpdtrp0(xN, _282534)))], (1663 ^ _229511) ^ [_282936, _282938] : [szmzizndt0(sdtlpdtrp0(xN, _282938)) = szmzizndt0(sdtlpdtrp0(xN, _282936)), aElementOf0(_282938, szNzAzT0), aElementOf0(_282936, szNzAzT0), -(_282938 = _282936)], (1677 ^ _229511) ^ [_283334] : [aElementOf0(_283334, szNzAzT0), 1680 ^ _229511 : [(1681 ^ _229511) ^ [_283494] : [-(aElementOf0(sdtpldt0(_283494, szmzizndt0(sdtlpdtrp0(xN, _283334))), slbdtsldtrb0(xS, xK))), aSet0(_283494), aElementOf0(_283494, slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _283334), szmzizndt0(sdtlpdtrp0(xN, _283334))), xk))]]], (1691 ^ _229511) ^ [] : [-(aFunction0(xC))], (1693 ^ _229511) ^ [] : [-(szDzozmdt0(xC) = szNzAzT0)], (1695 ^ _229511) ^ [_283934] : [aElementOf0(_283934, szNzAzT0), 1698 ^ _229511 : [(1699 ^ _229511) ^ [] : [-(aFunction0(sdtlpdtrp0(xC, _283934)))], (1701 ^ _229511) ^ [] : [-(szDzozmdt0(sdtlpdtrp0(xC, _283934)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _283934), szmzizndt0(sdtlpdtrp0(xN, _283934))), xk))], (1703 ^ _229511) ^ [_284285] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _283934), _284285) = sdtlpdtrp0(xc, sdtpldt0(_284285, szmzizndt0(sdtlpdtrp0(xN, _283934))))), aSet0(_284285), aElementOf0(_284285, slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _283934), szmzizndt0(sdtlpdtrp0(xN, _283934))), xk))]]], (1713 ^ _229511) ^ [_284645] : [aElementOf0(_284645, szNzAzT0), -(aSubsetOf0(sdtlcdtrc0(sdtlpdtrp0(xC, _284645), szDzozmdt0(sdtlpdtrp0(xC, _284645))), xT))], (1719 ^ _229511) ^ [_284857] : [aElementOf0(_284857, szNzAzT0), 1722 ^ _229511 : [(1723 ^ _229511) ^ [_285039] : [aSubsetOf0(_285039, sdtmndt0(sdtlpdtrp0(xN, _284857), szmzizndt0(sdtlpdtrp0(xN, _284857)))), isCountable0(_285039), 1730 ^ _229511 : [(1731 ^ _229511) ^ [_285309] : [-(aElementOf0(_285309, slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _284857), szmzizndt0(sdtlpdtrp0(xN, _284857))), xk))), aSet0(_285309), aElementOf0(_285309, slbdtsldtrb0(_285039, xk))]]]]], (1741 ^ _229511) ^ [_285652] : [aElementOf0(_285652, szNzAzT0), 1745 ^ _229511 : [(1746 ^ _229511) ^ [] : [-(aElementOf0(1744 ^ [_285652], xT))], (1749 ^ _229511) ^ [] : [-(aSubsetOf0(1747 ^ [_285652], sdtmndt0(sdtlpdtrp0(xN, _285652), szmzizndt0(sdtlpdtrp0(xN, _285652)))))], (1751 ^ _229511) ^ [] : [-(isCountable0(1747 ^ [_285652]))], (1753 ^ _229511) ^ [_286246] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _285652), _286246) = 1744 ^ [_285652]), aSet0(_286246), aElementOf0(_286246, slbdtsldtrb0(1747 ^ [_285652], xk))]]], (1763 ^ _229511) ^ [_286580] : [aElementOf0(_286580, szNzAzT0), 1767 ^ _229511 : [(1768 ^ _229511) ^ [] : [-(aElementOf0(1766 ^ [_286580], xT))], (1770 ^ _229511) ^ [_286889] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _286580), _286889) = 1766 ^ [_286580]), aSet0(_286889), aElementOf0(_286889, slbdtsldtrb0(sdtlpdtrp0(xN, szszuzczcdt0(_286580)), xk))]]], (1780 ^ _229511) ^ [] : [-(aFunction0(xe))], (1782 ^ _229511) ^ [] : [-(szDzozmdt0(xe) = szNzAzT0)], (1784 ^ _229511) ^ [_287325] : [aElementOf0(_287325, szNzAzT0), -(sdtlpdtrp0(xe, _287325) = szmzizndt0(sdtlpdtrp0(xN, _287325)))], (1808 ^ _229511) ^ [] : [-(aSubsetOf0(sdtlcdtrc0(xd, szDzozmdt0(xd)), xT))], (1810 ^ _229511) ^ [] : [-(aElementOf0(szDzizrdt0(xd), xT))], (1812 ^ _229511) ^ [] : [-(isCountable0(sdtlbdtrb0(xd, szDzizrdt0(xd))))], (1814 ^ _229511) ^ [] : [-(aSet0(xO))], (1816 ^ _229511) ^ [] : [-(xO = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))], (1818 ^ _229511) ^ [] : [-(aSet0(xO))], (1820 ^ _229511) ^ [] : [-(isCountable0(xO))], (1833 ^ _229511) ^ [] : [-(aSubsetOf0(xO, xS))], (1835 ^ _229511) ^ [] : [-(aElementOf0(xQ, slbdtsldtrb0(xO, xK)))], (1837 ^ _229511) ^ [] : [-(aSubsetOf0(xQ, xO))], (1839 ^ _229511) ^ [] : [xQ = slcrc0], (1841 ^ _229511) ^ [] : [-(aSubsetOf0(xQ, szNzAzT0))], (1843 ^ _229511) ^ [] : [-(aElementOf0(xQ, szDzozmdt0(xc)))], (1845 ^ _229511) ^ [] : [-(xp = szmzizndt0(xQ))], (1847 ^ _229511) ^ [] : [-(aSet0(xP))], (1849 ^ _229511) ^ [] : [-(xP = sdtmndt0(xQ, szmzizndt0(xQ)))], (1851 ^ _229511) ^ [] : [-(aElementOf0(xp, xQ))], (1853 ^ _229511) ^ [] : [-(aElementOf0(xp, xO))], (1855 ^ _229511) ^ [] : [-(aSubsetOf0(xP, xQ))], (1857 ^ _229511) ^ [] : [-(aSubsetOf0(xP, xO))], (1859 ^ _229511) ^ [] : [-(sbrdtbr0(xP) = xk)], (1822 ^ _229511) ^ [_288501] : [aElementOf0(_288501, xO), 1826 ^ _229511 : [(1827 ^ _229511) ^ [] : [-(aElementOf0(1825 ^ [_288501], szNzAzT0))], (1829 ^ _229511) ^ [] : [-(aElementOf0(1825 ^ [_288501], sdtlbdtrb0(xd, szDzizrdt0(xd))))], (1831 ^ _229511) ^ [] : [-(sdtlpdtrp0(xe, 1825 ^ [_288501]) = _288501)]]], (1790 ^ _229511) ^ [] : [-(aFunction0(xd))], (1792 ^ _229511) ^ [] : [-(szDzozmdt0(xd) = szNzAzT0)], (1794 ^ _229511) ^ [_287641] : [aElementOf0(_287641, szNzAzT0), 1797 ^ _229511 : [(1798 ^ _229511) ^ [_287796] : [-(sdtlpdtrp0(xd, _287641) = sdtlpdtrp0(sdtlpdtrp0(xC, _287641), _287796)), aSet0(_287796), aElementOf0(_287796, slbdtsldtrb0(sdtlpdtrp0(xN, szszuzczcdt0(_287641)), xk))]]]], input).
% 101.36/98.69 ncf('1',plain,[aElementOf0(xP, slbdtsldtrb0(xO, xk))],start(1861 ^ 0)).
% 101.36/98.69 ncf('1.1',plain,[-(aElementOf0(xP, slbdtsldtrb0(xO, xk))), 1180 : aSubsetOf0(xP, xO), 1180 : sbrdtbr0(xP) = xk, 1180 : slbdtsldtrb0(xO, xk) = slbdtsldtrb0(xO, xk), 1166 : aSet0(xO), 1166 : aElementOf0(xk, szNzAzT0)],extension(1158 ^ 1,bind([[_265518, _265520, _265798, _266321], [xk, xO, slbdtsldtrb0(xO, xk), xP]]))).
% 101.36/98.69 ncf('1.1.1',plain,[-(aSubsetOf0(xP, xO))],extension(1857 ^ 6)).
% 101.36/98.69 ncf('1.1.2',plain,[-(sbrdtbr0(xP) = xk)],extension(1859 ^ 6)).
% 101.36/98.69 ncf('1.1.3',plain,[-(slbdtsldtrb0(xO, xk) = slbdtsldtrb0(xO, xk))],extension(2 ^ 4,bind([[_229655], [slbdtsldtrb0(xO, xk)]]))).
% 101.36/98.69 ncf('1.1.4',plain,[-(aSet0(xO))],extension(1814 ^ 2)).
% 101.36/98.69 ncf('1.1.5',plain,[-(aElementOf0(xk, szNzAzT0))],extension(1615 ^ 2)).
% 101.36/98.69 %-----------------------------------------------------
% 101.36/98.69 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------