%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM632+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri May 19 11:45:13 EDT 2023
% Result : Theorem 0.35s 1.39s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM632+1 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n020.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 18 17:41:17 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.35/1.39
% 0.35/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.35/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.35/1.39 %-----------------------------------------------------
% 0.35/1.39 ncf(matrix, plain, [(1875 ^ _230602) ^ [] : [sdtlpdtrp0(xc, xQ) = szDzizrdt0(xd)], (126 ^ _230602) ^ [_234623, _234625] : [_234625 = _234623, -(szmzazxdt0(_234625) = szmzazxdt0(_234623))], (132 ^ _230602) ^ [_234841, _234843] : [_234843 = _234841, -(slbdtrb0(_234843) = slbdtrb0(_234841))], (138 ^ _230602) ^ [_235087, _235089, _235091, _235093] : [-(sdtexdt0(_235093, _235089) = sdtexdt0(_235091, _235087)), _235093 = _235091, _235089 = _235087], (148 ^ _230602) ^ [_235446, _235448, _235450, _235452] : [-(sdtpldt0(_235452, _235448) = sdtpldt0(_235450, _235446)), _235452 = _235450, _235448 = _235446], (158 ^ _230602) ^ [_235805, _235807, _235809, _235811] : [-(sdtlcdtrc0(_235811, _235807) = sdtlcdtrc0(_235809, _235805)), _235811 = _235809, _235807 = _235805], (168 ^ _230602) ^ [_236136, _236138] : [_236138 = _236136, -(szDzozmdt0(_236138) = szDzozmdt0(_236136))], (174 ^ _230602) ^ [_236382, _236384, _236386, _236388] : [-(sdtmndt0(_236388, _236384) = sdtmndt0(_236386, _236382)), _236388 = _236386, _236384 = _236382], (184 ^ _230602) ^ [_236713, _236715] : [_236715 = _236713, -(szmzizndt0(_236715) = szmzizndt0(_236713))], (190 ^ _230602) ^ [_236931, _236933] : [_236933 = _236931, -(sbrdtbr0(_236933) = sbrdtbr0(_236931))], (196 ^ _230602) ^ [_237177, _237179, _237181, _237183] : [-(slbdtsldtrb0(_237183, _237179) = slbdtsldtrb0(_237181, _237177)), _237183 = _237181, _237179 = _237177], (206 ^ _230602) ^ [_237536, _237538, _237540, _237542] : [-(sdtlbdtrb0(_237542, _237538) = sdtlbdtrb0(_237540, _237536)), _237542 = _237540, _237538 = _237536], (216 ^ _230602) ^ [_237867, _237869] : [_237869 = _237867, -(szszuzczcdt0(_237869) = szszuzczcdt0(_237867))], (232 ^ _230602) ^ [_238424, _238426] : [_238426 = _238424, -(szDzizrdt0(_238426) = szDzizrdt0(_238424))], (222 ^ _230602) ^ [_238113, _238115, _238117, _238119] : [-(sdtlpdtrp0(_238119, _238115) = sdtlpdtrp0(_238117, _238113)), _238119 = _238117, _238115 = _238113], (2 ^ _230602) ^ [_230746] : [-(_230746 = _230746)], (4 ^ _230602) ^ [_230853, _230855] : [_230855 = _230853, -(_230853 = _230855)], (10 ^ _230602) ^ [_231057, _231059, _231061] : [-(_231061 = _231057), _231061 = _231059, _231059 = _231057], (20 ^ _230602) ^ [_231370, _231372] : [-(aElement0(_231370)), _231372 = _231370, aElement0(_231372)], (30 ^ _230602) ^ [_231665, _231667] : [-(isFinite0(_231665)), _231667 = _231665, isFinite0(_231667)], (40 ^ _230602) ^ [_231988, _231990, _231992, _231994] : [-(iLess0(_231992, _231988)), iLess0(_231994, _231990), _231994 = _231992, _231990 = _231988], (54 ^ _230602) ^ [_232432, _232434, _232436, _232438] : [-(sdtlseqdt0(_232436, _232432)), sdtlseqdt0(_232438, _232434), _232438 = _232436, _232434 = _232432], (68 ^ _230602) ^ [_232848, _232850] : [-(aFunction0(_232848)), _232850 = _232848, aFunction0(_232850)], (78 ^ _230602) ^ [_233143, _233145] : [-(isCountable0(_233143)), _233145 = _233143, isCountable0(_233145)], (88 ^ _230602) ^ [_233438, _233440] : [-(aSet0(_233438)), _233440 = _233438, aSet0(_233440)], (98 ^ _230602) ^ [_233761, _233763, _233765, _233767] : [-(aElementOf0(_233765, _233761)), aElementOf0(_233767, _233763), _233767 = _233765, _233763 = _233761], (112 ^ _230602) ^ [_234185, _234187, _234189, _234191] : [-(aSubsetOf0(_234189, _234185)), aSubsetOf0(_234191, _234187), _234191 = _234189, _234187 = _234185], (238 ^ _230602) ^ [_238714] : [aSet0(_238714), true___, -(true___)], (248 ^ _230602) ^ [_238969] : [aElement0(_238969), true___, -(true___)], (258 ^ _230602) ^ [_239224] : [aSet0(_239224), 261 ^ _230602 : [(262 ^ _230602) ^ [_239354] : [aElementOf0(_239354, _239224), -(aElement0(_239354))]]], (268 ^ _230602) ^ [_239555] : [aSet0(_239555), isFinite0(_239555), true___, -(true___)], (282 ^ _230602) ^ [_239925] : [_239925 = slcrc0, 285 ^ _230602 : [(286 ^ _230602) ^ [] : [-(aSet0(_239925))], (288 ^ _230602) ^ [_240106] : [aElementOf0(_240106, _239925)]]], (290 ^ _230602) ^ [_240174] : [-(_240174 = slcrc0), aSet0(_240174), -(aElementOf0(295 ^ [_240174], _240174))], (301 ^ _230602) ^ [] : [-(isFinite0(slcrc0))], (303 ^ _230602) ^ [_240556] : [aSet0(_240556), isCountable0(_240556), true___, -(true___)], (317 ^ _230602) ^ [_240897] : [isFinite0(_240897), aSet0(_240897), isCountable0(_240897)], (327 ^ _230602) ^ [_241167] : [_241167 = slcrc0, aSet0(_241167), isCountable0(_241167)], (337 ^ _230602) ^ [_241439] : [aSet0(_241439), 340 ^ _230602 : [(341 ^ _230602) ^ [_241615] : [aSubsetOf0(_241615, _241439), 344 ^ _230602 : [(345 ^ _230602) ^ [] : [-(aSet0(_241615))], (347 ^ _230602) ^ [_241824] : [aElementOf0(_241824, _241615), -(aElementOf0(_241824, _241439))]]], (353 ^ _230602) ^ [_242003] : [-(aSubsetOf0(_242003, _241439)), aSet0(_242003), 359 ^ _230602 : [(360 ^ _230602) ^ [] : [-(aElementOf0(358 ^ [_241439, _242003], _242003))], (362 ^ _230602) ^ [] : [aElementOf0(358 ^ [_241439, _242003], _241439)]]]]], (366 ^ _230602) ^ [_242440] : [aSet0(_242440), isFinite0(_242440), 373 ^ _230602 : [(374 ^ _230602) ^ [_242653] : [aSubsetOf0(_242653, _242440), -(isFinite0(_242653))]]], (380 ^ _230602) ^ [_242856] : [aSet0(_242856), -(aSubsetOf0(_242856, _242856))], (386 ^ _230602) ^ [_243058, _243060] : [aSet0(_243060), aSet0(_243058), -(_243060 = _243058), aSubsetOf0(_243060, _243058), aSubsetOf0(_243058, _243060)], (404 ^ _230602) ^ [_243547, _243549, _243551] : [aSet0(_243551), aSet0(_243549), aSet0(_243547), -(aSubsetOf0(_243551, _243547)), aSubsetOf0(_243551, _243549), aSubsetOf0(_243549, _243547)], (426 ^ _230602) ^ [_244133, _244135] : [aSet0(_244135), aElement0(_244133), 433 ^ _230602 : [(464 ^ _230602) ^ [_245394] : [-(_245394 = sdtpldt0(_244135, _244133)), aSet0(_245394), 472 ^ _230602 : [(473 ^ _230602) ^ [] : [-(aElementOf0(469 ^ [_244133, _244135, _245394], _245394))], (475 ^ _230602) ^ [] : [aElement0(469 ^ [_244133, _244135, _245394]), 478 ^ _230602 : [(479 ^ _230602) ^ [] : [aElementOf0(469 ^ [_244133, _244135, _245394], _244135)], (481 ^ _230602) ^ [] : [469 ^ [_244133, _244135, _245394] = _244133]]]], 482 ^ _230602 : [(491 ^ _230602) ^ [] : [aElementOf0(469 ^ [_244133, _244135, _245394], _245394)], (483 ^ _230602) ^ [] : [-(aElement0(469 ^ [_244133, _244135, _245394]))], (485 ^ _230602) ^ [] : [-(aElementOf0(469 ^ [_244133, _244135, _245394], _244135)), -(469 ^ [_244133, _244135, _245394] = _244133)]]], (434 ^ _230602) ^ [_244414] : [_244414 = sdtpldt0(_244135, _244133), 437 ^ _230602 : [(438 ^ _230602) ^ [] : [-(aSet0(_244414))], (440 ^ _230602) ^ [_244677] : [aElementOf0(_244677, _244414), 443 ^ _230602 : [(444 ^ _230602) ^ [] : [-(aElement0(_244677))], (446 ^ _230602) ^ [] : [-(aElementOf0(_244677, _244135)), -(_244677 = _244133)]]], (452 ^ _230602) ^ [_245032] : [-(aElementOf0(_245032, _244414)), aElement0(_245032), 457 ^ _230602 : [(458 ^ _230602) ^ [] : [aElementOf0(_245032, _244135)], (460 ^ _230602) ^ [] : [_245032 = _244133]]]]]]], (495 ^ _230602) ^ [_246431, _246433] : [aSet0(_246433), aElement0(_246431), 502 ^ _230602 : [(533 ^ _230602) ^ [_247699] : [-(_247699 = sdtmndt0(_246433, _246431)), aSet0(_247699), 553 ^ _230602 : [(554 ^ _230602) ^ [] : [-(aElement0(538 ^ [_246431, _246433, _247699]))], (556 ^ _230602) ^ [] : [-(aElementOf0(538 ^ [_246431, _246433, _247699], _246433))], (558 ^ _230602) ^ [] : [538 ^ [_246431, _246433, _247699] = _246431], (560 ^ _230602) ^ [] : [aElementOf0(538 ^ [_246431, _246433, _247699], _247699)]], 541 ^ _230602 : [(542 ^ _230602) ^ [] : [-(aElementOf0(538 ^ [_246431, _246433, _247699], _247699))], (544 ^ _230602) ^ [] : [aElement0(538 ^ [_246431, _246433, _247699]), aElementOf0(538 ^ [_246431, _246433, _247699], _246433), -(538 ^ [_246431, _246433, _247699] = _246431)]]], (503 ^ _230602) ^ [_246714] : [_246714 = sdtmndt0(_246433, _246431), 506 ^ _230602 : [(507 ^ _230602) ^ [] : [-(aSet0(_246714))], (509 ^ _230602) ^ [_246979] : [aElementOf0(_246979, _246714), 512 ^ _230602 : [(513 ^ _230602) ^ [] : [-(aElement0(_246979))], (515 ^ _230602) ^ [] : [-(aElementOf0(_246979, _246433))], (517 ^ _230602) ^ [] : [_246979 = _246431]]], (519 ^ _230602) ^ [_247315] : [-(aElementOf0(_247315, _246714)), aElement0(_247315), aElementOf0(_247315, _246433), -(_247315 = _246431)]]]]], (564 ^ _230602) ^ [_248729] : [aSet0(_248729), 567 ^ _230602 : [(568 ^ _230602) ^ [_248866] : [aElementOf0(_248866, _248729), -(sdtpldt0(sdtmndt0(_248729, _248866), _248866) = _248729)]]], (574 ^ _230602) ^ [_249095, _249097] : [aElement0(_249097), aSet0(_249095), -(aElementOf0(_249097, _249095)), -(sdtmndt0(sdtpldt0(_249095, _249097), _249097) = _249095)], (588 ^ _230602) ^ [_249482] : [aElement0(_249482), 591 ^ _230602 : [(592 ^ _230602) ^ [_249619] : [-(isCountable0(sdtpldt0(_249619, _249482))), aSet0(_249619), isCountable0(_249619)]]], (602 ^ _230602) ^ [_249911] : [aElement0(_249911), 605 ^ _230602 : [(606 ^ _230602) ^ [_250048] : [-(isCountable0(sdtmndt0(_250048, _249911))), aSet0(_250048), isCountable0(_250048)]]], (616 ^ _230602) ^ [_250340] : [aElement0(_250340), 619 ^ _230602 : [(620 ^ _230602) ^ [_250477] : [-(isFinite0(sdtpldt0(_250477, _250340))), aSet0(_250477), isFinite0(_250477)]]], (630 ^ _230602) ^ [_250769] : [aElement0(_250769), 633 ^ _230602 : [(634 ^ _230602) ^ [_250906] : [-(isFinite0(sdtmndt0(_250906, _250769))), aSet0(_250906), isFinite0(_250906)]]], (644 ^ _230602) ^ [] : [-(aSet0(szNzAzT0))], (646 ^ _230602) ^ [] : [-(isCountable0(szNzAzT0))], (648 ^ _230602) ^ [] : [-(aElementOf0(sz00, szNzAzT0))], (650 ^ _230602) ^ [_251359] : [aElementOf0(_251359, szNzAzT0), 653 ^ _230602 : [(654 ^ _230602) ^ [] : [-(aElementOf0(szszuzczcdt0(_251359), szNzAzT0))], (656 ^ _230602) ^ [] : [szszuzczcdt0(_251359) = sz00]]], (658 ^ _230602) ^ [_251645, _251647] : [aElementOf0(_251647, szNzAzT0), aElementOf0(_251645, szNzAzT0), szszuzczcdt0(_251647) = szszuzczcdt0(_251645), -(_251647 = _251645)], (672 ^ _230602) ^ [_252029] : [aElementOf0(_252029, szNzAzT0), -(_252029 = sz00), 680 ^ _230602 : [(681 ^ _230602) ^ [] : [-(aElementOf0(679 ^ [_252029], szNzAzT0))], (683 ^ _230602) ^ [] : [-(_252029 = szszuzczcdt0(679 ^ [_252029]))]]], (685 ^ _230602) ^ [_252446] : [aElementOf0(_252446, szNzAzT0), _252446 = szszuzczcdt0(_252446)], (691 ^ _230602) ^ [_252655, _252657] : [aElementOf0(_252657, szNzAzT0), aElementOf0(_252655, szNzAzT0), sdtlseqdt0(_252657, _252655), true___, -(true___)], (709 ^ _230602) ^ [_253105] : [aElementOf0(_253105, szNzAzT0), -(sdtlseqdt0(sz00, _253105))], (715 ^ _230602) ^ [_253295] : [aElementOf0(_253295, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_253295), sz00)], (721 ^ _230602) ^ [_253504, _253506] : [aElementOf0(_253506, szNzAzT0), aElementOf0(_253504, szNzAzT0), 728 ^ _230602 : [(729 ^ _230602) ^ [] : [sdtlseqdt0(_253506, _253504), -(sdtlseqdt0(szszuzczcdt0(_253506), szszuzczcdt0(_253504)))], (735 ^ _230602) ^ [] : [sdtlseqdt0(szszuzczcdt0(_253506), szszuzczcdt0(_253504)), -(sdtlseqdt0(_253506, _253504))]]], (741 ^ _230602) ^ [_254053] : [aElementOf0(_254053, szNzAzT0), -(sdtlseqdt0(_254053, szszuzczcdt0(_254053)))], (747 ^ _230602) ^ [_254247] : [aElementOf0(_254247, szNzAzT0), -(sdtlseqdt0(_254247, _254247))], (753 ^ _230602) ^ [_254451, _254453] : [aElementOf0(_254453, szNzAzT0), aElementOf0(_254451, szNzAzT0), -(_254453 = _254451), sdtlseqdt0(_254453, _254451), sdtlseqdt0(_254451, _254453)], (771 ^ _230602) ^ [_254944, _254946, _254948] : [aElementOf0(_254948, szNzAzT0), aElementOf0(_254946, szNzAzT0), aElementOf0(_254944, szNzAzT0), -(sdtlseqdt0(_254948, _254944)), sdtlseqdt0(_254948, _254946), sdtlseqdt0(_254946, _254944)], (793 ^ _230602) ^ [_255536, _255538] : [aElementOf0(_255538, szNzAzT0), aElementOf0(_255536, szNzAzT0), -(sdtlseqdt0(_255538, _255536)), -(sdtlseqdt0(szszuzczcdt0(_255536), _255538))], (807 ^ _230602) ^ [_255931, _255933] : [aElementOf0(_255933, szNzAzT0), aElementOf0(_255931, szNzAzT0), iLess0(_255933, _255931), true___, -(true___)], (825 ^ _230602) ^ [_256381] : [aElementOf0(_256381, szNzAzT0), -(iLess0(_256381, szszuzczcdt0(_256381)))], (831 ^ _230602) ^ [_256575] : [aSet0(_256575), -(aElement0(sbrdtbr0(_256575)))], (837 ^ _230602) ^ [_256765] : [aSet0(_256765), 840 ^ _230602 : [(841 ^ _230602) ^ [] : [aElementOf0(sbrdtbr0(_256765), szNzAzT0), -(isFinite0(_256765))], (847 ^ _230602) ^ [] : [isFinite0(_256765), -(aElementOf0(sbrdtbr0(_256765), szNzAzT0))]]], (853 ^ _230602) ^ [_257196] : [aSet0(_257196), 856 ^ _230602 : [(857 ^ _230602) ^ [] : [sbrdtbr0(_257196) = sz00, -(_257196 = slcrc0)], (863 ^ _230602) ^ [] : [_257196 = slcrc0, -(sbrdtbr0(_257196) = sz00)]]], (869 ^ _230602) ^ [_257630] : [aSet0(_257630), isFinite0(_257630), 876 ^ _230602 : [(877 ^ _230602) ^ [_257860] : [aElement0(_257860), -(aElementOf0(_257860, _257630)), -(sbrdtbr0(sdtpldt0(_257630, _257860)) = szszuzczcdt0(sbrdtbr0(_257630)))]]], (887 ^ _230602) ^ [_258173] : [aSet0(_258173), 890 ^ _230602 : [(891 ^ _230602) ^ [_258318] : [-(szszuzczcdt0(sbrdtbr0(sdtmndt0(_258173, _258318))) = sbrdtbr0(_258173)), isFinite0(_258173), aElementOf0(_258318, _258173)]]], (901 ^ _230602) ^ [_258626] : [aSet0(_258626), 904 ^ _230602 : [(905 ^ _230602) ^ [_258766] : [-(sdtlseqdt0(sbrdtbr0(_258766), sbrdtbr0(_258626))), isFinite0(_258626), aSubsetOf0(_258766, _258626)]]], (915 ^ _230602) ^ [_259078, _259080] : [aSet0(_259080), aElementOf0(_259078, szNzAzT0), 931 ^ _230602 : [(932 ^ _230602) ^ [] : [-(aSubsetOf0(930 ^ [_259078, _259080], _259080))], (934 ^ _230602) ^ [] : [-(sbrdtbr0(930 ^ [_259078, _259080]) = _259078)]], isFinite0(_259080), sdtlseqdt0(_259078, sbrdtbr0(_259080))], (936 ^ _230602) ^ [_259694] : [aSubsetOf0(_259694, szNzAzT0), -(_259694 = slcrc0), 943 ^ _230602 : [(944 ^ _230602) ^ [_259963] : [_259963 = szmzizndt0(_259694), 947 ^ _230602 : [(948 ^ _230602) ^ [] : [-(aElementOf0(_259963, _259694))], (950 ^ _230602) ^ [_260178] : [aElementOf0(_260178, _259694), -(sdtlseqdt0(_259963, _260178))]]], (956 ^ _230602) ^ [_260357] : [-(_260357 = szmzizndt0(_259694)), aElementOf0(_260357, _259694), 962 ^ _230602 : [(963 ^ _230602) ^ [] : [-(aElementOf0(961 ^ [_259694, _260357], _259694))], (965 ^ _230602) ^ [] : [sdtlseqdt0(_260357, 961 ^ [_259694, _260357])]]]]], (969 ^ _230602) ^ [_260802] : [aSubsetOf0(_260802, szNzAzT0), isFinite0(_260802), -(_260802 = slcrc0), 980 ^ _230602 : [(981 ^ _230602) ^ [_261154] : [_261154 = szmzazxdt0(_260802), 984 ^ _230602 : [(985 ^ _230602) ^ [] : [-(aElementOf0(_261154, _260802))], (987 ^ _230602) ^ [_261369] : [aElementOf0(_261369, _260802), -(sdtlseqdt0(_261369, _261154))]]], (993 ^ _230602) ^ [_261548] : [-(_261548 = szmzazxdt0(_260802)), aElementOf0(_261548, _260802), 999 ^ _230602 : [(1000 ^ _230602) ^ [] : [-(aElementOf0(998 ^ [_260802, _261548], _260802))], (1002 ^ _230602) ^ [] : [sdtlseqdt0(998 ^ [_260802, _261548], _261548)]]]]], (1006 ^ _230602) ^ [_262009, _262011] : [-(szmzizndt0(_262011) = szmzizndt0(_262009)), aElementOf0(szmzizndt0(_262011), _262009), aElementOf0(szmzizndt0(_262009), _262011), aSubsetOf0(_262011, szNzAzT0), aSubsetOf0(_262009, szNzAzT0), -(_262011 = slcrc0), -(_262009 = slcrc0)], (1032 ^ _230602) ^ [_262676] : [aElementOf0(_262676, szNzAzT0), 1035 ^ _230602 : [(1060 ^ _230602) ^ [_263645] : [-(_263645 = slbdtrb0(_262676)), aSet0(_263645), 1076 ^ _230602 : [(1077 ^ _230602) ^ [] : [-(aElementOf0(1065 ^ [_262676, _263645], szNzAzT0))], (1079 ^ _230602) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(1065 ^ [_262676, _263645]), _262676))], (1081 ^ _230602) ^ [] : [aElementOf0(1065 ^ [_262676, _263645], _263645)]], 1068 ^ _230602 : [(1069 ^ _230602) ^ [] : [-(aElementOf0(1065 ^ [_262676, _263645], _263645))], (1071 ^ _230602) ^ [] : [aElementOf0(1065 ^ [_262676, _263645], szNzAzT0), sdtlseqdt0(szszuzczcdt0(1065 ^ [_262676, _263645]), _262676)]]], (1036 ^ _230602) ^ [_262864] : [_262864 = slbdtrb0(_262676), 1039 ^ _230602 : [(1040 ^ _230602) ^ [] : [-(aSet0(_262864))], (1042 ^ _230602) ^ [_263114] : [aElementOf0(_263114, _262864), 1045 ^ _230602 : [(1046 ^ _230602) ^ [] : [-(aElementOf0(_263114, szNzAzT0))], (1048 ^ _230602) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(_263114), _262676))]]], (1050 ^ _230602) ^ [_263367] : [-(aElementOf0(_263367, _262864)), aElementOf0(_263367, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_263367), _262676)]]]]], (1085 ^ _230602) ^ [_264448] : [aElementOf0(_264448, szNzAzT0), -(isFinite0(slbdtrb0(_264448)))], (1091 ^ _230602) ^ [] : [-(slbdtrb0(sz00) = slcrc0)], (1093 ^ _230602) ^ [_264707, _264709] : [aElementOf0(_264709, szNzAzT0), aElementOf0(_264707, szNzAzT0), 1100 ^ _230602 : [(1111 ^ _230602) ^ [] : [1112 ^ _230602 : [(1113 ^ _230602) ^ [] : [aElementOf0(_264709, slbdtrb0(_264707))], (1115 ^ _230602) ^ [] : [_264709 = _264707]], -(aElementOf0(_264709, slbdtrb0(szszuzczcdt0(_264707))))], (1101 ^ _230602) ^ [] : [aElementOf0(_264709, slbdtrb0(szszuzczcdt0(_264707))), -(aElementOf0(_264709, slbdtrb0(_264707))), -(_264709 = _264707)]]], (1119 ^ _230602) ^ [_265434, _265436] : [aElementOf0(_265436, szNzAzT0), aElementOf0(_265434, szNzAzT0), 1126 ^ _230602 : [(1127 ^ _230602) ^ [] : [sdtlseqdt0(_265436, _265434), -(aSubsetOf0(slbdtrb0(_265436), slbdtrb0(_265434)))], (1133 ^ _230602) ^ [] : [aSubsetOf0(slbdtrb0(_265436), slbdtrb0(_265434)), -(sdtlseqdt0(_265436, _265434))]]], (1139 ^ _230602) ^ [_265983] : [1147 ^ _230602 : [(1148 ^ _230602) ^ [] : [-(aElementOf0(1146 ^ [_265983], szNzAzT0))], (1150 ^ _230602) ^ [] : [-(aSubsetOf0(_265983, slbdtrb0(1146 ^ [_265983])))]], aSubsetOf0(_265983, szNzAzT0), isFinite0(_265983)], (1152 ^ _230602) ^ [_266397] : [aElementOf0(_266397, szNzAzT0), -(sbrdtbr0(slbdtrb0(_266397)) = _266397)], (1158 ^ _230602) ^ [_266609, _266611] : [aSet0(_266611), aElementOf0(_266609, szNzAzT0), 1165 ^ _230602 : [(1190 ^ _230602) ^ [_267702] : [-(_267702 = slbdtsldtrb0(_266611, _266609)), aSet0(_267702), 1206 ^ _230602 : [(1207 ^ _230602) ^ [] : [-(aSubsetOf0(1195 ^ [_266609, _266611, _267702], _266611))], (1209 ^ _230602) ^ [] : [-(sbrdtbr0(1195 ^ [_266609, _266611, _267702]) = _266609)], (1211 ^ _230602) ^ [] : [aElementOf0(1195 ^ [_266609, _266611, _267702], _267702)]], 1198 ^ _230602 : [(1199 ^ _230602) ^ [] : [-(aElementOf0(1195 ^ [_266609, _266611, _267702], _267702))], (1201 ^ _230602) ^ [] : [aSubsetOf0(1195 ^ [_266609, _266611, _267702], _266611), sbrdtbr0(1195 ^ [_266609, _266611, _267702]) = _266609]]], (1166 ^ _230602) ^ [_266889] : [_266889 = slbdtsldtrb0(_266611, _266609), 1169 ^ _230602 : [(1170 ^ _230602) ^ [] : [-(aSet0(_266889))], (1172 ^ _230602) ^ [_267149] : [aElementOf0(_267149, _266889), 1175 ^ _230602 : [(1176 ^ _230602) ^ [] : [-(aSubsetOf0(_267149, _266611))], (1178 ^ _230602) ^ [] : [-(sbrdtbr0(_267149) = _266609)]]], (1180 ^ _230602) ^ [_267412] : [-(aElementOf0(_267412, _266889)), aSubsetOf0(_267412, _266611), sbrdtbr0(_267412) = _266609]]]]], (1215 ^ _230602) ^ [_268551] : [aSet0(_268551), isFinite0(_268551), 1222 ^ _230602 : [(1223 ^ _230602) ^ [_268767] : [aElementOf0(_268767, szNzAzT0), -(isFinite0(slbdtsldtrb0(_268551, _268767)))]]], (1229 ^ _230602) ^ [_268976] : [aSet0(_268976), -(isFinite0(_268976)), 1236 ^ _230602 : [(1237 ^ _230602) ^ [_269198] : [aElementOf0(_269198, szNzAzT0), slbdtsldtrb0(_268976, _269198) = slcrc0]]], (1243 ^ _230602) ^ [_269410] : [aSet0(_269410), isCountable0(_269410), 1250 ^ _230602 : [(1251 ^ _230602) ^ [_269634] : [-(isCountable0(slbdtsldtrb0(_269410, _269634))), aElementOf0(_269634, szNzAzT0), -(_269634 = sz00)]]], (1261 ^ _230602) ^ [_269935] : [aElementOf0(_269935, szNzAzT0), 1264 ^ _230602 : [(1265 ^ _230602) ^ [_270122, _270124] : [aSet0(_270124), aSet0(_270122), -(_269935 = sz00), -(aSubsetOf0(_270124, _270122)), aSubsetOf0(slbdtsldtrb0(_270124, _269935), slbdtsldtrb0(_270122, _269935)), -(slbdtsldtrb0(_270124, _269935) = slcrc0)]]], (1287 ^ _230602) ^ [_270741, _270743] : [aSet0(_270743), aElementOf0(_270741, szNzAzT0), 1294 ^ _230602 : [(1295 ^ _230602) ^ [_270992] : [1303 ^ _230602 : [(1304 ^ _230602) ^ [] : [-(aSubsetOf0(1302 ^ [_270741, _270743, _270992], _270743))], (1306 ^ _230602) ^ [] : [-(isFinite0(1302 ^ [_270741, _270743, _270992]))], (1308 ^ _230602) ^ [] : [-(aSubsetOf0(_270992, slbdtsldtrb0(1302 ^ [_270741, _270743, _270992], _270741)))]], aSubsetOf0(_270992, slbdtsldtrb0(_270743, _270741)), isFinite0(_270992)]]], (1310 ^ _230602) ^ [_271554] : [aFunction0(_271554), true___, -(true___)], (1320 ^ _230602) ^ [_271809] : [aFunction0(_271809), -(aSet0(szDzozmdt0(_271809)))], (1326 ^ _230602) ^ [_271999] : [aFunction0(_271999), 1329 ^ _230602 : [(1330 ^ _230602) ^ [_272134] : [aElementOf0(_272134, szDzozmdt0(_271999)), -(aElement0(sdtlpdtrp0(_271999, _272134)))]]], (1336 ^ _230602) ^ [_272359, _272361] : [aFunction0(_272361), aElement0(_272359), 1343 ^ _230602 : [(1368 ^ _230602) ^ [_273468] : [-(_273468 = sdtlbdtrb0(_272361, _272359)), aSet0(_273468), 1384 ^ _230602 : [(1385 ^ _230602) ^ [] : [-(aElementOf0(1373 ^ [_272359, _272361, _273468], szDzozmdt0(_272361)))], (1387 ^ _230602) ^ [] : [-(sdtlpdtrp0(_272361, 1373 ^ [_272359, _272361, _273468]) = _272359)], (1389 ^ _230602) ^ [] : [aElementOf0(1373 ^ [_272359, _272361, _273468], _273468)]], 1376 ^ _230602 : [(1377 ^ _230602) ^ [] : [-(aElementOf0(1373 ^ [_272359, _272361, _273468], _273468))], (1379 ^ _230602) ^ [] : [aElementOf0(1373 ^ [_272359, _272361, _273468], szDzozmdt0(_272361)), sdtlpdtrp0(_272361, 1373 ^ [_272359, _272361, _273468]) = _272359]]], (1344 ^ _230602) ^ [_272640] : [_272640 = sdtlbdtrb0(_272361, _272359), 1347 ^ _230602 : [(1348 ^ _230602) ^ [] : [-(aSet0(_272640))], (1350 ^ _230602) ^ [_272903] : [aElementOf0(_272903, _272640), 1353 ^ _230602 : [(1354 ^ _230602) ^ [] : [-(aElementOf0(_272903, szDzozmdt0(_272361)))], (1356 ^ _230602) ^ [] : [-(sdtlpdtrp0(_272361, _272903) = _272359)]]], (1358 ^ _230602) ^ [_273172] : [-(aElementOf0(_273172, _272640)), aElementOf0(_273172, szDzozmdt0(_272361)), sdtlpdtrp0(_272361, _273172) = _272359]]]]], (1393 ^ _230602) ^ [_274343, _274345] : [-(aSubsetOf0(sdtlbdtrb0(_274345, _274343), szDzozmdt0(_274345))), aFunction0(_274345), aElement0(_274343)], (1403 ^ _230602) ^ [_274634] : [aFunction0(_274634), 1406 ^ _230602 : [(1407 ^ _230602) ^ [_274811] : [aSubsetOf0(_274811, szDzozmdt0(_274634)), 1410 ^ _230602 : [(1436 ^ _230602) ^ [_275998] : [-(_275998 = sdtlcdtrc0(_274634, _274811)), aSet0(_275998), 1453 ^ _230602 : [(1454 ^ _230602) ^ [] : [-(aElementOf0(1452 ^ [_274634, _274811, _275998], _274811))], (1456 ^ _230602) ^ [] : [-(sdtlpdtrp0(_274634, 1452 ^ [_274634, _274811, _275998]) = 1441 ^ [_274634, _274811, _275998])], (1458 ^ _230602) ^ [] : [aElementOf0(1441 ^ [_274634, _274811, _275998], _275998)]], 1444 ^ _230602 : [(1445 ^ _230602) ^ [] : [-(aElementOf0(1441 ^ [_274634, _274811, _275998], _275998))], (1447 ^ _230602) ^ [_276391] : [aElementOf0(_276391, _274811), sdtlpdtrp0(_274634, _276391) = 1441 ^ [_274634, _274811, _275998]]]], (1411 ^ _230602) ^ [_275016] : [_275016 = sdtlcdtrc0(_274634, _274811), 1414 ^ _230602 : [(1415 ^ _230602) ^ [] : [-(aSet0(_275016))], (1417 ^ _230602) ^ [_275282] : [aElementOf0(_275282, _275016), 1421 ^ _230602 : [(1422 ^ _230602) ^ [] : [-(aElementOf0(1420 ^ [_274634, _274811, _275016, _275282], _274811))], (1424 ^ _230602) ^ [] : [-(sdtlpdtrp0(_274634, 1420 ^ [_274634, _274811, _275016, _275282]) = _275282)]]], (1426 ^ _230602) ^ [_275636] : [-(aElementOf0(_275636, _275016)), 1427 ^ _230602 : [(1428 ^ _230602) ^ [_275741] : [aElementOf0(_275741, _274811), sdtlpdtrp0(_274634, _275741) = _275636]]]]]]]]], (1462 ^ _230602) ^ [_277002] : [aFunction0(_277002), 1465 ^ _230602 : [(1466 ^ _230602) ^ [_277143] : [aElementOf0(_277143, szDzozmdt0(_277002)), -(aElementOf0(sdtlpdtrp0(_277002, _277143), sdtlcdtrc0(_277002, szDzozmdt0(_277002))))]]], (1472 ^ _230602) ^ [_277366] : [aFunction0(_277366), 1475 ^ _230602 : [(1476 ^ _230602) ^ [_277543] : [aSubsetOf0(_277543, szDzozmdt0(_277366)), 1479 ^ _230602 : [(1480 ^ _230602) ^ [_277748] : [_277748 = sdtexdt0(_277366, _277543), 1483 ^ _230602 : [(1484 ^ _230602) ^ [] : [-(aFunction0(_277748))], (1486 ^ _230602) ^ [] : [-(szDzozmdt0(_277748) = _277543)], (1488 ^ _230602) ^ [_278055] : [aElementOf0(_278055, _277543), -(sdtlpdtrp0(_277748, _278055) = sdtlpdtrp0(_277366, _278055))]]], (1494 ^ _230602) ^ [_278256] : [-(_278256 = sdtexdt0(_277366, _277543)), aFunction0(_278256), szDzozmdt0(_278256) = _277543, 1504 ^ _230602 : [(1505 ^ _230602) ^ [] : [-(aElementOf0(1503 ^ [_277366, _277543, _278256], _277543))], (1507 ^ _230602) ^ [] : [sdtlpdtrp0(_278256, 1503 ^ [_277366, _277543, _278256]) = sdtlpdtrp0(_277366, 1503 ^ [_277366, _277543, _278256])]]]]]]], (1511 ^ _230602) ^ [_278850] : [aFunction0(_278850), 1514 ^ _230602 : [(1515 ^ _230602) ^ [_279038] : [aSubsetOf0(_279038, szDzozmdt0(_278850)), isCountable0(_279038), 1526 ^ _230602 : [(1527 ^ _230602) ^ [] : [-(aElementOf0(1524 ^ [_278850, _279038], szDzozmdt0(_278850)))], (1529 ^ _230602) ^ [] : [-(aElementOf0(1525 ^ [_278850, _279038], szDzozmdt0(_278850)))], (1531 ^ _230602) ^ [] : [1524 ^ [_278850, _279038] = 1525 ^ [_278850, _279038]], (1533 ^ _230602) ^ [] : [-(sdtlpdtrp0(_278850, 1524 ^ [_278850, _279038]) = sdtlpdtrp0(_278850, 1525 ^ [_278850, _279038]))]], -(isCountable0(sdtlcdtrc0(_278850, _279038)))]]], (1537 ^ _230602) ^ [_279910] : [aFunction0(_279910), 1548 ^ _230602 : [(1549 ^ _230602) ^ [] : [-(aElement0(szDzizrdt0(_279910)))], (1551 ^ _230602) ^ [] : [-(isCountable0(sdtlbdtrb0(_279910, szDzizrdt0(_279910))))]], isCountable0(szDzozmdt0(_279910)), isFinite0(sdtlcdtrc0(_279910, szDzozmdt0(_279910)))], (1553 ^ _230602) ^ [] : [-(aSet0(xT))], (1555 ^ _230602) ^ [] : [-(isFinite0(xT))], (1557 ^ _230602) ^ [] : [-(aElementOf0(xK, szNzAzT0))], (1559 ^ _230602) ^ [] : [-(aSubsetOf0(xS, szNzAzT0))], (1561 ^ _230602) ^ [] : [-(isCountable0(xS))], (1563 ^ _230602) ^ [] : [-(aFunction0(xc))], (1565 ^ _230602) ^ [] : [-(szDzozmdt0(xc) = slbdtsldtrb0(xS, xK))], (1567 ^ _230602) ^ [] : [-(aSubsetOf0(sdtlcdtrc0(xc, szDzozmdt0(xc)), xT))], (1569 ^ _230602) ^ [_280793] : [aElementOf0(_280793, szNzAzT0), 1572 ^ _230602 : [(1573 ^ _230602) ^ [_281013] : [aSubsetOf0(_281013, szNzAzT0), isCountable0(_281013), 1580 ^ _230602 : [(1581 ^ _230602) ^ [_281310] : [aFunction0(_281310), szDzozmdt0(_281310) = slbdtsldtrb0(_281013, _280793), aSubsetOf0(sdtlcdtrc0(_281310, szDzozmdt0(_281310)), xT), iLess0(_280793, xK), 1597 ^ _230602 : [(1598 ^ _230602) ^ [] : [-(aElementOf0(1596 ^ [_280793, _281013, _281310], xT))], (1601 ^ _230602) ^ [] : [-(aSubsetOf0(1599 ^ [_280793, _281013, _281310], _281013))], (1603 ^ _230602) ^ [] : [-(isCountable0(1599 ^ [_280793, _281013, _281310]))], (1605 ^ _230602) ^ [_282185] : [aElementOf0(_282185, slbdtsldtrb0(1599 ^ [_280793, _281013, _281310], _280793)), -(sdtlpdtrp0(_281310, _282185) = 1596 ^ [_280793, _281013, _281310])]]]]]]], (1611 ^ _230602) ^ [] : [xK = sz00], (1613 ^ _230602) ^ [] : [xK = sz00], (1615 ^ _230602) ^ [] : [-(aElementOf0(xk, szNzAzT0))], (1617 ^ _230602) ^ [] : [-(szszuzczcdt0(xk) = xK)], (1619 ^ _230602) ^ [] : [-(aFunction0(xN))], (1621 ^ _230602) ^ [] : [-(szDzozmdt0(xN) = szNzAzT0)], (1623 ^ _230602) ^ [] : [-(sdtlpdtrp0(xN, sz00) = xS)], (1625 ^ _230602) ^ [_282849] : [aElementOf0(_282849, szNzAzT0), 1636 ^ _230602 : [(1637 ^ _230602) ^ [] : [-(aSubsetOf0(sdtlpdtrp0(xN, szszuzczcdt0(_282849)), sdtmndt0(sdtlpdtrp0(xN, _282849), szmzizndt0(sdtlpdtrp0(xN, _282849)))))], (1639 ^ _230602) ^ [] : [-(isCountable0(sdtlpdtrp0(xN, szszuzczcdt0(_282849))))]], aSubsetOf0(sdtlpdtrp0(xN, _282849), szNzAzT0), isCountable0(sdtlpdtrp0(xN, _282849))], (1641 ^ _230602) ^ [_283338] : [aElementOf0(_283338, szNzAzT0), 1644 ^ _230602 : [(1645 ^ _230602) ^ [] : [-(aSubsetOf0(sdtlpdtrp0(xN, _283338), szNzAzT0))], (1647 ^ _230602) ^ [] : [-(isCountable0(sdtlpdtrp0(xN, _283338)))]]], (1649 ^ _230602) ^ [_283625, _283627] : [aElementOf0(_283627, szNzAzT0), aElementOf0(_283625, szNzAzT0), sdtlseqdt0(_283625, _283627), -(aSubsetOf0(sdtlpdtrp0(xN, _283627), sdtlpdtrp0(xN, _283625)))], (1663 ^ _230602) ^ [_284027, _284029] : [szmzizndt0(sdtlpdtrp0(xN, _284029)) = szmzizndt0(sdtlpdtrp0(xN, _284027)), aElementOf0(_284029, szNzAzT0), aElementOf0(_284027, szNzAzT0), -(_284029 = _284027)], (1677 ^ _230602) ^ [_284425] : [aElementOf0(_284425, szNzAzT0), 1680 ^ _230602 : [(1681 ^ _230602) ^ [_284585] : [-(aElementOf0(sdtpldt0(_284585, szmzizndt0(sdtlpdtrp0(xN, _284425))), slbdtsldtrb0(xS, xK))), aSet0(_284585), aElementOf0(_284585, slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _284425), szmzizndt0(sdtlpdtrp0(xN, _284425))), xk))]]], (1691 ^ _230602) ^ [] : [-(aFunction0(xC))], (1693 ^ _230602) ^ [] : [-(szDzozmdt0(xC) = szNzAzT0)], (1695 ^ _230602) ^ [_285025] : [aElementOf0(_285025, szNzAzT0), 1698 ^ _230602 : [(1699 ^ _230602) ^ [] : [-(aFunction0(sdtlpdtrp0(xC, _285025)))], (1701 ^ _230602) ^ [] : [-(szDzozmdt0(sdtlpdtrp0(xC, _285025)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _285025), szmzizndt0(sdtlpdtrp0(xN, _285025))), xk))], (1703 ^ _230602) ^ [_285376] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _285025), _285376) = sdtlpdtrp0(xc, sdtpldt0(_285376, szmzizndt0(sdtlpdtrp0(xN, _285025))))), aSet0(_285376), aElementOf0(_285376, slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _285025), szmzizndt0(sdtlpdtrp0(xN, _285025))), xk))]]], (1713 ^ _230602) ^ [_285736] : [aElementOf0(_285736, szNzAzT0), -(aSubsetOf0(sdtlcdtrc0(sdtlpdtrp0(xC, _285736), szDzozmdt0(sdtlpdtrp0(xC, _285736))), xT))], (1719 ^ _230602) ^ [_285948] : [aElementOf0(_285948, szNzAzT0), 1722 ^ _230602 : [(1723 ^ _230602) ^ [_286130] : [aSubsetOf0(_286130, sdtmndt0(sdtlpdtrp0(xN, _285948), szmzizndt0(sdtlpdtrp0(xN, _285948)))), isCountable0(_286130), 1730 ^ _230602 : [(1731 ^ _230602) ^ [_286400] : [-(aElementOf0(_286400, slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _285948), szmzizndt0(sdtlpdtrp0(xN, _285948))), xk))), aSet0(_286400), aElementOf0(_286400, slbdtsldtrb0(_286130, xk))]]]]], (1741 ^ _230602) ^ [_286743] : [aElementOf0(_286743, szNzAzT0), 1745 ^ _230602 : [(1746 ^ _230602) ^ [] : [-(aElementOf0(1744 ^ [_286743], xT))], (1749 ^ _230602) ^ [] : [-(aSubsetOf0(1747 ^ [_286743], sdtmndt0(sdtlpdtrp0(xN, _286743), szmzizndt0(sdtlpdtrp0(xN, _286743)))))], (1751 ^ _230602) ^ [] : [-(isCountable0(1747 ^ [_286743]))], (1753 ^ _230602) ^ [_287337] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _286743), _287337) = 1744 ^ [_286743]), aSet0(_287337), aElementOf0(_287337, slbdtsldtrb0(1747 ^ [_286743], xk))]]], (1763 ^ _230602) ^ [_287671] : [aElementOf0(_287671, szNzAzT0), 1767 ^ _230602 : [(1768 ^ _230602) ^ [] : [-(aElementOf0(1766 ^ [_287671], xT))], (1770 ^ _230602) ^ [_287980] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _287671), _287980) = 1766 ^ [_287671]), aSet0(_287980), aElementOf0(_287980, slbdtsldtrb0(sdtlpdtrp0(xN, szszuzczcdt0(_287671)), xk))]]], (1780 ^ _230602) ^ [] : [-(aFunction0(xe))], (1782 ^ _230602) ^ [] : [-(szDzozmdt0(xe) = szNzAzT0)], (1784 ^ _230602) ^ [_288416] : [aElementOf0(_288416, szNzAzT0), -(sdtlpdtrp0(xe, _288416) = szmzizndt0(sdtlpdtrp0(xN, _288416)))], (1808 ^ _230602) ^ [] : [-(aSubsetOf0(sdtlcdtrc0(xd, szDzozmdt0(xd)), xT))], (1810 ^ _230602) ^ [] : [-(aElementOf0(szDzizrdt0(xd), xT))], (1812 ^ _230602) ^ [] : [-(isCountable0(sdtlbdtrb0(xd, szDzizrdt0(xd))))], (1814 ^ _230602) ^ [] : [-(aSet0(xO))], (1816 ^ _230602) ^ [] : [-(xO = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))], (1818 ^ _230602) ^ [] : [-(aSet0(xO))], (1820 ^ _230602) ^ [] : [-(isCountable0(xO))], (1833 ^ _230602) ^ [] : [-(aSubsetOf0(xO, xS))], (1835 ^ _230602) ^ [] : [-(aElementOf0(xQ, slbdtsldtrb0(xO, xK)))], (1837 ^ _230602) ^ [] : [-(aSubsetOf0(xQ, xO))], (1839 ^ _230602) ^ [] : [xQ = slcrc0], (1841 ^ _230602) ^ [] : [-(aSubsetOf0(xQ, szNzAzT0))], (1843 ^ _230602) ^ [] : [-(aElementOf0(xQ, szDzozmdt0(xc)))], (1845 ^ _230602) ^ [] : [-(xp = szmzizndt0(xQ))], (1847 ^ _230602) ^ [] : [-(aSet0(xP))], (1849 ^ _230602) ^ [] : [-(xP = sdtmndt0(xQ, szmzizndt0(xQ)))], (1851 ^ _230602) ^ [] : [-(aElementOf0(xp, xQ))], (1853 ^ _230602) ^ [] : [-(aElementOf0(xp, xO))], (1855 ^ _230602) ^ [] : [-(aSubsetOf0(xP, xQ))], (1857 ^ _230602) ^ [] : [-(aSubsetOf0(xP, xO))], (1859 ^ _230602) ^ [] : [-(sbrdtbr0(xP) = xk)], (1861 ^ _230602) ^ [] : [-(aElementOf0(xP, slbdtsldtrb0(xO, xk)))], (1863 ^ _230602) ^ [] : [-(aElementOf0(xn, sdtlbdtrb0(xd, szDzizrdt0(xd))))], (1865 ^ _230602) ^ [] : [-(aElementOf0(xn, szNzAzT0))], (1867 ^ _230602) ^ [] : [-(sdtlpdtrp0(xe, xn) = xp)], (1869 ^ _230602) ^ [] : [-(sdtlpdtrp0(xd, xn) = szDzizrdt0(xd))], (1871 ^ _230602) ^ [] : [-(aSubsetOf0(xP, sdtlpdtrp0(xN, szszuzczcdt0(xn))))], (1873 ^ _230602) ^ [] : [-(sdtlpdtrp0(xc, xQ) = sdtlpdtrp0(xd, xn))], (1822 ^ _230602) ^ [_289592] : [aElementOf0(_289592, xO), 1826 ^ _230602 : [(1827 ^ _230602) ^ [] : [-(aElementOf0(1825 ^ [_289592], szNzAzT0))], (1829 ^ _230602) ^ [] : [-(aElementOf0(1825 ^ [_289592], sdtlbdtrb0(xd, szDzizrdt0(xd))))], (1831 ^ _230602) ^ [] : [-(sdtlpdtrp0(xe, 1825 ^ [_289592]) = _289592)]]], (1790 ^ _230602) ^ [] : [-(aFunction0(xd))], (1792 ^ _230602) ^ [] : [-(szDzozmdt0(xd) = szNzAzT0)], (1794 ^ _230602) ^ [_288732] : [aElementOf0(_288732, szNzAzT0), 1797 ^ _230602 : [(1798 ^ _230602) ^ [_288887] : [-(sdtlpdtrp0(xd, _288732) = sdtlpdtrp0(sdtlpdtrp0(xC, _288732), _288887)), aSet0(_288887), aElementOf0(_288887, slbdtsldtrb0(sdtlpdtrp0(xN, szszuzczcdt0(_288732)), xk))]]]], input).
% 0.35/1.39 ncf('1',plain,[sdtlpdtrp0(xc, xQ) = szDzizrdt0(xd)],start(1875 ^ 0)).
% 0.35/1.39 ncf('1.1',plain,[-(sdtlpdtrp0(xc, xQ) = szDzizrdt0(xd)), sdtlpdtrp0(xc, xQ) = sdtlpdtrp0(xd, xn), sdtlpdtrp0(xd, xn) = szDzizrdt0(xd)],extension(10 ^ 1,bind([[_231057, _231059, _231061], [szDzizrdt0(xd), sdtlpdtrp0(xd, xn), sdtlpdtrp0(xc, xQ)]]))).
% 0.35/1.39 ncf('1.1.1',plain,[-(sdtlpdtrp0(xc, xQ) = sdtlpdtrp0(xd, xn))],extension(1873 ^ 2)).
% 0.35/1.39 ncf('1.1.2',plain,[-(sdtlpdtrp0(xd, xn) = szDzizrdt0(xd))],extension(1869 ^ 2)).
% 0.35/1.39 %-----------------------------------------------------
% 0.35/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------