%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM576+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n031.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:02 EDT 2023
% Result : Theorem 0.40s 1.37s
% Output : Proof 0.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.01/0.12 % Problem : NUM576+3 : TPTP v8.1.2. Released v4.0.0.
% 0.12/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n031.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:04:55 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.40/1.37
% 0.40/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.40/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.40/1.37 %-----------------------------------------------------
% 0.40/1.37 ncf(matrix, plain, [(1894 ^ _228996) ^ [] : [xi = xj], (1896 ^ _228996) ^ [] : [sdtlseqdt0(szszuzczcdt0(xj), xi)], (1898 ^ _228996) ^ [] : [sdtlseqdt0(szszuzczcdt0(xi), xj)], (126 ^ _228996) ^ [_233045, _233047, _233049, _233051] : [-(sdtpldt0(_233051, _233047) = sdtpldt0(_233049, _233045)), _233051 = _233049, _233047 = _233045], (136 ^ _228996) ^ [_233376, _233378] : [_233378 = _233376, -(szmzazxdt0(_233378) = szmzazxdt0(_233376))], (142 ^ _228996) ^ [_233594, _233596] : [_233596 = _233594, -(slbdtrb0(_233596) = slbdtrb0(_233594))], (148 ^ _228996) ^ [_233840, _233842, _233844, _233846] : [-(sdtexdt0(_233846, _233842) = sdtexdt0(_233844, _233840)), _233846 = _233844, _233842 = _233840], (158 ^ _228996) ^ [_234199, _234201, _234203, _234205] : [-(sdtlbdtrb0(_234205, _234201) = sdtlbdtrb0(_234203, _234199)), _234205 = _234203, _234201 = _234199], (168 ^ _228996) ^ [_234530, _234532] : [_234532 = _234530, -(szDzizrdt0(_234532) = szDzizrdt0(_234530))], (174 ^ _228996) ^ [_234776, _234778, _234780, _234782] : [-(sdtlcdtrc0(_234782, _234778) = sdtlcdtrc0(_234780, _234776)), _234782 = _234780, _234778 = _234776], (184 ^ _228996) ^ [_235107, _235109] : [_235109 = _235107, -(sbrdtbr0(_235109) = sbrdtbr0(_235107))], (190 ^ _228996) ^ [_235353, _235355, _235357, _235359] : [-(slbdtsldtrb0(_235359, _235355) = slbdtsldtrb0(_235357, _235353)), _235359 = _235357, _235355 = _235353], (200 ^ _228996) ^ [_235684, _235686] : [_235686 = _235684, -(szDzozmdt0(_235686) = szDzozmdt0(_235684))], (206 ^ _228996) ^ [_235930, _235932, _235934, _235936] : [-(sdtmndt0(_235936, _235932) = sdtmndt0(_235934, _235930)), _235936 = _235934, _235932 = _235930], (216 ^ _228996) ^ [_236261, _236263] : [_236263 = _236261, -(szmzizndt0(_236263) = szmzizndt0(_236261))], (232 ^ _228996) ^ [_236818, _236820] : [_236820 = _236818, -(szszuzczcdt0(_236820) = szszuzczcdt0(_236818))], (222 ^ _228996) ^ [_236507, _236509, _236511, _236513] : [-(sdtlpdtrp0(_236513, _236509) = sdtlpdtrp0(_236511, _236507)), _236513 = _236511, _236509 = _236507], (2 ^ _228996) ^ [_229140] : [-(_229140 = _229140)], (4 ^ _228996) ^ [_229247, _229249] : [_229249 = _229247, -(_229247 = _229249)], (10 ^ _228996) ^ [_229451, _229453, _229455] : [-(_229455 = _229451), _229455 = _229453, _229453 = _229451], (20 ^ _228996) ^ [_229764, _229766] : [-(isFinite0(_229764)), _229766 = _229764, isFinite0(_229766)], (30 ^ _228996) ^ [_230087, _230089, _230091, _230093] : [-(iLess0(_230091, _230087)), iLess0(_230093, _230089), _230093 = _230091, _230089 = _230087], (44 ^ _228996) ^ [_230503, _230505] : [-(aFunction0(_230503)), _230505 = _230503, aFunction0(_230505)], (54 ^ _228996) ^ [_230798, _230800] : [-(aElement0(_230798)), _230800 = _230798, aElement0(_230800)], (64 ^ _228996) ^ [_231093, _231095] : [-(aSet0(_231093)), _231095 = _231093, aSet0(_231095)], (74 ^ _228996) ^ [_231388, _231390] : [-(isCountable0(_231388)), _231390 = _231388, isCountable0(_231390)], (84 ^ _228996) ^ [_231711, _231713, _231715, _231717] : [-(aSubsetOf0(_231715, _231711)), aSubsetOf0(_231717, _231713), _231717 = _231715, _231713 = _231711], (98 ^ _228996) ^ [_232155, _232157, _232159, _232161] : [-(aElementOf0(_232159, _232155)), aElementOf0(_232161, _232157), _232161 = _232159, _232157 = _232155], (112 ^ _228996) ^ [_232579, _232581, _232583, _232585] : [-(sdtlseqdt0(_232583, _232579)), sdtlseqdt0(_232585, _232581), _232585 = _232583, _232581 = _232579], (238 ^ _228996) ^ [_237108] : [aSet0(_237108), true___, -(true___)], (248 ^ _228996) ^ [_237363] : [aElement0(_237363), true___, -(true___)], (258 ^ _228996) ^ [_237618] : [aSet0(_237618), 261 ^ _228996 : [(262 ^ _228996) ^ [_237748] : [aElementOf0(_237748, _237618), -(aElement0(_237748))]]], (268 ^ _228996) ^ [_237949] : [aSet0(_237949), isFinite0(_237949), true___, -(true___)], (282 ^ _228996) ^ [_238319] : [_238319 = slcrc0, 285 ^ _228996 : [(286 ^ _228996) ^ [] : [-(aSet0(_238319))], (288 ^ _228996) ^ [_238500] : [aElementOf0(_238500, _238319)]]], (290 ^ _228996) ^ [_238568] : [-(_238568 = slcrc0), aSet0(_238568), -(aElementOf0(295 ^ [_238568], _238568))], (301 ^ _228996) ^ [] : [-(isFinite0(slcrc0))], (303 ^ _228996) ^ [_238950] : [aSet0(_238950), isCountable0(_238950), true___, -(true___)], (317 ^ _228996) ^ [_239291] : [isFinite0(_239291), aSet0(_239291), isCountable0(_239291)], (327 ^ _228996) ^ [_239561] : [_239561 = slcrc0, aSet0(_239561), isCountable0(_239561)], (337 ^ _228996) ^ [_239833] : [aSet0(_239833), 340 ^ _228996 : [(341 ^ _228996) ^ [_240009] : [aSubsetOf0(_240009, _239833), 344 ^ _228996 : [(345 ^ _228996) ^ [] : [-(aSet0(_240009))], (347 ^ _228996) ^ [_240218] : [aElementOf0(_240218, _240009), -(aElementOf0(_240218, _239833))]]], (353 ^ _228996) ^ [_240397] : [-(aSubsetOf0(_240397, _239833)), aSet0(_240397), 359 ^ _228996 : [(360 ^ _228996) ^ [] : [-(aElementOf0(358 ^ [_239833, _240397], _240397))], (362 ^ _228996) ^ [] : [aElementOf0(358 ^ [_239833, _240397], _239833)]]]]], (366 ^ _228996) ^ [_240834] : [aSet0(_240834), isFinite0(_240834), 373 ^ _228996 : [(374 ^ _228996) ^ [_241047] : [aSubsetOf0(_241047, _240834), -(isFinite0(_241047))]]], (380 ^ _228996) ^ [_241250] : [aSet0(_241250), -(aSubsetOf0(_241250, _241250))], (386 ^ _228996) ^ [_241452, _241454] : [aSet0(_241454), aSet0(_241452), -(_241454 = _241452), aSubsetOf0(_241454, _241452), aSubsetOf0(_241452, _241454)], (404 ^ _228996) ^ [_241941, _241943, _241945] : [aSet0(_241945), aSet0(_241943), aSet0(_241941), -(aSubsetOf0(_241945, _241941)), aSubsetOf0(_241945, _241943), aSubsetOf0(_241943, _241941)], (426 ^ _228996) ^ [_242527, _242529] : [aSet0(_242529), aElement0(_242527), 433 ^ _228996 : [(464 ^ _228996) ^ [_243788] : [-(_243788 = sdtpldt0(_242529, _242527)), aSet0(_243788), 472 ^ _228996 : [(473 ^ _228996) ^ [] : [-(aElementOf0(469 ^ [_242527, _242529, _243788], _243788))], (475 ^ _228996) ^ [] : [aElement0(469 ^ [_242527, _242529, _243788]), 478 ^ _228996 : [(479 ^ _228996) ^ [] : [aElementOf0(469 ^ [_242527, _242529, _243788], _242529)], (481 ^ _228996) ^ [] : [469 ^ [_242527, _242529, _243788] = _242527]]]], 482 ^ _228996 : [(491 ^ _228996) ^ [] : [aElementOf0(469 ^ [_242527, _242529, _243788], _243788)], (483 ^ _228996) ^ [] : [-(aElement0(469 ^ [_242527, _242529, _243788]))], (485 ^ _228996) ^ [] : [-(aElementOf0(469 ^ [_242527, _242529, _243788], _242529)), -(469 ^ [_242527, _242529, _243788] = _242527)]]], (434 ^ _228996) ^ [_242808] : [_242808 = sdtpldt0(_242529, _242527), 437 ^ _228996 : [(438 ^ _228996) ^ [] : [-(aSet0(_242808))], (440 ^ _228996) ^ [_243071] : [aElementOf0(_243071, _242808), 443 ^ _228996 : [(444 ^ _228996) ^ [] : [-(aElement0(_243071))], (446 ^ _228996) ^ [] : [-(aElementOf0(_243071, _242529)), -(_243071 = _242527)]]], (452 ^ _228996) ^ [_243426] : [-(aElementOf0(_243426, _242808)), aElement0(_243426), 457 ^ _228996 : [(458 ^ _228996) ^ [] : [aElementOf0(_243426, _242529)], (460 ^ _228996) ^ [] : [_243426 = _242527]]]]]]], (495 ^ _228996) ^ [_244825, _244827] : [aSet0(_244827), aElement0(_244825), 502 ^ _228996 : [(533 ^ _228996) ^ [_246093] : [-(_246093 = sdtmndt0(_244827, _244825)), aSet0(_246093), 553 ^ _228996 : [(554 ^ _228996) ^ [] : [-(aElement0(538 ^ [_244825, _244827, _246093]))], (556 ^ _228996) ^ [] : [-(aElementOf0(538 ^ [_244825, _244827, _246093], _244827))], (558 ^ _228996) ^ [] : [538 ^ [_244825, _244827, _246093] = _244825], (560 ^ _228996) ^ [] : [aElementOf0(538 ^ [_244825, _244827, _246093], _246093)]], 541 ^ _228996 : [(542 ^ _228996) ^ [] : [-(aElementOf0(538 ^ [_244825, _244827, _246093], _246093))], (544 ^ _228996) ^ [] : [aElement0(538 ^ [_244825, _244827, _246093]), aElementOf0(538 ^ [_244825, _244827, _246093], _244827), -(538 ^ [_244825, _244827, _246093] = _244825)]]], (503 ^ _228996) ^ [_245108] : [_245108 = sdtmndt0(_244827, _244825), 506 ^ _228996 : [(507 ^ _228996) ^ [] : [-(aSet0(_245108))], (509 ^ _228996) ^ [_245373] : [aElementOf0(_245373, _245108), 512 ^ _228996 : [(513 ^ _228996) ^ [] : [-(aElement0(_245373))], (515 ^ _228996) ^ [] : [-(aElementOf0(_245373, _244827))], (517 ^ _228996) ^ [] : [_245373 = _244825]]], (519 ^ _228996) ^ [_245709] : [-(aElementOf0(_245709, _245108)), aElement0(_245709), aElementOf0(_245709, _244827), -(_245709 = _244825)]]]]], (564 ^ _228996) ^ [_247123] : [aSet0(_247123), 567 ^ _228996 : [(568 ^ _228996) ^ [_247260] : [aElementOf0(_247260, _247123), -(sdtpldt0(sdtmndt0(_247123, _247260), _247260) = _247123)]]], (574 ^ _228996) ^ [_247489, _247491] : [aElement0(_247491), aSet0(_247489), -(aElementOf0(_247491, _247489)), -(sdtmndt0(sdtpldt0(_247489, _247491), _247491) = _247489)], (588 ^ _228996) ^ [_247876] : [aElement0(_247876), 591 ^ _228996 : [(592 ^ _228996) ^ [_248013] : [-(isCountable0(sdtpldt0(_248013, _247876))), aSet0(_248013), isCountable0(_248013)]]], (602 ^ _228996) ^ [_248305] : [aElement0(_248305), 605 ^ _228996 : [(606 ^ _228996) ^ [_248442] : [-(isCountable0(sdtmndt0(_248442, _248305))), aSet0(_248442), isCountable0(_248442)]]], (616 ^ _228996) ^ [_248734] : [aElement0(_248734), 619 ^ _228996 : [(620 ^ _228996) ^ [_248871] : [-(isFinite0(sdtpldt0(_248871, _248734))), aSet0(_248871), isFinite0(_248871)]]], (630 ^ _228996) ^ [_249163] : [aElement0(_249163), 633 ^ _228996 : [(634 ^ _228996) ^ [_249300] : [-(isFinite0(sdtmndt0(_249300, _249163))), aSet0(_249300), isFinite0(_249300)]]], (644 ^ _228996) ^ [] : [-(aSet0(szNzAzT0))], (646 ^ _228996) ^ [] : [-(isCountable0(szNzAzT0))], (648 ^ _228996) ^ [] : [-(aElementOf0(sz00, szNzAzT0))], (650 ^ _228996) ^ [_249753] : [aElementOf0(_249753, szNzAzT0), 653 ^ _228996 : [(654 ^ _228996) ^ [] : [-(aElementOf0(szszuzczcdt0(_249753), szNzAzT0))], (656 ^ _228996) ^ [] : [szszuzczcdt0(_249753) = sz00]]], (658 ^ _228996) ^ [_250039, _250041] : [aElementOf0(_250041, szNzAzT0), aElementOf0(_250039, szNzAzT0), szszuzczcdt0(_250041) = szszuzczcdt0(_250039), -(_250041 = _250039)], (672 ^ _228996) ^ [_250423] : [aElementOf0(_250423, szNzAzT0), -(_250423 = sz00), 680 ^ _228996 : [(681 ^ _228996) ^ [] : [-(aElementOf0(679 ^ [_250423], szNzAzT0))], (683 ^ _228996) ^ [] : [-(_250423 = szszuzczcdt0(679 ^ [_250423]))]]], (685 ^ _228996) ^ [_250840] : [aElementOf0(_250840, szNzAzT0), _250840 = szszuzczcdt0(_250840)], (691 ^ _228996) ^ [_251049, _251051] : [aElementOf0(_251051, szNzAzT0), aElementOf0(_251049, szNzAzT0), sdtlseqdt0(_251051, _251049), true___, -(true___)], (709 ^ _228996) ^ [_251499] : [aElementOf0(_251499, szNzAzT0), -(sdtlseqdt0(sz00, _251499))], (715 ^ _228996) ^ [_251689] : [aElementOf0(_251689, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_251689), sz00)], (721 ^ _228996) ^ [_251898, _251900] : [aElementOf0(_251900, szNzAzT0), aElementOf0(_251898, szNzAzT0), 728 ^ _228996 : [(729 ^ _228996) ^ [] : [sdtlseqdt0(_251900, _251898), -(sdtlseqdt0(szszuzczcdt0(_251900), szszuzczcdt0(_251898)))], (735 ^ _228996) ^ [] : [sdtlseqdt0(szszuzczcdt0(_251900), szszuzczcdt0(_251898)), -(sdtlseqdt0(_251900, _251898))]]], (741 ^ _228996) ^ [_252447] : [aElementOf0(_252447, szNzAzT0), -(sdtlseqdt0(_252447, szszuzczcdt0(_252447)))], (747 ^ _228996) ^ [_252641] : [aElementOf0(_252641, szNzAzT0), -(sdtlseqdt0(_252641, _252641))], (753 ^ _228996) ^ [_252845, _252847] : [aElementOf0(_252847, szNzAzT0), aElementOf0(_252845, szNzAzT0), -(_252847 = _252845), sdtlseqdt0(_252847, _252845), sdtlseqdt0(_252845, _252847)], (771 ^ _228996) ^ [_253338, _253340, _253342] : [aElementOf0(_253342, szNzAzT0), aElementOf0(_253340, szNzAzT0), aElementOf0(_253338, szNzAzT0), -(sdtlseqdt0(_253342, _253338)), sdtlseqdt0(_253342, _253340), sdtlseqdt0(_253340, _253338)], (793 ^ _228996) ^ [_253930, _253932] : [aElementOf0(_253932, szNzAzT0), aElementOf0(_253930, szNzAzT0), -(sdtlseqdt0(_253932, _253930)), -(sdtlseqdt0(szszuzczcdt0(_253930), _253932))], (807 ^ _228996) ^ [_254325, _254327] : [aElementOf0(_254327, szNzAzT0), aElementOf0(_254325, szNzAzT0), iLess0(_254327, _254325), true___, -(true___)], (825 ^ _228996) ^ [_254775] : [aElementOf0(_254775, szNzAzT0), -(iLess0(_254775, szszuzczcdt0(_254775)))], (831 ^ _228996) ^ [_254969] : [aSet0(_254969), -(aElement0(sbrdtbr0(_254969)))], (837 ^ _228996) ^ [_255159] : [aSet0(_255159), 840 ^ _228996 : [(841 ^ _228996) ^ [] : [aElementOf0(sbrdtbr0(_255159), szNzAzT0), -(isFinite0(_255159))], (847 ^ _228996) ^ [] : [isFinite0(_255159), -(aElementOf0(sbrdtbr0(_255159), szNzAzT0))]]], (853 ^ _228996) ^ [_255590] : [aSet0(_255590), 856 ^ _228996 : [(857 ^ _228996) ^ [] : [sbrdtbr0(_255590) = sz00, -(_255590 = slcrc0)], (863 ^ _228996) ^ [] : [_255590 = slcrc0, -(sbrdtbr0(_255590) = sz00)]]], (869 ^ _228996) ^ [_256024] : [aSet0(_256024), isFinite0(_256024), 876 ^ _228996 : [(877 ^ _228996) ^ [_256254] : [aElement0(_256254), -(aElementOf0(_256254, _256024)), -(sbrdtbr0(sdtpldt0(_256024, _256254)) = szszuzczcdt0(sbrdtbr0(_256024)))]]], (887 ^ _228996) ^ [_256567] : [aSet0(_256567), 890 ^ _228996 : [(891 ^ _228996) ^ [_256712] : [-(szszuzczcdt0(sbrdtbr0(sdtmndt0(_256567, _256712))) = sbrdtbr0(_256567)), isFinite0(_256567), aElementOf0(_256712, _256567)]]], (901 ^ _228996) ^ [_257020] : [aSet0(_257020), 904 ^ _228996 : [(905 ^ _228996) ^ [_257160] : [-(sdtlseqdt0(sbrdtbr0(_257160), sbrdtbr0(_257020))), isFinite0(_257020), aSubsetOf0(_257160, _257020)]]], (915 ^ _228996) ^ [_257472, _257474] : [aSet0(_257474), aElementOf0(_257472, szNzAzT0), 931 ^ _228996 : [(932 ^ _228996) ^ [] : [-(aSubsetOf0(930 ^ [_257472, _257474], _257474))], (934 ^ _228996) ^ [] : [-(sbrdtbr0(930 ^ [_257472, _257474]) = _257472)]], isFinite0(_257474), sdtlseqdt0(_257472, sbrdtbr0(_257474))], (936 ^ _228996) ^ [_258088] : [aSubsetOf0(_258088, szNzAzT0), -(_258088 = slcrc0), 943 ^ _228996 : [(944 ^ _228996) ^ [_258357] : [_258357 = szmzizndt0(_258088), 947 ^ _228996 : [(948 ^ _228996) ^ [] : [-(aElementOf0(_258357, _258088))], (950 ^ _228996) ^ [_258572] : [aElementOf0(_258572, _258088), -(sdtlseqdt0(_258357, _258572))]]], (956 ^ _228996) ^ [_258751] : [-(_258751 = szmzizndt0(_258088)), aElementOf0(_258751, _258088), 962 ^ _228996 : [(963 ^ _228996) ^ [] : [-(aElementOf0(961 ^ [_258088, _258751], _258088))], (965 ^ _228996) ^ [] : [sdtlseqdt0(_258751, 961 ^ [_258088, _258751])]]]]], (969 ^ _228996) ^ [_259196] : [aSubsetOf0(_259196, szNzAzT0), isFinite0(_259196), -(_259196 = slcrc0), 980 ^ _228996 : [(981 ^ _228996) ^ [_259548] : [_259548 = szmzazxdt0(_259196), 984 ^ _228996 : [(985 ^ _228996) ^ [] : [-(aElementOf0(_259548, _259196))], (987 ^ _228996) ^ [_259763] : [aElementOf0(_259763, _259196), -(sdtlseqdt0(_259763, _259548))]]], (993 ^ _228996) ^ [_259942] : [-(_259942 = szmzazxdt0(_259196)), aElementOf0(_259942, _259196), 999 ^ _228996 : [(1000 ^ _228996) ^ [] : [-(aElementOf0(998 ^ [_259196, _259942], _259196))], (1002 ^ _228996) ^ [] : [sdtlseqdt0(998 ^ [_259196, _259942], _259942)]]]]], (1006 ^ _228996) ^ [_260403, _260405] : [-(szmzizndt0(_260405) = szmzizndt0(_260403)), aElementOf0(szmzizndt0(_260405), _260403), aElementOf0(szmzizndt0(_260403), _260405), aSubsetOf0(_260405, szNzAzT0), aSubsetOf0(_260403, szNzAzT0), -(_260405 = slcrc0), -(_260403 = slcrc0)], (1032 ^ _228996) ^ [_261070] : [aElementOf0(_261070, szNzAzT0), 1035 ^ _228996 : [(1060 ^ _228996) ^ [_262039] : [-(_262039 = slbdtrb0(_261070)), aSet0(_262039), 1076 ^ _228996 : [(1077 ^ _228996) ^ [] : [-(aElementOf0(1065 ^ [_261070, _262039], szNzAzT0))], (1079 ^ _228996) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(1065 ^ [_261070, _262039]), _261070))], (1081 ^ _228996) ^ [] : [aElementOf0(1065 ^ [_261070, _262039], _262039)]], 1068 ^ _228996 : [(1069 ^ _228996) ^ [] : [-(aElementOf0(1065 ^ [_261070, _262039], _262039))], (1071 ^ _228996) ^ [] : [aElementOf0(1065 ^ [_261070, _262039], szNzAzT0), sdtlseqdt0(szszuzczcdt0(1065 ^ [_261070, _262039]), _261070)]]], (1036 ^ _228996) ^ [_261258] : [_261258 = slbdtrb0(_261070), 1039 ^ _228996 : [(1040 ^ _228996) ^ [] : [-(aSet0(_261258))], (1042 ^ _228996) ^ [_261508] : [aElementOf0(_261508, _261258), 1045 ^ _228996 : [(1046 ^ _228996) ^ [] : [-(aElementOf0(_261508, szNzAzT0))], (1048 ^ _228996) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(_261508), _261070))]]], (1050 ^ _228996) ^ [_261761] : [-(aElementOf0(_261761, _261258)), aElementOf0(_261761, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_261761), _261070)]]]]], (1085 ^ _228996) ^ [_262842] : [aElementOf0(_262842, szNzAzT0), -(isFinite0(slbdtrb0(_262842)))], (1091 ^ _228996) ^ [] : [-(slbdtrb0(sz00) = slcrc0)], (1093 ^ _228996) ^ [_263101, _263103] : [aElementOf0(_263103, szNzAzT0), aElementOf0(_263101, szNzAzT0), 1100 ^ _228996 : [(1111 ^ _228996) ^ [] : [1112 ^ _228996 : [(1113 ^ _228996) ^ [] : [aElementOf0(_263103, slbdtrb0(_263101))], (1115 ^ _228996) ^ [] : [_263103 = _263101]], -(aElementOf0(_263103, slbdtrb0(szszuzczcdt0(_263101))))], (1101 ^ _228996) ^ [] : [aElementOf0(_263103, slbdtrb0(szszuzczcdt0(_263101))), -(aElementOf0(_263103, slbdtrb0(_263101))), -(_263103 = _263101)]]], (1119 ^ _228996) ^ [_263828, _263830] : [aElementOf0(_263830, szNzAzT0), aElementOf0(_263828, szNzAzT0), 1126 ^ _228996 : [(1127 ^ _228996) ^ [] : [sdtlseqdt0(_263830, _263828), -(aSubsetOf0(slbdtrb0(_263830), slbdtrb0(_263828)))], (1133 ^ _228996) ^ [] : [aSubsetOf0(slbdtrb0(_263830), slbdtrb0(_263828)), -(sdtlseqdt0(_263830, _263828))]]], (1139 ^ _228996) ^ [_264377] : [1147 ^ _228996 : [(1148 ^ _228996) ^ [] : [-(aElementOf0(1146 ^ [_264377], szNzAzT0))], (1150 ^ _228996) ^ [] : [-(aSubsetOf0(_264377, slbdtrb0(1146 ^ [_264377])))]], aSubsetOf0(_264377, szNzAzT0), isFinite0(_264377)], (1152 ^ _228996) ^ [_264791] : [aElementOf0(_264791, szNzAzT0), -(sbrdtbr0(slbdtrb0(_264791)) = _264791)], (1158 ^ _228996) ^ [_265003, _265005] : [aSet0(_265005), aElementOf0(_265003, szNzAzT0), 1165 ^ _228996 : [(1190 ^ _228996) ^ [_266096] : [-(_266096 = slbdtsldtrb0(_265005, _265003)), aSet0(_266096), 1206 ^ _228996 : [(1207 ^ _228996) ^ [] : [-(aSubsetOf0(1195 ^ [_265003, _265005, _266096], _265005))], (1209 ^ _228996) ^ [] : [-(sbrdtbr0(1195 ^ [_265003, _265005, _266096]) = _265003)], (1211 ^ _228996) ^ [] : [aElementOf0(1195 ^ [_265003, _265005, _266096], _266096)]], 1198 ^ _228996 : [(1199 ^ _228996) ^ [] : [-(aElementOf0(1195 ^ [_265003, _265005, _266096], _266096))], (1201 ^ _228996) ^ [] : [aSubsetOf0(1195 ^ [_265003, _265005, _266096], _265005), sbrdtbr0(1195 ^ [_265003, _265005, _266096]) = _265003]]], (1166 ^ _228996) ^ [_265283] : [_265283 = slbdtsldtrb0(_265005, _265003), 1169 ^ _228996 : [(1170 ^ _228996) ^ [] : [-(aSet0(_265283))], (1172 ^ _228996) ^ [_265543] : [aElementOf0(_265543, _265283), 1175 ^ _228996 : [(1176 ^ _228996) ^ [] : [-(aSubsetOf0(_265543, _265005))], (1178 ^ _228996) ^ [] : [-(sbrdtbr0(_265543) = _265003)]]], (1180 ^ _228996) ^ [_265806] : [-(aElementOf0(_265806, _265283)), aSubsetOf0(_265806, _265005), sbrdtbr0(_265806) = _265003]]]]], (1215 ^ _228996) ^ [_266945] : [aSet0(_266945), isFinite0(_266945), 1222 ^ _228996 : [(1223 ^ _228996) ^ [_267161] : [aElementOf0(_267161, szNzAzT0), -(isFinite0(slbdtsldtrb0(_266945, _267161)))]]], (1229 ^ _228996) ^ [_267370] : [aSet0(_267370), -(isFinite0(_267370)), 1236 ^ _228996 : [(1237 ^ _228996) ^ [_267592] : [aElementOf0(_267592, szNzAzT0), slbdtsldtrb0(_267370, _267592) = slcrc0]]], (1243 ^ _228996) ^ [_267804] : [aSet0(_267804), isCountable0(_267804), 1250 ^ _228996 : [(1251 ^ _228996) ^ [_268028] : [-(isCountable0(slbdtsldtrb0(_267804, _268028))), aElementOf0(_268028, szNzAzT0), -(_268028 = sz00)]]], (1261 ^ _228996) ^ [_268329] : [aElementOf0(_268329, szNzAzT0), 1264 ^ _228996 : [(1265 ^ _228996) ^ [_268516, _268518] : [aSet0(_268518), aSet0(_268516), -(_268329 = sz00), -(aSubsetOf0(_268518, _268516)), aSubsetOf0(slbdtsldtrb0(_268518, _268329), slbdtsldtrb0(_268516, _268329)), -(slbdtsldtrb0(_268518, _268329) = slcrc0)]]], (1287 ^ _228996) ^ [_269135, _269137] : [aSet0(_269137), aElementOf0(_269135, szNzAzT0), 1294 ^ _228996 : [(1295 ^ _228996) ^ [_269386] : [1303 ^ _228996 : [(1304 ^ _228996) ^ [] : [-(aSubsetOf0(1302 ^ [_269135, _269137, _269386], _269137))], (1306 ^ _228996) ^ [] : [-(isFinite0(1302 ^ [_269135, _269137, _269386]))], (1308 ^ _228996) ^ [] : [-(aSubsetOf0(_269386, slbdtsldtrb0(1302 ^ [_269135, _269137, _269386], _269135)))]], aSubsetOf0(_269386, slbdtsldtrb0(_269137, _269135)), isFinite0(_269386)]]], (1310 ^ _228996) ^ [_269948] : [aFunction0(_269948), true___, -(true___)], (1320 ^ _228996) ^ [_270203] : [aFunction0(_270203), -(aSet0(szDzozmdt0(_270203)))], (1326 ^ _228996) ^ [_270393] : [aFunction0(_270393), 1329 ^ _228996 : [(1330 ^ _228996) ^ [_270528] : [aElementOf0(_270528, szDzozmdt0(_270393)), -(aElement0(sdtlpdtrp0(_270393, _270528)))]]], (1336 ^ _228996) ^ [_270753, _270755] : [aFunction0(_270755), aElement0(_270753), 1343 ^ _228996 : [(1368 ^ _228996) ^ [_271862] : [-(_271862 = sdtlbdtrb0(_270755, _270753)), aSet0(_271862), 1384 ^ _228996 : [(1385 ^ _228996) ^ [] : [-(aElementOf0(1373 ^ [_270753, _270755, _271862], szDzozmdt0(_270755)))], (1387 ^ _228996) ^ [] : [-(sdtlpdtrp0(_270755, 1373 ^ [_270753, _270755, _271862]) = _270753)], (1389 ^ _228996) ^ [] : [aElementOf0(1373 ^ [_270753, _270755, _271862], _271862)]], 1376 ^ _228996 : [(1377 ^ _228996) ^ [] : [-(aElementOf0(1373 ^ [_270753, _270755, _271862], _271862))], (1379 ^ _228996) ^ [] : [aElementOf0(1373 ^ [_270753, _270755, _271862], szDzozmdt0(_270755)), sdtlpdtrp0(_270755, 1373 ^ [_270753, _270755, _271862]) = _270753]]], (1344 ^ _228996) ^ [_271034] : [_271034 = sdtlbdtrb0(_270755, _270753), 1347 ^ _228996 : [(1348 ^ _228996) ^ [] : [-(aSet0(_271034))], (1350 ^ _228996) ^ [_271297] : [aElementOf0(_271297, _271034), 1353 ^ _228996 : [(1354 ^ _228996) ^ [] : [-(aElementOf0(_271297, szDzozmdt0(_270755)))], (1356 ^ _228996) ^ [] : [-(sdtlpdtrp0(_270755, _271297) = _270753)]]], (1358 ^ _228996) ^ [_271566] : [-(aElementOf0(_271566, _271034)), aElementOf0(_271566, szDzozmdt0(_270755)), sdtlpdtrp0(_270755, _271566) = _270753]]]]], (1393 ^ _228996) ^ [_272737, _272739] : [-(aSubsetOf0(sdtlbdtrb0(_272739, _272737), szDzozmdt0(_272739))), aFunction0(_272739), aElement0(_272737)], (1403 ^ _228996) ^ [_273028] : [aFunction0(_273028), 1406 ^ _228996 : [(1407 ^ _228996) ^ [_273205] : [aSubsetOf0(_273205, szDzozmdt0(_273028)), 1410 ^ _228996 : [(1436 ^ _228996) ^ [_274392] : [-(_274392 = sdtlcdtrc0(_273028, _273205)), aSet0(_274392), 1453 ^ _228996 : [(1454 ^ _228996) ^ [] : [-(aElementOf0(1452 ^ [_273028, _273205, _274392], _273205))], (1456 ^ _228996) ^ [] : [-(sdtlpdtrp0(_273028, 1452 ^ [_273028, _273205, _274392]) = 1441 ^ [_273028, _273205, _274392])], (1458 ^ _228996) ^ [] : [aElementOf0(1441 ^ [_273028, _273205, _274392], _274392)]], 1444 ^ _228996 : [(1445 ^ _228996) ^ [] : [-(aElementOf0(1441 ^ [_273028, _273205, _274392], _274392))], (1447 ^ _228996) ^ [_274785] : [aElementOf0(_274785, _273205), sdtlpdtrp0(_273028, _274785) = 1441 ^ [_273028, _273205, _274392]]]], (1411 ^ _228996) ^ [_273410] : [_273410 = sdtlcdtrc0(_273028, _273205), 1414 ^ _228996 : [(1415 ^ _228996) ^ [] : [-(aSet0(_273410))], (1417 ^ _228996) ^ [_273676] : [aElementOf0(_273676, _273410), 1421 ^ _228996 : [(1422 ^ _228996) ^ [] : [-(aElementOf0(1420 ^ [_273028, _273205, _273410, _273676], _273205))], (1424 ^ _228996) ^ [] : [-(sdtlpdtrp0(_273028, 1420 ^ [_273028, _273205, _273410, _273676]) = _273676)]]], (1426 ^ _228996) ^ [_274030] : [-(aElementOf0(_274030, _273410)), 1427 ^ _228996 : [(1428 ^ _228996) ^ [_274135] : [aElementOf0(_274135, _273205), sdtlpdtrp0(_273028, _274135) = _274030]]]]]]]]], (1462 ^ _228996) ^ [_275396] : [aFunction0(_275396), 1465 ^ _228996 : [(1466 ^ _228996) ^ [_275537] : [aElementOf0(_275537, szDzozmdt0(_275396)), -(aElementOf0(sdtlpdtrp0(_275396, _275537), sdtlcdtrc0(_275396, szDzozmdt0(_275396))))]]], (1472 ^ _228996) ^ [_275760] : [aFunction0(_275760), 1475 ^ _228996 : [(1476 ^ _228996) ^ [_275937] : [aSubsetOf0(_275937, szDzozmdt0(_275760)), 1479 ^ _228996 : [(1480 ^ _228996) ^ [_276142] : [_276142 = sdtexdt0(_275760, _275937), 1483 ^ _228996 : [(1484 ^ _228996) ^ [] : [-(aFunction0(_276142))], (1486 ^ _228996) ^ [] : [-(szDzozmdt0(_276142) = _275937)], (1488 ^ _228996) ^ [_276449] : [aElementOf0(_276449, _275937), -(sdtlpdtrp0(_276142, _276449) = sdtlpdtrp0(_275760, _276449))]]], (1494 ^ _228996) ^ [_276650] : [-(_276650 = sdtexdt0(_275760, _275937)), aFunction0(_276650), szDzozmdt0(_276650) = _275937, 1504 ^ _228996 : [(1505 ^ _228996) ^ [] : [-(aElementOf0(1503 ^ [_275760, _275937, _276650], _275937))], (1507 ^ _228996) ^ [] : [sdtlpdtrp0(_276650, 1503 ^ [_275760, _275937, _276650]) = sdtlpdtrp0(_275760, 1503 ^ [_275760, _275937, _276650])]]]]]]], (1511 ^ _228996) ^ [_277244] : [aFunction0(_277244), 1514 ^ _228996 : [(1515 ^ _228996) ^ [_277432] : [aSubsetOf0(_277432, szDzozmdt0(_277244)), isCountable0(_277432), 1526 ^ _228996 : [(1527 ^ _228996) ^ [] : [-(aElementOf0(1524 ^ [_277244, _277432], szDzozmdt0(_277244)))], (1529 ^ _228996) ^ [] : [-(aElementOf0(1525 ^ [_277244, _277432], szDzozmdt0(_277244)))], (1531 ^ _228996) ^ [] : [1524 ^ [_277244, _277432] = 1525 ^ [_277244, _277432]], (1533 ^ _228996) ^ [] : [-(sdtlpdtrp0(_277244, 1524 ^ [_277244, _277432]) = sdtlpdtrp0(_277244, 1525 ^ [_277244, _277432]))]], -(isCountable0(sdtlcdtrc0(_277244, _277432)))]]], (1537 ^ _228996) ^ [_278304] : [aFunction0(_278304), 1548 ^ _228996 : [(1549 ^ _228996) ^ [] : [-(aElement0(szDzizrdt0(_278304)))], (1551 ^ _228996) ^ [] : [-(isCountable0(sdtlbdtrb0(_278304, szDzizrdt0(_278304))))]], isCountable0(szDzozmdt0(_278304)), isFinite0(sdtlcdtrc0(_278304, szDzozmdt0(_278304)))], (1553 ^ _228996) ^ [] : [-(aSet0(xT))], (1555 ^ _228996) ^ [] : [-(isFinite0(xT))], (1557 ^ _228996) ^ [] : [-(aElementOf0(xK, szNzAzT0))], (1559 ^ _228996) ^ [] : [-(aSet0(xS))], (1567 ^ _228996) ^ [] : [-(aSubsetOf0(xS, szNzAzT0))], (1569 ^ _228996) ^ [] : [-(isCountable0(xS))], (1561 ^ _228996) ^ [_278989] : [aElementOf0(_278989, xS), -(aElementOf0(_278989, szNzAzT0))], (1571 ^ _228996) ^ [] : [-(aFunction0(xc))], (1573 ^ _228996) ^ [_279366] : [aElementOf0(_279366, szDzozmdt0(xc)), 1576 ^ _228996 : [(1577 ^ _228996) ^ [] : [-(aSet0(_279366))], (1585 ^ _228996) ^ [] : [-(aSubsetOf0(_279366, xS))], (1587 ^ _228996) ^ [] : [-(sbrdtbr0(_279366) = xK)], (1579 ^ _228996) ^ [_279601] : [aElementOf0(_279601, _279366), -(aElementOf0(_279601, xS))]]], (1589 ^ _228996) ^ [_279888] : [-(aElementOf0(_279888, szDzozmdt0(xc))), sbrdtbr0(_279888) = xK, 1592 ^ _228996 : [(1602 ^ _228996) ^ [] : [aSubsetOf0(_279888, xS)], (1593 ^ _228996) ^ [] : [aSet0(_279888), 1597 ^ _228996 : [(1598 ^ _228996) ^ [] : [-(aElementOf0(1596 ^ [_279888], _279888))], (1600 ^ _228996) ^ [] : [aElementOf0(1596 ^ [_279888], xS)]]]]], (1608 ^ _228996) ^ [] : [-(szDzozmdt0(xc) = slbdtsldtrb0(xS, xK))], (1610 ^ _228996) ^ [] : [-(aSet0(sdtlcdtrc0(xc, szDzozmdt0(xc))))], (1637 ^ _228996) ^ [] : [-(aSubsetOf0(sdtlcdtrc0(xc, szDzozmdt0(xc)), xT))], (1631 ^ _228996) ^ [_281241] : [aElementOf0(_281241, sdtlcdtrc0(xc, szDzozmdt0(xc))), -(aElementOf0(_281241, xT))], (1612 ^ _228996) ^ [_280594] : [aElementOf0(_280594, sdtlcdtrc0(xc, szDzozmdt0(xc))), 1616 ^ _228996 : [(1617 ^ _228996) ^ [] : [-(aElementOf0(1615 ^ [_280594], szDzozmdt0(xc)))], (1619 ^ _228996) ^ [] : [-(sdtlpdtrp0(xc, 1615 ^ [_280594]) = _280594)]]], (1621 ^ _228996) ^ [_280894] : [-(aElementOf0(_280894, sdtlcdtrc0(xc, szDzozmdt0(xc)))), 1622 ^ _228996 : [(1623 ^ _228996) ^ [_280987] : [aElementOf0(_280987, szDzozmdt0(xc)), sdtlpdtrp0(xc, _280987) = _280894]]], (1639 ^ _228996) ^ [_281480] : [aElementOf0(_281480, szNzAzT0), 1642 ^ _228996 : [(1643 ^ _228996) ^ [_281943] : [isCountable0(_281943), 1646 ^ _228996 : [(1656 ^ _228996) ^ [] : [aSubsetOf0(_281943, szNzAzT0)], (1647 ^ _228996) ^ [] : [aSet0(_281943), 1651 ^ _228996 : [(1652 ^ _228996) ^ [] : [-(aElementOf0(1650 ^ [_281480, _281943], _281943))], (1654 ^ _228996) ^ [] : [aElementOf0(1650 ^ [_281480, _281943], szNzAzT0)]]]], 1659 ^ _228996 : [(1660 ^ _228996) ^ [_282767] : [iLess0(_281480, xK), 1736 ^ _228996 : [(1737 ^ _228996) ^ [] : [-(aElementOf0(1735 ^ [_281480, _281943, _282767], xT))], (1740 ^ _228996) ^ [] : [-(aSet0(1738 ^ [_281480, _281943, _282767]))], (1742 ^ _228996) ^ [_286321] : [aElementOf0(_286321, 1738 ^ [_281480, _281943, _282767]), -(aElementOf0(_286321, _281943))], (1748 ^ _228996) ^ [] : [-(aSubsetOf0(1738 ^ [_281480, _281943, _282767], _281943))], (1750 ^ _228996) ^ [] : [-(isCountable0(1738 ^ [_281480, _281943, _282767]))], (1752 ^ _228996) ^ [_286686] : [-(sdtlpdtrp0(_282767, _286686) = 1735 ^ [_281480, _281943, _282767]), 1753 ^ _228996 : [(1769 ^ _228996) ^ [] : [aElementOf0(_286686, slbdtsldtrb0(1738 ^ [_281480, _281943, _282767], _281480))], (1754 ^ _228996) ^ [] : [sbrdtbr0(_286686) = _281480, 1755 ^ _228996 : [(1765 ^ _228996) ^ [] : [aSubsetOf0(_286686, 1738 ^ [_281480, _281943, _282767])], (1756 ^ _228996) ^ [] : [aSet0(_286686), 1760 ^ _228996 : [(1761 ^ _228996) ^ [] : [-(aElementOf0(1759 ^ [_281480, _281943, _282767, _286686], _286686))], (1763 ^ _228996) ^ [] : [aElementOf0(1759 ^ [_281480, _281943, _282767, _286686], 1738 ^ [_281480, _281943, _282767])]]]]]]]], aFunction0(_282767), 1668 ^ _228996 : [(1702 ^ _228996) ^ [] : [szDzozmdt0(_282767) = slbdtsldtrb0(_281943, _281480)], (1669 ^ _228996) ^ [] : [1687 ^ _228996 : [(1700 ^ _228996) ^ [] : [aElementOf0(1667 ^ [_281480, _281943, _282767], szDzozmdt0(_282767))], (1688 ^ _228996) ^ [] : [-(aSet0(1667 ^ [_281480, _281943, _282767]))], (1696 ^ _228996) ^ [] : [-(aSubsetOf0(1667 ^ [_281480, _281943, _282767], _281943))], (1698 ^ _228996) ^ [] : [-(sbrdtbr0(1667 ^ [_281480, _281943, _282767]) = _281480)], (1690 ^ _228996) ^ [_284129] : [aElementOf0(_284129, 1667 ^ [_281480, _281943, _282767]), -(aElementOf0(_284129, _281943))]], 1670 ^ _228996 : [(1671 ^ _228996) ^ [] : [-(aElementOf0(1667 ^ [_281480, _281943, _282767], szDzozmdt0(_282767)))], (1673 ^ _228996) ^ [] : [sbrdtbr0(1667 ^ [_281480, _281943, _282767]) = _281480, 1674 ^ _228996 : [(1684 ^ _228996) ^ [] : [aSubsetOf0(1667 ^ [_281480, _281943, _282767], _281943)], (1675 ^ _228996) ^ [] : [aSet0(1667 ^ [_281480, _281943, _282767]), 1679 ^ _228996 : [(1680 ^ _228996) ^ [] : [-(aElementOf0(1678 ^ [_281480, _281943, _282767], 1667 ^ [_281480, _281943, _282767]))], (1682 ^ _228996) ^ [] : [aElementOf0(1678 ^ [_281480, _281943, _282767], _281943)]]]]]]]], 1703 ^ _228996 : [(1726 ^ _228996) ^ [] : [-(aElementOf0(1724 ^ [_281480, _281943, _282767], sdtlcdtrc0(_282767, szDzozmdt0(_282767))))], (1728 ^ _228996) ^ [] : [aElementOf0(1724 ^ [_281480, _281943, _282767], xT)], (1730 ^ _228996) ^ [] : [aSubsetOf0(sdtlcdtrc0(_282767, szDzozmdt0(_282767)), xT)], (1704 ^ _228996) ^ [] : [-(aSet0(sdtlcdtrc0(_282767, szDzozmdt0(_282767))))], (1706 ^ _228996) ^ [_284726] : [aElementOf0(_284726, sdtlcdtrc0(_282767, szDzozmdt0(_282767))), 1710 ^ _228996 : [(1711 ^ _228996) ^ [] : [-(aElementOf0(1709 ^ [_281480, _281943, _282767, _284726], szDzozmdt0(_282767)))], (1713 ^ _228996) ^ [] : [-(sdtlpdtrp0(_282767, 1709 ^ [_281480, _281943, _282767, _284726]) = _284726)]]], (1715 ^ _228996) ^ [_285096] : [-(aElementOf0(_285096, sdtlcdtrc0(_282767, szDzozmdt0(_282767)))), 1716 ^ _228996 : [(1717 ^ _228996) ^ [_285208] : [aElementOf0(_285208, szDzozmdt0(_282767)), sdtlpdtrp0(_282767, _285208) = _285096]]]]]]]]], (1773 ^ _228996) ^ [] : [xK = sz00], (1775 ^ _228996) ^ [] : [xK = sz00], (1777 ^ _228996) ^ [] : [-(aElementOf0(xk, szNzAzT0))], (1779 ^ _228996) ^ [] : [-(szszuzczcdt0(xk) = xK)], (1854 ^ _228996) ^ [_290331] : [aElementOf0(_290331, szNzAzT0), 1857 ^ _228996 : [(1858 ^ _228996) ^ [] : [-(aSet0(sdtlpdtrp0(xN, _290331)))], (1866 ^ _228996) ^ [] : [-(aSubsetOf0(sdtlpdtrp0(xN, _290331), szNzAzT0))], (1868 ^ _228996) ^ [] : [-(isCountable0(sdtlpdtrp0(xN, _290331)))], (1860 ^ _228996) ^ [_290578] : [aElementOf0(_290578, sdtlpdtrp0(xN, _290331)), -(aElementOf0(_290578, szNzAzT0))]]], (1890 ^ _228996) ^ [] : [-(aElementOf0(xi, szNzAzT0))], (1892 ^ _228996) ^ [] : [-(aElementOf0(xj, szNzAzT0))], (1870 ^ _228996) ^ [_290922, _290924] : [aElementOf0(_290924, szNzAzT0), aElementOf0(_290922, szNzAzT0), sdtlseqdt0(_290922, _290924), 1881 ^ _228996 : [(1888 ^ _228996) ^ [] : [-(aSubsetOf0(sdtlpdtrp0(xN, _290924), sdtlpdtrp0(xN, _290922)))], (1882 ^ _228996) ^ [_291271] : [aElementOf0(_291271, sdtlpdtrp0(xN, _290924)), -(aElementOf0(_291271, sdtlpdtrp0(xN, _290922)))]]], (1781 ^ _228996) ^ [] : [-(aFunction0(xN))], (1783 ^ _228996) ^ [] : [-(szDzozmdt0(xN) = szNzAzT0)], (1785 ^ _228996) ^ [] : [-(sdtlpdtrp0(xN, sz00) = xS)], (1787 ^ _228996) ^ [_287914] : [aElementOf0(_287914, szNzAzT0), isCountable0(sdtlpdtrp0(xN, _287914)), 1794 ^ _228996 : [(1804 ^ _228996) ^ [] : [aSubsetOf0(sdtlpdtrp0(xN, _287914), szNzAzT0)], (1795 ^ _228996) ^ [] : [aSet0(sdtlpdtrp0(xN, _287914)), 1799 ^ _228996 : [(1800 ^ _228996) ^ [] : [-(aElementOf0(1798 ^ [_287914], sdtlpdtrp0(xN, _287914)))], (1802 ^ _228996) ^ [] : [aElementOf0(1798 ^ [_287914], szNzAzT0)]]]], 1807 ^ _228996 : [(1808 ^ _228996) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _287914)), sdtlpdtrp0(xN, _287914)))], (1810 ^ _228996) ^ [_288782] : [aElementOf0(_288782, sdtlpdtrp0(xN, _287914)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _287914)), _288782))], (1816 ^ _228996) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _287914), szmzizndt0(sdtlpdtrp0(xN, _287914)))))], (1842 ^ _228996) ^ [] : [-(aSet0(sdtlpdtrp0(xN, szszuzczcdt0(_287914))))], (1850 ^ _228996) ^ [] : [-(aSubsetOf0(sdtlpdtrp0(xN, szszuzczcdt0(_287914)), sdtmndt0(sdtlpdtrp0(xN, _287914), szmzizndt0(sdtlpdtrp0(xN, _287914)))))], (1852 ^ _228996) ^ [] : [-(isCountable0(sdtlpdtrp0(xN, szszuzczcdt0(_287914))))], (1844 ^ _228996) ^ [_289934] : [aElementOf0(_289934, sdtlpdtrp0(xN, szszuzczcdt0(_287914))), -(aElementOf0(_289934, sdtmndt0(sdtlpdtrp0(xN, _287914), szmzizndt0(sdtlpdtrp0(xN, _287914)))))], (1818 ^ _228996) ^ [_289099] : [aElementOf0(_289099, sdtmndt0(sdtlpdtrp0(xN, _287914), szmzizndt0(sdtlpdtrp0(xN, _287914)))), 1821 ^ _228996 : [(1822 ^ _228996) ^ [] : [-(aElement0(_289099))], (1824 ^ _228996) ^ [] : [-(aElementOf0(_289099, sdtlpdtrp0(xN, _287914)))], (1826 ^ _228996) ^ [] : [_289099 = szmzizndt0(sdtlpdtrp0(xN, _287914))]]], (1828 ^ _228996) ^ [_289449] : [-(aElementOf0(_289449, sdtmndt0(sdtlpdtrp0(xN, _287914), szmzizndt0(sdtlpdtrp0(xN, _287914))))), aElement0(_289449), aElementOf0(_289449, sdtlpdtrp0(xN, _287914)), -(_289449 = szmzizndt0(sdtlpdtrp0(xN, _287914)))]]]], input).
% 0.40/1.37 ncf('1',plain,[xi = xj],start(1894 ^ 0)).
% 0.40/1.37 ncf('1.1',plain,[-(xi = xj), aElementOf0(xi, szNzAzT0), aElementOf0(xj, szNzAzT0), sdtlseqdt0(xi, xj), sdtlseqdt0(xj, xi)],extension(753 ^ 1,bind([[_252845, _252847], [xj, xi]]))).
% 0.40/1.37 ncf('1.1.1',plain,[-(aElementOf0(xi, szNzAzT0))],extension(1890 ^ 2)).
% 0.40/1.37 ncf('1.1.2',plain,[-(aElementOf0(xj, szNzAzT0))],extension(1892 ^ 2)).
% 0.40/1.37 ncf('1.1.3',plain,[-(sdtlseqdt0(xi, xj)), aElementOf0(xi, szNzAzT0), aElementOf0(xj, szNzAzT0), -(sdtlseqdt0(szszuzczcdt0(xj), xi))],extension(793 ^ 2,bind([[_253930, _253932], [xj, xi]]))).
% 0.40/1.37 ncf('1.1.3.1',plain,[-(aElementOf0(xi, szNzAzT0))],lemmata('[1].x')).
% 0.40/1.37 ncf('1.1.3.2',plain,[-(aElementOf0(xj, szNzAzT0))],lemmata('[1].x')).
% 0.40/1.37 ncf('1.1.3.3',plain,[sdtlseqdt0(szszuzczcdt0(xj), xi)],extension(1896 ^ 3)).
% 0.40/1.37 ncf('1.1.4',plain,[-(sdtlseqdt0(xj, xi)), aElementOf0(xj, szNzAzT0), aElementOf0(xi, szNzAzT0), -(sdtlseqdt0(szszuzczcdt0(xi), xj))],extension(793 ^ 2,bind([[_253930, _253932], [xi, xj]]))).
% 0.40/1.37 ncf('1.1.4.1',plain,[-(aElementOf0(xj, szNzAzT0))],lemmata('[1].x')).
% 0.40/1.37 ncf('1.1.4.2',plain,[-(aElementOf0(xi, szNzAzT0))],lemmata('[1].x')).
% 0.40/1.37 ncf('1.1.4.3',plain,[sdtlseqdt0(szszuzczcdt0(xi), xj)],extension(1898 ^ 3)).
% 0.40/1.37 %-----------------------------------------------------
% 0.40/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------