↑ Up

nanoCoP---2.0.THM-Prf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : nanoCoP---2.0
% Problem  : NUM603+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : nanocop.sh %s %d

% Computer : n027.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:07 EDT 2023

% Result   : Theorem 54.61s 53.07s
% Output   : Proof 54.61s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : NUM603+3 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.13  % Command  : nanocop.sh %s %d
% 0.12/0.34  % Computer : n027.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:42:05 EDT 2023
% 0.12/0.34  % CPUTime  : 
% 54.61/53.07  
% 54.61/53.07  /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 54.61/53.07  Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 54.61/53.07  %-----------------------------------------------------
% 54.61/53.07  ncf(matrix, plain, [(2626 ^ _474339) ^ [] : [aSubsetOf0(sdtlpdtrp0(xN, xi), xS)], (2624 ^ _474339) ^ [] : [aElementOf0(2620 ^ [], xS)], (2622 ^ _474339) ^ [] : [-(aElementOf0(2620 ^ [], sdtlpdtrp0(xN, xi)))], !, (685 ^ _382164) ^ [_403988] : [aElementOf0(_403988, szNzAzT0), _403988 = szszuzczcdt0(_403988)], (2225 ^ _382164) ^ [_458178] : [aElementOf0(_458178, szNzAzT0), 2228 ^ _382164 : [(2229 ^ _382164) ^ [_458677] : [isCountable0(_458677), 2232 ^ _382164 : [(2276 ^ _382164) ^ [] : [aSubsetOf0(_458677, sdtmndt0(sdtlpdtrp0(xN, _458178), szmzizndt0(sdtlpdtrp0(xN, _458178))))], (2243 ^ _382164) ^ [_459583] : [aElementOf0(_459583, sdtmndt0(sdtlpdtrp0(xN, _458178), szmzizndt0(sdtlpdtrp0(xN, _458178)))), 2246 ^ _382164 : [(2251 ^ _382164) ^ [] : [_459583 = szmzizndt0(sdtlpdtrp0(xN, _458178))], (2249 ^ _382164) ^ [] : [-(aElementOf0(_459583, sdtlpdtrp0(xN, _458178)))], (2247 ^ _382164) ^ [] : [-(aElement0(_459583))]]], (2253 ^ _382164) ^ [_459945] : [-(aElementOf0(_459945, sdtmndt0(sdtlpdtrp0(xN, _458178), szmzizndt0(sdtlpdtrp0(xN, _458178))))), aElement0(_459945), aElementOf0(_459945, sdtlpdtrp0(xN, _458178)), -(_459945 = szmzizndt0(sdtlpdtrp0(xN, _458178)))], (2267 ^ _382164) ^ [] : [aSet0(_458677), 2271 ^ _382164 : [(2274 ^ _382164) ^ [] : [aElementOf0(2270 ^ [_458178, _458677], sdtmndt0(sdtlpdtrp0(xN, _458178), szmzizndt0(sdtlpdtrp0(xN, _458178))))], (2272 ^ _382164) ^ [] : [-(aElementOf0(2270 ^ [_458178, _458677], _458677))]]], (2233 ^ _382164) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _458178)), sdtlpdtrp0(xN, _458178)))], (2235 ^ _382164) ^ [_459254] : [aElementOf0(_459254, sdtlpdtrp0(xN, _458178)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _458178)), _459254))], (2241 ^ _382164) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _458178), szmzizndt0(sdtlpdtrp0(xN, _458178)))))]], 2279 ^ _382164 : [(2280 ^ _382164) ^ [_460778] : [aSet0(_460778), 2285 ^ _382164 : [(2286 ^ _382164) ^ [] : [2288 ^ _382164 : [(2293 ^ _382164) ^ [] : [aSubsetOf0(_460778, _458677)], (2291 ^ _382164) ^ [] : [aElementOf0(2287 ^ [_458178, _458677, _460778], _458677)], (2289 ^ _382164) ^ [] : [-(aElementOf0(2287 ^ [_458178, _458677, _460778], _460778))]], sbrdtbr0(_460778) = xk], (2297 ^ _382164) ^ [] : [aElementOf0(_460778, slbdtsldtrb0(_458677, xk))]], 2298 ^ _382164 : [(2307 ^ _382164) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _458178), szmzizndt0(sdtlpdtrp0(xN, _458178)))))], (2333 ^ _382164) ^ [_462833] : [aElementOf0(_462833, _460778), -(aElementOf0(_462833, sdtmndt0(sdtlpdtrp0(xN, _458178), szmzizndt0(sdtlpdtrp0(xN, _458178)))))], (2299 ^ _382164) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _458178)), sdtlpdtrp0(xN, _458178)))], (2309 ^ _382164) ^ [_462010] : [aElementOf0(_462010, sdtmndt0(sdtlpdtrp0(xN, _458178), szmzizndt0(sdtlpdtrp0(xN, _458178)))), 2312 ^ _382164 : [(2317 ^ _382164) ^ [] : [_462010 = szmzizndt0(sdtlpdtrp0(xN, _458178))], (2315 ^ _382164) ^ [] : [-(aElementOf0(_462010, sdtlpdtrp0(xN, _458178)))], (2313 ^ _382164) ^ [] : [-(aElement0(_462010))]]], (2339 ^ _382164) ^ [] : [-(aSubsetOf0(_460778, sdtmndt0(sdtlpdtrp0(xN, _458178), szmzizndt0(sdtlpdtrp0(xN, _458178)))))], (2341 ^ _382164) ^ [] : [-(aElementOf0(_460778, slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _458178), szmzizndt0(sdtlpdtrp0(xN, _458178))), xk)))], (2319 ^ _382164) ^ [_462384] : [-(aElementOf0(_462384, sdtmndt0(sdtlpdtrp0(xN, _458178), szmzizndt0(sdtlpdtrp0(xN, _458178))))), aElement0(_462384), aElementOf0(_462384, sdtlpdtrp0(xN, _458178)), -(_462384 = szmzizndt0(sdtlpdtrp0(xN, _458178)))], (2301 ^ _382164) ^ [_461673] : [aElementOf0(_461673, sdtlpdtrp0(xN, _458178)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _458178)), _461673))]]]]]]], (2544 ^ _382164) ^ [] : [-(aSet0(xO))], (126 ^ _382164) ^ [_386165, _386167] : [_386167 = _386165, -(szmzazxdt0(_386167) = szmzazxdt0(_386165))], (1553 ^ _382164) ^ [] : [-(aSet0(xT))], (2495 ^ _382164) ^ [_469472] : [aElementOf0(_469472, sdtlcdtrc0(xd, szDzozmdt0(xd))), 2499 ^ _382164 : [(2502 ^ _382164) ^ [] : [-(sdtlpdtrp0(xd, 2498 ^ [_469472]) = _469472)], (2500 ^ _382164) ^ [] : [-(aElementOf0(2498 ^ [_469472], szDzozmdt0(xd)))]]], (228 ^ _382164) ^ [_389853, _389855, _389857, _389859] : [-(sdtlpdtrp0(_389859, _389855) = sdtlpdtrp0(_389857, _389853)), _389859 = _389857, _389855 = _389853], (30 ^ _382164) ^ [_383235, _383237, _383239, _383241] : [-(iLess0(_383239, _383235)), iLess0(_383241, _383237), _383241 = _383239, _383237 = _383235], (1561 ^ _382164) ^ [_432137] : [aElementOf0(_432137, xS), -(aElementOf0(_432137, szNzAzT0))], (2024 ^ _382164) ^ [] : [-(aFunction0(xC))], (831 ^ _382164) ^ [_408117] : [aSet0(_408117), -(aElement0(sbrdtbr0(_408117)))], (837 ^ _382164) ^ [_408307] : [aSet0(_408307), 840 ^ _382164 : [(847 ^ _382164) ^ [] : [isFinite0(_408307), -(aElementOf0(sbrdtbr0(_408307), szNzAzT0))], (841 ^ _382164) ^ [] : [aElementOf0(sbrdtbr0(_408307), szNzAzT0), -(isFinite0(_408307))]]], (1557 ^ _382164) ^ [] : [-(aElementOf0(xK, szNzAzT0))], (1890 ^ _382164) ^ [_444716, _444718] : [aElementOf0(_444718, szNzAzT0), aElementOf0(_444716, szNzAzT0), -(_444718 = _444716), 1901 ^ _382164 : [(1904 ^ _382164) ^ [_445207] : [aElementOf0(_445207, sdtlpdtrp0(xN, _444718)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _444718)), _445207))], (1919 ^ _382164) ^ [] : [szmzizndt0(sdtlpdtrp0(xN, _444718)) = szmzizndt0(sdtlpdtrp0(xN, _444716))], (1910 ^ _382164) ^ [] : [aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _444718)), sdtlpdtrp0(xN, _444716)), 1914 ^ _382164 : [(1917 ^ _382164) ^ [] : [sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _444718)), 1913 ^ [_444716, _444718])], (1915 ^ _382164) ^ [] : [-(aElementOf0(1913 ^ [_444716, _444718], sdtlpdtrp0(xN, _444716)))]]], (1902 ^ _382164) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _444718)), sdtlpdtrp0(xN, _444718)))]]], (2520 ^ _382164) ^ [] : [-(aSubsetOf0(sdtlcdtrc0(xd, szDzozmdt0(xd)), xT))], (238 ^ _382164) ^ [_390256] : [aSet0(_390256), true___, -(true___)], (1921 ^ _382164) ^ [_445807] : [aElementOf0(_445807, szNzAzT0), 1924 ^ _382164 : [(1925 ^ _382164) ^ [_446272] : [aSet0(_446272), 1930 ^ _382164 : [(1976 ^ _382164) ^ [] : [aElementOf0(_446272, slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _445807), szmzizndt0(sdtlpdtrp0(xN, _445807))), xk))], (1941 ^ _382164) ^ [_447188] : [aElementOf0(_447188, sdtmndt0(sdtlpdtrp0(xN, _445807), szmzizndt0(sdtlpdtrp0(xN, _445807)))), 1944 ^ _382164 : [(1949 ^ _382164) ^ [] : [_447188 = szmzizndt0(sdtlpdtrp0(xN, _445807))], (1947 ^ _382164) ^ [] : [-(aElementOf0(_447188, sdtlpdtrp0(xN, _445807)))], (1945 ^ _382164) ^ [] : [-(aElement0(_447188))]]], (1951 ^ _382164) ^ [_447550] : [-(aElementOf0(_447550, sdtmndt0(sdtlpdtrp0(xN, _445807), szmzizndt0(sdtlpdtrp0(xN, _445807))))), aElement0(_447550), aElementOf0(_447550, sdtlpdtrp0(xN, _445807)), -(_447550 = szmzizndt0(sdtlpdtrp0(xN, _445807)))], (1965 ^ _382164) ^ [] : [1967 ^ _382164 : [(1972 ^ _382164) ^ [] : [aSubsetOf0(_446272, sdtmndt0(sdtlpdtrp0(xN, _445807), szmzizndt0(sdtlpdtrp0(xN, _445807))))], (1970 ^ _382164) ^ [] : [aElementOf0(1966 ^ [_445807, _446272], sdtmndt0(sdtlpdtrp0(xN, _445807), szmzizndt0(sdtlpdtrp0(xN, _445807))))], (1968 ^ _382164) ^ [] : [-(aElementOf0(1966 ^ [_445807, _446272], _446272))]], sbrdtbr0(_446272) = xk], (1931 ^ _382164) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _445807)), sdtlpdtrp0(xN, _445807)))], (1933 ^ _382164) ^ [_446859] : [aElementOf0(_446859, sdtlpdtrp0(xN, _445807)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _445807)), _446859))], (1939 ^ _382164) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _445807), szmzizndt0(sdtlpdtrp0(xN, _445807)))))]], 1977 ^ _382164 : [(2020 ^ _382164) ^ [] : [-(sbrdtbr0(sdtpldt0(_446272, szmzizndt0(sdtlpdtrp0(xN, _445807)))) = xK)], (1978 ^ _382164) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _445807)), sdtlpdtrp0(xN, _445807)))], (1980 ^ _382164) ^ [_448519] : [aElementOf0(_448519, sdtlpdtrp0(xN, _445807)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _445807)), _448519))], (2012 ^ _382164) ^ [_449611] : [aElementOf0(_449611, sdtpldt0(_446272, szmzizndt0(sdtlpdtrp0(xN, _445807)))), -(aElementOf0(_449611, xS))], (2022 ^ _382164) ^ [] : [-(aElementOf0(sdtpldt0(_446272, szmzizndt0(sdtlpdtrp0(xN, _445807))), slbdtsldtrb0(xS, xK)))], (2000 ^ _382164) ^ [_449210] : [-(aElementOf0(_449210, sdtpldt0(_446272, szmzizndt0(sdtlpdtrp0(xN, _445807))))), aElement0(_449210), 2005 ^ _382164 : [(2008 ^ _382164) ^ [] : [_449210 = szmzizndt0(sdtlpdtrp0(xN, _445807))], (2006 ^ _382164) ^ [] : [aElementOf0(_449210, _446272)]]], (2018 ^ _382164) ^ [] : [-(aSubsetOf0(sdtpldt0(_446272, szmzizndt0(sdtlpdtrp0(xN, _445807))), xS))], (1988 ^ _382164) ^ [_448843] : [aElementOf0(_448843, sdtpldt0(_446272, szmzizndt0(sdtlpdtrp0(xN, _445807)))), 1991 ^ _382164 : [(1994 ^ _382164) ^ [] : [-(aElementOf0(_448843, _446272)), -(_448843 = szmzizndt0(sdtlpdtrp0(xN, _445807)))], (1992 ^ _382164) ^ [] : [-(aElement0(_448843))]]], (1986 ^ _382164) ^ [] : [-(aSet0(sdtpldt0(_446272, szmzizndt0(sdtlpdtrp0(xN, _445807)))))]]]]], (1393 ^ _382164) ^ [_425885, _425887] : [-(aSubsetOf0(sdtlbdtrb0(_425887, _425885), szDzozmdt0(_425887))), aFunction0(_425887), aElement0(_425885)], (2192 ^ _382164) ^ [_456769] : [aElementOf0(_456769, szNzAzT0), 2195 ^ _382164 : [(2196 ^ _382164) ^ [] : [-(aSet0(sdtlcdtrc0(sdtlpdtrp0(xC, _456769), szDzozmdt0(sdtlpdtrp0(xC, _456769)))))], (2217 ^ _382164) ^ [_457890] : [aElementOf0(_457890, sdtlcdtrc0(sdtlpdtrp0(xC, _456769), szDzozmdt0(sdtlpdtrp0(xC, _456769)))), -(aElementOf0(_457890, xT))], (2207 ^ _382164) ^ [_457483] : [-(aElementOf0(_457483, sdtlcdtrc0(sdtlpdtrp0(xC, _456769), szDzozmdt0(sdtlpdtrp0(xC, _456769))))), 2208 ^ _382164 : [(2209 ^ _382164) ^ [_457599] : [aElementOf0(_457599, szDzozmdt0(sdtlpdtrp0(xC, _456769))), sdtlpdtrp0(sdtlpdtrp0(xC, _456769), _457599) = _457483]]], (2198 ^ _382164) ^ [_457119] : [aElementOf0(_457119, sdtlcdtrc0(sdtlpdtrp0(xC, _456769), szDzozmdt0(sdtlpdtrp0(xC, _456769)))), 2202 ^ _382164 : [(2205 ^ _382164) ^ [] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _456769), 2201 ^ [_456769, _457119]) = _457119)], (2203 ^ _382164) ^ [] : [-(aElementOf0(2201 ^ [_456769, _457119], szDzozmdt0(sdtlpdtrp0(xC, _456769))))]]], (2223 ^ _382164) ^ [] : [-(aSubsetOf0(sdtlcdtrc0(sdtlpdtrp0(xC, _456769), szDzozmdt0(sdtlpdtrp0(xC, _456769))), xT))]]], (715 ^ _382164) ^ [_404837] : [aElementOf0(_404837, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_404837), sz00)], (747 ^ _382164) ^ [_405789] : [aElementOf0(_405789, szNzAzT0), -(sdtlseqdt0(_405789, _405789))], (2575 ^ _382164) ^ [_472009] : [-(aElementOf0(_472009, xO)), 2576 ^ _382164 : [(2577 ^ _382164) ^ [_472102] : [aElementOf0(_472102, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlpdtrp0(xe, _472102) = _472009]]], (2534 ^ _382164) ^ [_470720] : [-(aElementOf0(_470720, sdtlbdtrb0(xd, szDzizrdt0(xd)))), aElementOf0(_470720, szDzozmdt0(xd)), sdtlpdtrp0(xd, _470720) = szDzizrdt0(xd)], (650 ^ _382164) ^ [_402901] : [aElementOf0(_402901, szNzAzT0), 653 ^ _382164 : [(656 ^ _382164) ^ [] : [szszuzczcdt0(_402901) = sz00], (654 ^ _382164) ^ [] : [-(aElementOf0(szszuzczcdt0(_402901), szNzAzT0))]]], (2026 ^ _382164) ^ [] : [-(szDzozmdt0(xC) = szNzAzT0)], (709 ^ _382164) ^ [_404647] : [aElementOf0(_404647, szNzAzT0), -(sdtlseqdt0(sz00, _404647))], (196 ^ _382164) ^ [_388691, _388693] : [_388693 = _388691, -(szDzozmdt0(_388693) = szDzozmdt0(_388691))], (564 ^ _382164) ^ [_400271] : [aSet0(_400271), 567 ^ _382164 : [(568 ^ _382164) ^ [_400408] : [aElementOf0(_400408, _400271), -(sdtpldt0(sdtmndt0(_400271, _400408), _400408) = _400271)]]], (1785 ^ _382164) ^ [] : [-(sdtlpdtrp0(xN, sz00) = xS)], (212 ^ _382164) ^ [_389296, _389298, _389300, _389302] : [-(sdtlbdtrb0(_389302, _389298) = sdtlbdtrb0(_389300, _389296)), _389302 = _389300, _389298 = _389296], (1777 ^ _382164) ^ [] : [-(aElementOf0(xk, szNzAzT0))], (2 ^ _382164) ^ [_382288] : [-(_382288 = _382288)], (404 ^ _382164) ^ [_395089, _395091, _395093] : [aSet0(_395093), aSet0(_395091), aSet0(_395089), -(aSubsetOf0(_395093, _395089)), aSubsetOf0(_395093, _395091), aSubsetOf0(_395091, _395089)], (268 ^ _382164) ^ [_391097] : [aSet0(_391097), isFinite0(_391097), true___, -(true___)], (180 ^ _382164) ^ [_388142, _388144, _388146, _388148] : [-(slbdtsldtrb0(_388148, _388144) = slbdtsldtrb0(_388146, _388142)), _388148 = _388146, _388144 = _388142], (1589 ^ _382164) ^ [_433036] : [-(aElementOf0(_433036, szDzozmdt0(xc))), sbrdtbr0(_433036) = xK, 1592 ^ _382164 : [(1593 ^ _382164) ^ [] : [aSet0(_433036), 1597 ^ _382164 : [(1600 ^ _382164) ^ [] : [aElementOf0(1596 ^ [_433036], xS)], (1598 ^ _382164) ^ [] : [-(aElementOf0(1596 ^ [_433036], _433036))]]], (1602 ^ _382164) ^ [] : [aSubsetOf0(_433036, xS)]]], (303 ^ _382164) ^ [_392098] : [aSet0(_392098), isCountable0(_392098), true___, -(true___)], (1608 ^ _382164) ^ [] : [-(szDzozmdt0(xc) = slbdtsldtrb0(xS, xK))], (741 ^ _382164) ^ [_405595] : [aElementOf0(_405595, szNzAzT0), -(sdtlseqdt0(_405595, szszuzczcdt0(_405595)))], (1287 ^ _382164) ^ [_422283, _422285] : [aSet0(_422285), aElementOf0(_422283, szNzAzT0), 1294 ^ _382164 : [(1295 ^ _382164) ^ [_422534] : [1303 ^ _382164 : [(1308 ^ _382164) ^ [] : [-(aSubsetOf0(_422534, slbdtsldtrb0(1302 ^ [_422283, _422285, _422534], _422283)))], (1306 ^ _382164) ^ [] : [-(isFinite0(1302 ^ [_422283, _422285, _422534]))], (1304 ^ _382164) ^ [] : [-(aSubsetOf0(1302 ^ [_422283, _422285, _422534], _422285))]], aSubsetOf0(_422534, slbdtsldtrb0(_422285, _422283)), isFinite0(_422534)]]], (602 ^ _382164) ^ [_401453] : [aElement0(_401453), 605 ^ _382164 : [(606 ^ _382164) ^ [_401590] : [-(isCountable0(sdtmndt0(_401590, _401453))), aSet0(_401590), isCountable0(_401590)]]], (1775 ^ _382164) ^ [] : [xK = sz00], (1119 ^ _382164) ^ [_416976, _416978] : [aElementOf0(_416978, szNzAzT0), aElementOf0(_416976, szNzAzT0), 1126 ^ _382164 : [(1133 ^ _382164) ^ [] : [aSubsetOf0(slbdtrb0(_416978), slbdtrb0(_416976)), -(sdtlseqdt0(_416978, _416976))], (1127 ^ _382164) ^ [] : [sdtlseqdt0(_416978, _416976), -(aSubsetOf0(slbdtrb0(_416978), slbdtrb0(_416976)))]]], (2466 ^ _382164) ^ [] : [-(szDzozmdt0(xd) = szNzAzT0)], (68 ^ _382164) ^ [_384390, _384392] : [-(aFunction0(_384390)), _384392 = _384390, aFunction0(_384392)], (190 ^ _382164) ^ [_388473, _388475] : [_388475 = _388473, -(szszuzczcdt0(_388475) = szszuzczcdt0(_388473))], (282 ^ _382164) ^ [_391467] : [_391467 = slcrc0, 285 ^ _382164 : [(288 ^ _382164) ^ [_391648] : [aElementOf0(_391648, _391467)], (286 ^ _382164) ^ [] : [-(aSet0(_391467))]]], (1511 ^ _382164) ^ [_430392] : [aFunction0(_430392), 1514 ^ _382164 : [(1515 ^ _382164) ^ [_430580] : [aSubsetOf0(_430580, szDzozmdt0(_430392)), isCountable0(_430580), 1526 ^ _382164 : [(1529 ^ _382164) ^ [] : [-(aElementOf0(1525 ^ [_430392, _430580], szDzozmdt0(_430392)))], (1531 ^ _382164) ^ [] : [1524 ^ [_430392, _430580] = 1525 ^ [_430392, _430580]], (1533 ^ _382164) ^ [] : [-(sdtlpdtrp0(_430392, 1524 ^ [_430392, _430580]) = sdtlpdtrp0(_430392, 1525 ^ [_430392, _430580]))], (1527 ^ _382164) ^ [] : [-(aElementOf0(1524 ^ [_430392, _430580], szDzozmdt0(_430392)))]], -(isCountable0(sdtlcdtrc0(_430392, _430580)))]]], (901 ^ _382164) ^ [_410168] : [aSet0(_410168), 904 ^ _382164 : [(905 ^ _382164) ^ [_410308] : [-(sdtlseqdt0(sbrdtbr0(_410308), sbrdtbr0(_410168))), isFinite0(_410168), aSubsetOf0(_410308, _410168)]]], (2343 ^ _382164) ^ [_463247] : [aElementOf0(_463247, szNzAzT0), 2347 ^ _382164 : [(2371 ^ _382164) ^ [_464956] : [-(aElementOf0(_464956, sdtmndt0(sdtlpdtrp0(xN, _463247), szmzizndt0(sdtlpdtrp0(xN, _463247))))), aElement0(_464956), aElementOf0(_464956, sdtlpdtrp0(xN, _463247)), -(_464956 = szmzizndt0(sdtlpdtrp0(xN, _463247)))], (2395 ^ _382164) ^ [] : [-(isCountable0(2349 ^ [_463247]))], (2361 ^ _382164) ^ [_464606] : [aElementOf0(_464606, sdtmndt0(sdtlpdtrp0(xN, _463247), szmzizndt0(sdtlpdtrp0(xN, _463247)))), 2364 ^ _382164 : [(2369 ^ _382164) ^ [] : [_464606 = szmzizndt0(sdtlpdtrp0(xN, _463247))], (2367 ^ _382164) ^ [] : [-(aElementOf0(_464606, sdtlpdtrp0(xN, _463247)))], (2365 ^ _382164) ^ [] : [-(aElement0(_464606))]]], (2385 ^ _382164) ^ [] : [-(aSet0(2349 ^ [_463247]))], (2348 ^ _382164) ^ [] : [-(aElementOf0(2346 ^ [_463247], xT))], (2351 ^ _382164) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _463247)), sdtlpdtrp0(xN, _463247)))], (2353 ^ _382164) ^ [_464289] : [aElementOf0(_464289, sdtlpdtrp0(xN, _463247)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _463247)), _464289))], (2359 ^ _382164) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _463247), szmzizndt0(sdtlpdtrp0(xN, _463247)))))], (2387 ^ _382164) ^ [_465441] : [aElementOf0(_465441, 2349 ^ [_463247]), -(aElementOf0(_465441, sdtmndt0(sdtlpdtrp0(xN, _463247), szmzizndt0(sdtlpdtrp0(xN, _463247)))))], (2393 ^ _382164) ^ [] : [-(aSubsetOf0(2349 ^ [_463247], sdtmndt0(sdtlpdtrp0(xN, _463247), szmzizndt0(sdtlpdtrp0(xN, _463247)))))], (2397 ^ _382164) ^ [_465799] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _463247), _465799) = 2346 ^ [_463247]), aSet0(_465799), 2402 ^ _382164 : [(2403 ^ _382164) ^ [] : [2405 ^ _382164 : [(2410 ^ _382164) ^ [] : [aSubsetOf0(_465799, 2349 ^ [_463247])], (2408 ^ _382164) ^ [] : [aElementOf0(2404 ^ [_463247, _465799], 2349 ^ [_463247])], (2406 ^ _382164) ^ [] : [-(aElementOf0(2404 ^ [_463247, _465799], _465799))]], sbrdtbr0(_465799) = xk], (2414 ^ _382164) ^ [] : [aElementOf0(_465799, slbdtsldtrb0(2349 ^ [_463247], xk))]]]]], (2548 ^ _382164) ^ [_471162] : [aElementOf0(_471162, sdtlbdtrb0(xd, szDzizrdt0(xd))), 2551 ^ _382164 : [(2554 ^ _382164) ^ [] : [-(sdtlpdtrp0(xd, _471162) = szDzizrdt0(xd))], (2552 ^ _382164) ^ [] : [-(aElementOf0(_471162, szDzozmdt0(xd)))]]], (616 ^ _382164) ^ [_401882] : [aElement0(_401882), 619 ^ _382164 : [(620 ^ _382164) ^ [_402019] : [-(isFinite0(sdtpldt0(_402019, _401882))), aSet0(_402019), isFinite0(_402019)]]], (1472 ^ _382164) ^ [_428908] : [aFunction0(_428908), 1475 ^ _382164 : [(1476 ^ _382164) ^ [_429085] : [aSubsetOf0(_429085, szDzozmdt0(_428908)), 1479 ^ _382164 : [(1494 ^ _382164) ^ [_429798] : [-(_429798 = sdtexdt0(_428908, _429085)), aFunction0(_429798), szDzozmdt0(_429798) = _429085, 1504 ^ _382164 : [(1507 ^ _382164) ^ [] : [sdtlpdtrp0(_429798, 1503 ^ [_428908, _429085, _429798]) = sdtlpdtrp0(_428908, 1503 ^ [_428908, _429085, _429798])], (1505 ^ _382164) ^ [] : [-(aElementOf0(1503 ^ [_428908, _429085, _429798], _429085))]]], (1480 ^ _382164) ^ [_429290] : [_429290 = sdtexdt0(_428908, _429085), 1483 ^ _382164 : [(1488 ^ _382164) ^ [_429597] : [aElementOf0(_429597, _429085), -(sdtlpdtrp0(_429290, _429597) = sdtlpdtrp0(_428908, _429597))], (1486 ^ _382164) ^ [] : [-(szDzozmdt0(_429290) = _429085)], (1484 ^ _382164) ^ [] : [-(aFunction0(_429290))]]]]]]], (1783 ^ _382164) ^ [] : [-(szDzozmdt0(xN) = szNzAzT0)], (202 ^ _382164) ^ [_388937, _388939, _388941, _388943] : [-(sdtlcdtrc0(_388943, _388939) = sdtlcdtrc0(_388941, _388937)), _388943 = _388941, _388939 = _388937], (2468 ^ _382164) ^ [_468434] : [aElementOf0(_468434, szNzAzT0), 2471 ^ _382164 : [(2472 ^ _382164) ^ [_468630] : [-(sdtlpdtrp0(xd, _468434) = sdtlpdtrp0(sdtlpdtrp0(xC, _468434), _468630)), aSet0(_468630), 2477 ^ _382164 : [(2478 ^ _382164) ^ [] : [2480 ^ _382164 : [(2485 ^ _382164) ^ [] : [aSubsetOf0(_468630, sdtlpdtrp0(xN, szszuzczcdt0(_468434)))], (2483 ^ _382164) ^ [] : [aElementOf0(2479 ^ [_468434, _468630], sdtlpdtrp0(xN, szszuzczcdt0(_468434)))], (2481 ^ _382164) ^ [] : [-(aElementOf0(2479 ^ [_468434, _468630], _468630))]], sbrdtbr0(_468630) = xk], (2489 ^ _382164) ^ [] : [aElementOf0(_468630, slbdtsldtrb0(sdtlpdtrp0(xN, szszuzczcdt0(_468434)), xk))]]]]], (2617 ^ _382164) ^ [] : [-(aElementOf0(xi, szNzAzT0))], (1085 ^ _382164) ^ [_415990] : [aElementOf0(_415990, szNzAzT0), -(isFinite0(slbdtrb0(_415990)))], (2522 ^ _382164) ^ [] : [-(aElementOf0(szDzizrdt0(xd), xT))], (158 ^ _382164) ^ [_387347, _387349, _387351, _387353] : [-(sdtmndt0(_387353, _387349) = sdtmndt0(_387351, _387347)), _387353 = _387351, _387349 = _387347], (2028 ^ _382164) ^ [_450179] : [aElementOf0(_450179, szNzAzT0), 2031 ^ _382164 : [(2042 ^ _382164) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _450179), szmzizndt0(sdtlpdtrp0(xN, _450179)))))], (2105 ^ _382164) ^ [_453461] : [2157 ^ _382164 : [(2158 ^ _382164) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _450179)), sdtlpdtrp0(xN, _450179)))], (2190 ^ _382164) ^ [] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _450179), _453461) = sdtlpdtrp0(xc, sdtpldt0(_453461, szmzizndt0(sdtlpdtrp0(xN, _450179)))))], (2178 ^ _382164) ^ [_456267] : [-(aElementOf0(_456267, sdtpldt0(_453461, szmzizndt0(sdtlpdtrp0(xN, _450179))))), aElement0(_456267), 2183 ^ _382164 : [(2186 ^ _382164) ^ [] : [_456267 = szmzizndt0(sdtlpdtrp0(xN, _450179))], (2184 ^ _382164) ^ [] : [aElementOf0(_456267, _453461)]]], (2166 ^ _382164) ^ [_455900] : [aElementOf0(_455900, sdtpldt0(_453461, szmzizndt0(sdtlpdtrp0(xN, _450179)))), 2169 ^ _382164 : [(2172 ^ _382164) ^ [] : [-(aElementOf0(_455900, _453461)), -(_455900 = szmzizndt0(sdtlpdtrp0(xN, _450179)))], (2170 ^ _382164) ^ [] : [-(aElement0(_455900))]]], (2160 ^ _382164) ^ [_455649] : [aElementOf0(_455649, sdtlpdtrp0(xN, _450179)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _450179)), _455649))]], aSet0(_453461), 2110 ^ _382164 : [(2156 ^ _382164) ^ [] : [aElementOf0(_453461, slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _450179), szmzizndt0(sdtlpdtrp0(xN, _450179))), xk))], (2121 ^ _382164) ^ [_454318] : [aElementOf0(_454318, sdtmndt0(sdtlpdtrp0(xN, _450179), szmzizndt0(sdtlpdtrp0(xN, _450179)))), 2124 ^ _382164 : [(2129 ^ _382164) ^ [] : [_454318 = szmzizndt0(sdtlpdtrp0(xN, _450179))], (2127 ^ _382164) ^ [] : [-(aElementOf0(_454318, sdtlpdtrp0(xN, _450179)))], (2125 ^ _382164) ^ [] : [-(aElement0(_454318))]]], (2131 ^ _382164) ^ [_454680] : [-(aElementOf0(_454680, sdtmndt0(sdtlpdtrp0(xN, _450179), szmzizndt0(sdtlpdtrp0(xN, _450179))))), aElement0(_454680), aElementOf0(_454680, sdtlpdtrp0(xN, _450179)), -(_454680 = szmzizndt0(sdtlpdtrp0(xN, _450179)))], (2145 ^ _382164) ^ [] : [2147 ^ _382164 : [(2152 ^ _382164) ^ [] : [aSubsetOf0(_453461, sdtmndt0(sdtlpdtrp0(xN, _450179), szmzizndt0(sdtlpdtrp0(xN, _450179))))], (2150 ^ _382164) ^ [] : [aElementOf0(2146 ^ [_450179, _453461], sdtmndt0(sdtlpdtrp0(xN, _450179), szmzizndt0(sdtlpdtrp0(xN, _450179))))], (2148 ^ _382164) ^ [] : [-(aElementOf0(2146 ^ [_450179, _453461], _453461))]], sbrdtbr0(_453461) = xk], (2111 ^ _382164) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _450179)), sdtlpdtrp0(xN, _450179)))], (2113 ^ _382164) ^ [_453989] : [aElementOf0(_453989, sdtlpdtrp0(xN, _450179)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _450179)), _453989))], (2119 ^ _382164) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _450179), szmzizndt0(sdtlpdtrp0(xN, _450179)))))]]], (2034 ^ _382164) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _450179)), sdtlpdtrp0(xN, _450179)))], (2032 ^ _382164) ^ [] : [-(aFunction0(sdtlpdtrp0(xC, _450179)))], (2054 ^ _382164) ^ [_451690] : [-(aElementOf0(_451690, sdtmndt0(sdtlpdtrp0(xN, _450179), szmzizndt0(sdtlpdtrp0(xN, _450179))))), aElement0(_451690), aElementOf0(_451690, sdtlpdtrp0(xN, _450179)), -(_451690 = szmzizndt0(sdtlpdtrp0(xN, _450179)))], (2103 ^ _382164) ^ [] : [-(szDzozmdt0(sdtlpdtrp0(xC, _450179)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _450179), szmzizndt0(sdtlpdtrp0(xN, _450179))), xk))], (2036 ^ _382164) ^ [_451023] : [aElementOf0(_451023, sdtlpdtrp0(xN, _450179)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _450179)), _451023))], (2084 ^ _382164) ^ [_452734] : [-(aElementOf0(_452734, szDzozmdt0(sdtlpdtrp0(xC, _450179)))), sbrdtbr0(_452734) = xk, 2087 ^ _382164 : [(2088 ^ _382164) ^ [] : [aSet0(_452734), 2092 ^ _382164 : [(2095 ^ _382164) ^ [] : [aElementOf0(2091 ^ [_450179, _452734], sdtmndt0(sdtlpdtrp0(xN, _450179), szmzizndt0(sdtlpdtrp0(xN, _450179))))], (2093 ^ _382164) ^ [] : [-(aElementOf0(2091 ^ [_450179, _452734], _452734))]]], (2097 ^ _382164) ^ [] : [aSubsetOf0(_452734, sdtmndt0(sdtlpdtrp0(xN, _450179), szmzizndt0(sdtlpdtrp0(xN, _450179))))]]], (2044 ^ _382164) ^ [_451340] : [aElementOf0(_451340, sdtmndt0(sdtlpdtrp0(xN, _450179), szmzizndt0(sdtlpdtrp0(xN, _450179)))), 2047 ^ _382164 : [(2052 ^ _382164) ^ [] : [_451340 = szmzizndt0(sdtlpdtrp0(xN, _450179))], (2050 ^ _382164) ^ [] : [-(aElementOf0(_451340, sdtlpdtrp0(xN, _450179)))], (2048 ^ _382164) ^ [] : [-(aElement0(_451340))]]], (2068 ^ _382164) ^ [_452127] : [aElementOf0(_452127, szDzozmdt0(sdtlpdtrp0(xC, _450179))), 2071 ^ _382164 : [(2080 ^ _382164) ^ [] : [-(aSubsetOf0(_452127, sdtmndt0(sdtlpdtrp0(xN, _450179), szmzizndt0(sdtlpdtrp0(xN, _450179)))))], (2082 ^ _382164) ^ [] : [-(sbrdtbr0(_452127) = xk)], (2074 ^ _382164) ^ [_452402] : [aElementOf0(_452402, _452127), -(aElementOf0(_452402, sdtmndt0(sdtlpdtrp0(xN, _450179), szmzizndt0(sdtlpdtrp0(xN, _450179)))))], (2072 ^ _382164) ^ [] : [-(aSet0(_452127))]]]]], (2589 ^ _382164) ^ [] : [-(isCountable0(xO))], (2613 ^ _382164) ^ [] : [-(sdtlpdtrp0(xe, 2609 ^ []) = xx)], (1093 ^ _382164) ^ [_416249, _416251] : [aElementOf0(_416251, szNzAzT0), aElementOf0(_416249, szNzAzT0), 1100 ^ _382164 : [(1101 ^ _382164) ^ [] : [aElementOf0(_416251, slbdtrb0(szszuzczcdt0(_416249))), -(aElementOf0(_416251, slbdtrb0(_416249))), -(_416251 = _416249)], (1111 ^ _382164) ^ [] : [1112 ^ _382164 : [(1115 ^ _382164) ^ [] : [_416251 = _416249], (1113 ^ _382164) ^ [] : [aElementOf0(_416251, slbdtrb0(_416249))]], -(aElementOf0(_416251, slbdtrb0(szszuzczcdt0(_416249))))]]], (1261 ^ _382164) ^ [_421477] : [aElementOf0(_421477, szNzAzT0), 1264 ^ _382164 : [(1265 ^ _382164) ^ [_421664, _421666] : [aSet0(_421666), aSet0(_421664), -(_421477 = sz00), -(aSubsetOf0(_421666, _421664)), aSubsetOf0(slbdtsldtrb0(_421666, _421477), slbdtsldtrb0(_421664, _421477)), -(slbdtsldtrb0(_421666, _421477) = slcrc0)]]], (174 ^ _382164) ^ [_387896, _387898] : [_387898 = _387896, -(sbrdtbr0(_387898) = sbrdtbr0(_387896))], (258 ^ _382164) ^ [_390766] : [aSet0(_390766), 261 ^ _382164 : [(262 ^ _382164) ^ [_390896] : [aElementOf0(_390896, _390766), -(aElement0(_390896))]]], (2504 ^ _382164) ^ [_469772] : [-(aElementOf0(_469772, sdtlcdtrc0(xd, szDzozmdt0(xd)))), 2505 ^ _382164 : [(2506 ^ _382164) ^ [_469865] : [aElementOf0(_469865, szDzozmdt0(xd)), sdtlpdtrp0(xd, _469865) = _469772]]], (4 ^ _382164) ^ [_382395, _382397] : [_382397 = _382395, -(_382395 = _382397)], (1091 ^ _382164) ^ [] : [-(slbdtrb0(sz00) = slcrc0)], (1139 ^ _382164) ^ [_417525] : [1147 ^ _382164 : [(1150 ^ _382164) ^ [] : [-(aSubsetOf0(_417525, slbdtrb0(1146 ^ [_417525])))], (1148 ^ _382164) ^ [] : [-(aElementOf0(1146 ^ [_417525], szNzAzT0))]], aSubsetOf0(_417525, szNzAzT0), isFinite0(_417525)], (1215 ^ _382164) ^ [_420093] : [aSet0(_420093), isFinite0(_420093), 1222 ^ _382164 : [(1223 ^ _382164) ^ [_420309] : [aElementOf0(_420309, szNzAzT0), -(isFinite0(slbdtsldtrb0(_420093, _420309)))]]], (2446 ^ _382164) ^ [] : [-(aFunction0(xe))], (644 ^ _382164) ^ [] : [-(aSet0(szNzAzT0))], (1573 ^ _382164) ^ [_432514] : [aElementOf0(_432514, szDzozmdt0(xc)), 1576 ^ _382164 : [(1585 ^ _382164) ^ [] : [-(aSubsetOf0(_432514, xS))], (1587 ^ _382164) ^ [] : [-(sbrdtbr0(_432514) = xK)], (1579 ^ _382164) ^ [_432749] : [aElementOf0(_432749, _432514), -(aElementOf0(_432749, xS))], (1577 ^ _382164) ^ [] : [-(aSet0(_432514))]]], (825 ^ _382164) ^ [_407923] : [aElementOf0(_407923, szNzAzT0), -(iLess0(_407923, szszuzczcdt0(_407923)))], (2585 ^ _382164) ^ [] : [-(xO = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))], (1006 ^ _382164) ^ [_413551, _413553] : [-(szmzizndt0(_413553) = szmzizndt0(_413551)), aElementOf0(szmzizndt0(_413553), _413551), aElementOf0(szmzizndt0(_413551), _413553), aSubsetOf0(_413553, szNzAzT0), aSubsetOf0(_413551, szNzAzT0), -(_413553 = slcrc0), -(_413551 = slcrc0)], (2514 ^ _382164) ^ [_470119] : [aElementOf0(_470119, sdtlcdtrc0(xd, szDzozmdt0(xd))), -(aElementOf0(_470119, xT))], (1610 ^ _382164) ^ [] : [-(aSet0(sdtlcdtrc0(xc, szDzozmdt0(xc))))], (1637 ^ _382164) ^ [] : [-(aSubsetOf0(sdtlcdtrc0(xc, szDzozmdt0(xc)), xT))], (1612 ^ _382164) ^ [_433742] : [aElementOf0(_433742, sdtlcdtrc0(xc, szDzozmdt0(xc))), 1616 ^ _382164 : [(1619 ^ _382164) ^ [] : [-(sdtlpdtrp0(xc, 1615 ^ [_433742]) = _433742)], (1617 ^ _382164) ^ [] : [-(aElementOf0(1615 ^ [_433742], szDzozmdt0(xc)))]]], (44 ^ _382164) ^ [_383651, _383653] : [-(aElement0(_383651)), _383653 = _383651, aElement0(_383653)], (2524 ^ _382164) ^ [] : [-(aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd))))], (1854 ^ _382164) ^ [_443479] : [aElementOf0(_443479, szNzAzT0), 1857 ^ _382164 : [(1866 ^ _382164) ^ [] : [-(aSubsetOf0(sdtlpdtrp0(xN, _443479), szNzAzT0))], (1868 ^ _382164) ^ [] : [-(isCountable0(sdtlpdtrp0(xN, _443479)))], (1860 ^ _382164) ^ [_443726] : [aElementOf0(_443726, sdtlpdtrp0(xN, _443479)), -(aElementOf0(_443726, szNzAzT0))], (1858 ^ _382164) ^ [] : [-(aSet0(sdtlpdtrp0(xN, _443479)))]]], (915 ^ _382164) ^ [_410620, _410622] : [aSet0(_410622), aElementOf0(_410620, szNzAzT0), 931 ^ _382164 : [(934 ^ _382164) ^ [] : [-(sbrdtbr0(930 ^ [_410620, _410622]) = _410620)], (932 ^ _382164) ^ [] : [-(aSubsetOf0(930 ^ [_410620, _410622], _410622))]], isFinite0(_410622), sdtlseqdt0(_410620, sbrdtbr0(_410622))], (1336 ^ _382164) ^ [_423901, _423903] : [aFunction0(_423903), aElement0(_423901), 1343 ^ _382164 : [(1344 ^ _382164) ^ [_424182] : [_424182 = sdtlbdtrb0(_423903, _423901), 1347 ^ _382164 : [(1358 ^ _382164) ^ [_424714] : [-(aElementOf0(_424714, _424182)), aElementOf0(_424714, szDzozmdt0(_423903)), sdtlpdtrp0(_423903, _424714) = _423901], (1350 ^ _382164) ^ [_424445] : [aElementOf0(_424445, _424182), 1353 ^ _382164 : [(1356 ^ _382164) ^ [] : [-(sdtlpdtrp0(_423903, _424445) = _423901)], (1354 ^ _382164) ^ [] : [-(aElementOf0(_424445, szDzozmdt0(_423903)))]]], (1348 ^ _382164) ^ [] : [-(aSet0(_424182))]]], (1368 ^ _382164) ^ [_425010] : [-(_425010 = sdtlbdtrb0(_423903, _423901)), aSet0(_425010), 1384 ^ _382164 : [(1389 ^ _382164) ^ [] : [aElementOf0(1373 ^ [_423901, _423903, _425010], _425010)], (1387 ^ _382164) ^ [] : [-(sdtlpdtrp0(_423903, 1373 ^ [_423901, _423903, _425010]) = _423901)], (1385 ^ _382164) ^ [] : [-(aElementOf0(1373 ^ [_423901, _423903, _425010], szDzozmdt0(_423903)))]], 1376 ^ _382164 : [(1379 ^ _382164) ^ [] : [aElementOf0(1373 ^ [_423901, _423903, _425010], szDzozmdt0(_423903)), sdtlpdtrp0(_423903, 1373 ^ [_423901, _423903, _425010]) = _423901], (1377 ^ _382164) ^ [] : [-(aElementOf0(1373 ^ [_423901, _423903, _425010], _425010))]]]]], (366 ^ _382164) ^ [_393982] : [aSet0(_393982), isFinite0(_393982), 373 ^ _382164 : [(374 ^ _382164) ^ [_394195] : [aSubsetOf0(_394195, _393982), -(isFinite0(_394195))]]], (648 ^ _382164) ^ [] : [-(aElementOf0(sz00, szNzAzT0))], (2587 ^ _382164) ^ [] : [-(aSet0(xO))], (1310 ^ _382164) ^ [_423096] : [aFunction0(_423096), true___, -(true___)], (426 ^ _382164) ^ [_395675, _395677] : [aSet0(_395677), aElement0(_395675), 433 ^ _382164 : [(434 ^ _382164) ^ [_395956] : [_395956 = sdtpldt0(_395677, _395675), 437 ^ _382164 : [(452 ^ _382164) ^ [_396574] : [-(aElementOf0(_396574, _395956)), aElement0(_396574), 457 ^ _382164 : [(460 ^ _382164) ^ [] : [_396574 = _395675], (458 ^ _382164) ^ [] : [aElementOf0(_396574, _395677)]]], (440 ^ _382164) ^ [_396219] : [aElementOf0(_396219, _395956), 443 ^ _382164 : [(446 ^ _382164) ^ [] : [-(aElementOf0(_396219, _395677)), -(_396219 = _395675)], (444 ^ _382164) ^ [] : [-(aElement0(_396219))]]], (438 ^ _382164) ^ [] : [-(aSet0(_395956))]]], (464 ^ _382164) ^ [_396936] : [-(_396936 = sdtpldt0(_395677, _395675)), aSet0(_396936), 472 ^ _382164 : [(475 ^ _382164) ^ [] : [aElement0(469 ^ [_395675, _395677, _396936]), 478 ^ _382164 : [(481 ^ _382164) ^ [] : [469 ^ [_395675, _395677, _396936] = _395675], (479 ^ _382164) ^ [] : [aElementOf0(469 ^ [_395675, _395677, _396936], _395677)]]], (473 ^ _382164) ^ [] : [-(aElementOf0(469 ^ [_395675, _395677, _396936], _396936))]], 482 ^ _382164 : [(485 ^ _382164) ^ [] : [-(aElementOf0(469 ^ [_395675, _395677, _396936], _395677)), -(469 ^ [_395675, _395677, _396936] = _395675)], (483 ^ _382164) ^ [] : [-(aElement0(469 ^ [_395675, _395677, _396936]))], (491 ^ _382164) ^ [] : [aElementOf0(469 ^ [_395675, _395677, _396936], _396936)]]]]], (112 ^ _382164) ^ [_385727, _385729, _385731, _385733] : [-(aSubsetOf0(_385731, _385727)), aSubsetOf0(_385733, _385729), _385733 = _385731, _385729 = _385727], (1229 ^ _382164) ^ [_420518] : [aSet0(_420518), -(isFinite0(_420518)), 1236 ^ _382164 : [(1237 ^ _382164) ^ [_420740] : [aElementOf0(_420740, szNzAzT0), slbdtsldtrb0(_420518, _420740) = slcrc0]]], (1567 ^ _382164) ^ [] : [-(aSubsetOf0(xS, szNzAzT0))], (380 ^ _382164) ^ [_394398] : [aSet0(_394398), -(aSubsetOf0(_394398, _394398))], (2418 ^ _382164) ^ [_466559] : [aElementOf0(_466559, szNzAzT0), 2422 ^ _382164 : [(2425 ^ _382164) ^ [_466950] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _466559), _466950) = 2421 ^ [_466559]), aSet0(_466950), 2430 ^ _382164 : [(2431 ^ _382164) ^ [] : [2433 ^ _382164 : [(2438 ^ _382164) ^ [] : [aSubsetOf0(_466950, sdtlpdtrp0(xN, szszuzczcdt0(_466559)))], (2436 ^ _382164) ^ [] : [aElementOf0(2432 ^ [_466559, _466950], sdtlpdtrp0(xN, szszuzczcdt0(_466559)))], (2434 ^ _382164) ^ [] : [-(aElementOf0(2432 ^ [_466559, _466950], _466950))]], sbrdtbr0(_466950) = xk], (2442 ^ _382164) ^ [] : [aElementOf0(_466950, slbdtsldtrb0(sdtlpdtrp0(xN, szszuzczcdt0(_466559)), xk))]]], (2423 ^ _382164) ^ [] : [-(aElementOf0(2421 ^ [_466559], xT))]]], (1326 ^ _382164) ^ [_423541] : [aFunction0(_423541), 1329 ^ _382164 : [(1330 ^ _382164) ^ [_423676] : [aElementOf0(_423676, szDzozmdt0(_423541)), -(aElement0(sdtlpdtrp0(_423541, _423676)))]]], (78 ^ _382164) ^ [_384685, _384687] : [-(aSet0(_384685)), _384687 = _384685, aSet0(_384687)], (2448 ^ _382164) ^ [] : [-(szDzozmdt0(xe) = szNzAzT0)], (98 ^ _382164) ^ [_385303, _385305, _385307, _385309] : [-(aElementOf0(_385307, _385303)), aElementOf0(_385309, _385305), _385309 = _385307, _385305 = _385303], (1152 ^ _382164) ^ [_417939] : [aElementOf0(_417939, szNzAzT0), -(sbrdtbr0(slbdtrb0(_417939)) = _417939)], (222 ^ _382164) ^ [_389627, _389629] : [_389629 = _389627, -(szDzizrdt0(_389629) = szDzizrdt0(_389627))], (658 ^ _382164) ^ [_403187, _403189] : [aElementOf0(_403189, szNzAzT0), aElementOf0(_403187, szNzAzT0), szszuzczcdt0(_403189) = szszuzczcdt0(_403187), -(_403189 = _403187)], (1320 ^ _382164) ^ [_423351] : [aFunction0(_423351), -(aSet0(szDzozmdt0(_423351)))], (630 ^ _382164) ^ [_402311] : [aElement0(_402311), 633 ^ _382164 : [(634 ^ _382164) ^ [_402448] : [-(isFinite0(sdtmndt0(_402448, _402311))), aSet0(_402448), isFinite0(_402448)]]], (1773 ^ _382164) ^ [] : [xK = sz00], (2619 ^ _382164) ^ [] : [-(sdtlpdtrp0(xe, xi) = xx)], (771 ^ _382164) ^ [_406486, _406488, _406490] : [aElementOf0(_406490, szNzAzT0), aElementOf0(_406488, szNzAzT0), aElementOf0(_406486, szNzAzT0), -(sdtlseqdt0(_406490, _406486)), sdtlseqdt0(_406490, _406488), sdtlseqdt0(_406488, _406486)], (1621 ^ _382164) ^ [_434042] : [-(aElementOf0(_434042, sdtlcdtrc0(xc, szDzozmdt0(xc)))), 1622 ^ _382164 : [(1623 ^ _382164) ^ [_434135] : [aElementOf0(_434135, szDzozmdt0(xc)), sdtlpdtrp0(xc, _434135) = _434042]]], (1559 ^ _382164) ^ [] : [-(aSet0(xS))], (1779 ^ _382164) ^ [] : [-(szszuzczcdt0(xk) = xK)], (88 ^ _382164) ^ [_384980, _384982] : [-(isCountable0(_384980)), _384982 = _384980, isCountable0(_384982)], (301 ^ _382164) ^ [] : [-(isFinite0(slcrc0))], (1569 ^ _382164) ^ [] : [-(isCountable0(xS))], (386 ^ _382164) ^ [_394600, _394602] : [aSet0(_394602), aSet0(_394600), -(_394602 = _394600), aSubsetOf0(_394602, _394600), aSubsetOf0(_394600, _394602)], (2450 ^ _382164) ^ [_467798] : [aElementOf0(_467798, szNzAzT0), 2453 ^ _382164 : [(2456 ^ _382164) ^ [_468053] : [aElementOf0(_468053, sdtlpdtrp0(xN, _467798)), -(sdtlseqdt0(sdtlpdtrp0(xe, _467798), _468053))], (2462 ^ _382164) ^ [] : [-(sdtlpdtrp0(xe, _467798) = szmzizndt0(sdtlpdtrp0(xN, _467798)))], (2454 ^ _382164) ^ [] : [-(aElementOf0(sdtlpdtrp0(xe, _467798), sdtlpdtrp0(xN, _467798)))]]], (168 ^ _382164) ^ [_387678, _387680] : [_387680 = _387678, -(szmzizndt0(_387680) = szmzizndt0(_387678))], (1639 ^ _382164) ^ [_434628] : [aElementOf0(_434628, szNzAzT0), 1642 ^ _382164 : [(1643 ^ _382164) ^ [_435091] : [isCountable0(_435091), 1646 ^ _382164 : [(1647 ^ _382164) ^ [] : [aSet0(_435091), 1651 ^ _382164 : [(1654 ^ _382164) ^ [] : [aElementOf0(1650 ^ [_434628, _435091], szNzAzT0)], (1652 ^ _382164) ^ [] : [-(aElementOf0(1650 ^ [_434628, _435091], _435091))]]], (1656 ^ _382164) ^ [] : [aSubsetOf0(_435091, szNzAzT0)]], 1659 ^ _382164 : [(1660 ^ _382164) ^ [_435915] : [iLess0(_434628, xK), 1736 ^ _382164 : [(1740 ^ _382164) ^ [] : [-(aSet0(1738 ^ [_434628, _435091, _435915]))], (1737 ^ _382164) ^ [] : [-(aElementOf0(1735 ^ [_434628, _435091, _435915], xT))], (1752 ^ _382164) ^ [_439834] : [-(sdtlpdtrp0(_435915, _439834) = 1735 ^ [_434628, _435091, _435915]), 1753 ^ _382164 : [(1754 ^ _382164) ^ [] : [sbrdtbr0(_439834) = _434628, 1755 ^ _382164 : [(1756 ^ _382164) ^ [] : [aSet0(_439834), 1760 ^ _382164 : [(1763 ^ _382164) ^ [] : [aElementOf0(1759 ^ [_434628, _435091, _435915, _439834], 1738 ^ [_434628, _435091, _435915])], (1761 ^ _382164) ^ [] : [-(aElementOf0(1759 ^ [_434628, _435091, _435915, _439834], _439834))]]], (1765 ^ _382164) ^ [] : [aSubsetOf0(_439834, 1738 ^ [_434628, _435091, _435915])]]], (1769 ^ _382164) ^ [] : [aElementOf0(_439834, slbdtsldtrb0(1738 ^ [_434628, _435091, _435915], _434628))]]], (1748 ^ _382164) ^ [] : [-(aSubsetOf0(1738 ^ [_434628, _435091, _435915], _435091))], (1750 ^ _382164) ^ [] : [-(isCountable0(1738 ^ [_434628, _435091, _435915]))], (1742 ^ _382164) ^ [_439469] : [aElementOf0(_439469, 1738 ^ [_434628, _435091, _435915]), -(aElementOf0(_439469, _435091))]], aFunction0(_435915), 1668 ^ _382164 : [(1669 ^ _382164) ^ [] : [1687 ^ _382164 : [(1700 ^ _382164) ^ [] : [aElementOf0(1667 ^ [_434628, _435091, _435915], szDzozmdt0(_435915))], (1696 ^ _382164) ^ [] : [-(aSubsetOf0(1667 ^ [_434628, _435091, _435915], _435091))], (1690 ^ _382164) ^ [_437277] : [aElementOf0(_437277, 1667 ^ [_434628, _435091, _435915]), -(aElementOf0(_437277, _435091))], (1698 ^ _382164) ^ [] : [-(sbrdtbr0(1667 ^ [_434628, _435091, _435915]) = _434628)], (1688 ^ _382164) ^ [] : [-(aSet0(1667 ^ [_434628, _435091, _435915]))]], 1670 ^ _382164 : [(1673 ^ _382164) ^ [] : [sbrdtbr0(1667 ^ [_434628, _435091, _435915]) = _434628, 1674 ^ _382164 : [(1675 ^ _382164) ^ [] : [aSet0(1667 ^ [_434628, _435091, _435915]), 1679 ^ _382164 : [(1682 ^ _382164) ^ [] : [aElementOf0(1678 ^ [_434628, _435091, _435915], _435091)], (1680 ^ _382164) ^ [] : [-(aElementOf0(1678 ^ [_434628, _435091, _435915], 1667 ^ [_434628, _435091, _435915]))]]], (1684 ^ _382164) ^ [] : [aSubsetOf0(1667 ^ [_434628, _435091, _435915], _435091)]]], (1671 ^ _382164) ^ [] : [-(aElementOf0(1667 ^ [_434628, _435091, _435915], szDzozmdt0(_435915)))]]], (1702 ^ _382164) ^ [] : [szDzozmdt0(_435915) = slbdtsldtrb0(_435091, _434628)]], 1703 ^ _382164 : [(1728 ^ _382164) ^ [] : [aElementOf0(1724 ^ [_434628, _435091, _435915], xT)], (1726 ^ _382164) ^ [] : [-(aElementOf0(1724 ^ [_434628, _435091, _435915], sdtlcdtrc0(_435915, szDzozmdt0(_435915))))], (1715 ^ _382164) ^ [_438244] : [-(aElementOf0(_438244, sdtlcdtrc0(_435915, szDzozmdt0(_435915)))), 1716 ^ _382164 : [(1717 ^ _382164) ^ [_438356] : [aElementOf0(_438356, szDzozmdt0(_435915)), sdtlpdtrp0(_435915, _438356) = _438244]]], (1704 ^ _382164) ^ [] : [-(aSet0(sdtlcdtrc0(_435915, szDzozmdt0(_435915))))], (1706 ^ _382164) ^ [_437874] : [aElementOf0(_437874, sdtlcdtrc0(_435915, szDzozmdt0(_435915))), 1710 ^ _382164 : [(1713 ^ _382164) ^ [] : [-(sdtlpdtrp0(_435915, 1709 ^ [_434628, _435091, _435915, _437874]) = _437874)], (1711 ^ _382164) ^ [] : [-(aElementOf0(1709 ^ [_434628, _435091, _435915, _437874], szDzozmdt0(_435915)))]]], (1730 ^ _382164) ^ [] : [aSubsetOf0(sdtlcdtrc0(_435915, szDzozmdt0(_435915)), xT)]]]]]]], (1870 ^ _382164) ^ [_444070, _444072] : [aElementOf0(_444072, szNzAzT0), aElementOf0(_444070, szNzAzT0), sdtlseqdt0(_444070, _444072), 1881 ^ _382164 : [(1882 ^ _382164) ^ [_444419] : [aElementOf0(_444419, sdtlpdtrp0(xN, _444072)), -(aElementOf0(_444419, sdtlpdtrp0(xN, _444070)))], (1888 ^ _382164) ^ [] : [-(aSubsetOf0(sdtlpdtrp0(xN, _444072), sdtlpdtrp0(xN, _444070)))]]], (1781 ^ _382164) ^ [] : [-(aFunction0(xN))], (2493 ^ _382164) ^ [] : [-(aSet0(sdtlcdtrc0(xd, szDzozmdt0(xd))))], (2464 ^ _382164) ^ [] : [-(aFunction0(xd))], (337 ^ _382164) ^ [_392981] : [aSet0(_392981), 340 ^ _382164 : [(353 ^ _382164) ^ [_393545] : [-(aSubsetOf0(_393545, _392981)), aSet0(_393545), 359 ^ _382164 : [(362 ^ _382164) ^ [] : [aElementOf0(358 ^ [_392981, _393545], _392981)], (360 ^ _382164) ^ [] : [-(aElementOf0(358 ^ [_392981, _393545], _393545))]]], (341 ^ _382164) ^ [_393157] : [aSubsetOf0(_393157, _392981), 344 ^ _382164 : [(347 ^ _382164) ^ [_393366] : [aElementOf0(_393366, _393157), -(aElementOf0(_393366, _392981))], (345 ^ _382164) ^ [] : [-(aSet0(_393157))]]]]], (1537 ^ _382164) ^ [_431452] : [aFunction0(_431452), 1548 ^ _382164 : [(1551 ^ _382164) ^ [] : [-(isCountable0(sdtlbdtrb0(_431452, szDzizrdt0(_431452))))], (1549 ^ _382164) ^ [] : [-(aElement0(szDzizrdt0(_431452)))]], isCountable0(szDzozmdt0(_431452)), isFinite0(sdtlcdtrc0(_431452, szDzozmdt0(_431452)))], (969 ^ _382164) ^ [_412344] : [aSubsetOf0(_412344, szNzAzT0), isFinite0(_412344), -(_412344 = slcrc0), 980 ^ _382164 : [(993 ^ _382164) ^ [_413090] : [-(_413090 = szmzazxdt0(_412344)), aElementOf0(_413090, _412344), 999 ^ _382164 : [(1002 ^ _382164) ^ [] : [sdtlseqdt0(998 ^ [_412344, _413090], _413090)], (1000 ^ _382164) ^ [] : [-(aElementOf0(998 ^ [_412344, _413090], _412344))]]], (981 ^ _382164) ^ [_412696] : [_412696 = szmzazxdt0(_412344), 984 ^ _382164 : [(987 ^ _382164) ^ [_412911] : [aElementOf0(_412911, _412344), -(sdtlseqdt0(_412911, _412696))], (985 ^ _382164) ^ [] : [-(aElementOf0(_412696, _412344))]]]]], (1571 ^ _382164) ^ [] : [-(aFunction0(xc))], (936 ^ _382164) ^ [_411236] : [aSubsetOf0(_411236, szNzAzT0), -(_411236 = slcrc0), 943 ^ _382164 : [(956 ^ _382164) ^ [_411899] : [-(_411899 = szmzizndt0(_411236)), aElementOf0(_411899, _411236), 962 ^ _382164 : [(965 ^ _382164) ^ [] : [sdtlseqdt0(_411899, 961 ^ [_411236, _411899])], (963 ^ _382164) ^ [] : [-(aElementOf0(961 ^ [_411236, _411899], _411236))]]], (944 ^ _382164) ^ [_411505] : [_411505 = szmzizndt0(_411236), 947 ^ _382164 : [(950 ^ _382164) ^ [_411720] : [aElementOf0(_411720, _411236), -(sdtlseqdt0(_411505, _411720))], (948 ^ _382164) ^ [] : [-(aElementOf0(_411505, _411236))]]]]], (672 ^ _382164) ^ [_403571] : [aElementOf0(_403571, szNzAzT0), -(_403571 = sz00), 680 ^ _382164 : [(683 ^ _382164) ^ [] : [-(_403571 = szszuzczcdt0(679 ^ [_403571]))], (681 ^ _382164) ^ [] : [-(aElementOf0(679 ^ [_403571], szNzAzT0))]]], (495 ^ _382164) ^ [_397973, _397975] : [aSet0(_397975), aElement0(_397973), 502 ^ _382164 : [(503 ^ _382164) ^ [_398256] : [_398256 = sdtmndt0(_397975, _397973), 506 ^ _382164 : [(519 ^ _382164) ^ [_398857] : [-(aElementOf0(_398857, _398256)), aElement0(_398857), aElementOf0(_398857, _397975), -(_398857 = _397973)], (509 ^ _382164) ^ [_398521] : [aElementOf0(_398521, _398256), 512 ^ _382164 : [(517 ^ _382164) ^ [] : [_398521 = _397973], (515 ^ _382164) ^ [] : [-(aElementOf0(_398521, _397975))], (513 ^ _382164) ^ [] : [-(aElement0(_398521))]]], (507 ^ _382164) ^ [] : [-(aSet0(_398256))]]], (533 ^ _382164) ^ [_399241] : [-(_399241 = sdtmndt0(_397975, _397973)), aSet0(_399241), 553 ^ _382164 : [(556 ^ _382164) ^ [] : [-(aElementOf0(538 ^ [_397973, _397975, _399241], _397975))], (558 ^ _382164) ^ [] : [538 ^ [_397973, _397975, _399241] = _397973], (560 ^ _382164) ^ [] : [aElementOf0(538 ^ [_397973, _397975, _399241], _399241)], (554 ^ _382164) ^ [] : [-(aElement0(538 ^ [_397973, _397975, _399241]))]], 541 ^ _382164 : [(544 ^ _382164) ^ [] : [aElement0(538 ^ [_397973, _397975, _399241]), aElementOf0(538 ^ [_397973, _397975, _399241], _397975), -(538 ^ [_397973, _397975, _399241] = _397973)], (542 ^ _382164) ^ [] : [-(aElementOf0(538 ^ [_397973, _397975, _399241], _399241))]]]]], (2591 ^ _382164) ^ [_472507] : [2601 ^ _382164 : [(2604 ^ _382164) ^ [] : [-(sdtlpdtrp0(xd, 2600 ^ [_472507]) = szDzizrdt0(xd))], (2606 ^ _382164) ^ [] : [-(aElementOf0(2600 ^ [_472507], sdtlbdtrb0(xd, szDzizrdt0(xd))))], (2608 ^ _382164) ^ [] : [-(sdtlpdtrp0(xe, 2600 ^ [_472507]) = _472507)], (2602 ^ _382164) ^ [] : [-(aElementOf0(2600 ^ [_472507], szNzAzT0))]], 2592 ^ _382164 : [(2593 ^ _382164) ^ [_472655] : [aElementOf0(_472655, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlpdtrp0(xe, _472655) = _472507], (2599 ^ _382164) ^ [] : [aElementOf0(_472507, xO)]]], (721 ^ _382164) ^ [_405046, _405048] : [aElementOf0(_405048, szNzAzT0), aElementOf0(_405046, szNzAzT0), 728 ^ _382164 : [(735 ^ _382164) ^ [] : [sdtlseqdt0(szszuzczcdt0(_405048), szszuzczcdt0(_405046)), -(sdtlseqdt0(_405048, _405046))], (729 ^ _382164) ^ [] : [sdtlseqdt0(_405048, _405046), -(sdtlseqdt0(szszuzczcdt0(_405048), szszuzczcdt0(_405046)))]]], (1555 ^ _382164) ^ [] : [-(isFinite0(xT))], (1403 ^ _382164) ^ [_426176] : [aFunction0(_426176), 1406 ^ _382164 : [(1407 ^ _382164) ^ [_426353] : [aSubsetOf0(_426353, szDzozmdt0(_426176)), 1410 ^ _382164 : [(1411 ^ _382164) ^ [_426558] : [_426558 = sdtlcdtrc0(_426176, _426353), 1414 ^ _382164 : [(1426 ^ _382164) ^ [_427178] : [-(aElementOf0(_427178, _426558)), 1427 ^ _382164 : [(1428 ^ _382164) ^ [_427283] : [aElementOf0(_427283, _426353), sdtlpdtrp0(_426176, _427283) = _427178]]], (1417 ^ _382164) ^ [_426824] : [aElementOf0(_426824, _426558), 1421 ^ _382164 : [(1424 ^ _382164) ^ [] : [-(sdtlpdtrp0(_426176, 1420 ^ [_426176, _426353, _426558, _426824]) = _426824)], (1422 ^ _382164) ^ [] : [-(aElementOf0(1420 ^ [_426176, _426353, _426558, _426824], _426353))]]], (1415 ^ _382164) ^ [] : [-(aSet0(_426558))]]], (1436 ^ _382164) ^ [_427540] : [-(_427540 = sdtlcdtrc0(_426176, _426353)), aSet0(_427540), 1453 ^ _382164 : [(1458 ^ _382164) ^ [] : [aElementOf0(1441 ^ [_426176, _426353, _427540], _427540)], (1456 ^ _382164) ^ [] : [-(sdtlpdtrp0(_426176, 1452 ^ [_426176, _426353, _427540]) = 1441 ^ [_426176, _426353, _427540])], (1454 ^ _382164) ^ [] : [-(aElementOf0(1452 ^ [_426176, _426353, _427540], _426353))]], 1444 ^ _382164 : [(1447 ^ _382164) ^ [_427933] : [aElementOf0(_427933, _426353), sdtlpdtrp0(_426176, _427933) = 1441 ^ [_426176, _426353, _427540]], (1445 ^ _382164) ^ [] : [-(aElementOf0(1441 ^ [_426176, _426353, _427540], _427540))]]]]]]], (138 ^ _382164) ^ [_386629, _386631, _386633, _386635] : [-(sdtexdt0(_386635, _386631) = sdtexdt0(_386633, _386629)), _386635 = _386633, _386631 = _386629], (574 ^ _382164) ^ [_400637, _400639] : [aElement0(_400639), aSet0(_400637), -(aElementOf0(_400639, _400637)), -(sdtmndt0(sdtpldt0(_400637, _400639), _400639) = _400637)], (2566 ^ _382164) ^ [_471709] : [aElementOf0(_471709, xO), 2570 ^ _382164 : [(2573 ^ _382164) ^ [] : [-(sdtlpdtrp0(xe, 2569 ^ [_471709]) = _471709)], (2571 ^ _382164) ^ [] : [-(aElementOf0(2569 ^ [_471709], sdtlbdtrb0(xd, szDzizrdt0(xd))))]]], (691 ^ _382164) ^ [_404197, _404199] : [aElementOf0(_404199, szNzAzT0), aElementOf0(_404197, szNzAzT0), sdtlseqdt0(_404199, _404197), true___, -(true___)], (887 ^ _382164) ^ [_409715] : [aSet0(_409715), 890 ^ _382164 : [(891 ^ _382164) ^ [_409860] : [-(szszuzczcdt0(sbrdtbr0(sdtmndt0(_409715, _409860))) = sbrdtbr0(_409715)), isFinite0(_409715), aElementOf0(_409860, _409715)]]], (248 ^ _382164) ^ [_390511] : [aElement0(_390511), true___, -(true___)], (807 ^ _382164) ^ [_407473, _407475] : [aElementOf0(_407475, szNzAzT0), aElementOf0(_407473, szNzAzT0), iLess0(_407475, _407473), true___, -(true___)], (2526 ^ _382164) ^ [_470485] : [aElementOf0(_470485, sdtlbdtrb0(xd, szDzizrdt0(xd))), 2529 ^ _382164 : [(2532 ^ _382164) ^ [] : [-(sdtlpdtrp0(xd, _470485) = szDzizrdt0(xd))], (2530 ^ _382164) ^ [] : [-(aElementOf0(_470485, szDzozmdt0(xd)))]]], (1243 ^ _382164) ^ [_420952] : [aSet0(_420952), isCountable0(_420952), 1250 ^ _382164 : [(1251 ^ _382164) ^ [_421176] : [-(isCountable0(slbdtsldtrb0(_420952, _421176))), aElementOf0(_421176, szNzAzT0), -(_421176 = sz00)]]], (327 ^ _382164) ^ [_392709] : [_392709 = slcrc0, aSet0(_392709), isCountable0(_392709)], (132 ^ _382164) ^ [_386383, _386385] : [_386385 = _386383, -(slbdtrb0(_386385) = slbdtrb0(_386383))], (753 ^ _382164) ^ [_405993, _405995] : [aElementOf0(_405995, szNzAzT0), aElementOf0(_405993, szNzAzT0), -(_405995 = _405993), sdtlseqdt0(_405995, _405993), sdtlseqdt0(_405993, _405995)], (2546 ^ _382164) ^ [] : [-(aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd))))], (646 ^ _382164) ^ [] : [-(isCountable0(szNzAzT0))], (793 ^ _382164) ^ [_407078, _407080] : [aElementOf0(_407080, szNzAzT0), aElementOf0(_407078, szNzAzT0), -(sdtlseqdt0(_407080, _407078)), -(sdtlseqdt0(szszuzczcdt0(_407078), _407080))], (148 ^ _382164) ^ [_386988, _386990, _386992, _386994] : [-(sdtpldt0(_386994, _386990) = sdtpldt0(_386992, _386988)), _386994 = _386992, _386990 = _386988], (1787 ^ _382164) ^ [_441062] : [aElementOf0(_441062, szNzAzT0), isCountable0(sdtlpdtrp0(xN, _441062)), 1794 ^ _382164 : [(1795 ^ _382164) ^ [] : [aSet0(sdtlpdtrp0(xN, _441062)), 1799 ^ _382164 : [(1802 ^ _382164) ^ [] : [aElementOf0(1798 ^ [_441062], szNzAzT0)], (1800 ^ _382164) ^ [] : [-(aElementOf0(1798 ^ [_441062], sdtlpdtrp0(xN, _441062)))]]], (1804 ^ _382164) ^ [] : [aSubsetOf0(sdtlpdtrp0(xN, _441062), szNzAzT0)]], 1807 ^ _382164 : [(1850 ^ _382164) ^ [] : [-(aSubsetOf0(sdtlpdtrp0(xN, szszuzczcdt0(_441062)), sdtmndt0(sdtlpdtrp0(xN, _441062), szmzizndt0(sdtlpdtrp0(xN, _441062)))))], (1808 ^ _382164) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _441062)), sdtlpdtrp0(xN, _441062)))], (1810 ^ _382164) ^ [_441930] : [aElementOf0(_441930, sdtlpdtrp0(xN, _441062)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _441062)), _441930))], (1844 ^ _382164) ^ [_443082] : [aElementOf0(_443082, sdtlpdtrp0(xN, szszuzczcdt0(_441062))), -(aElementOf0(_443082, sdtmndt0(sdtlpdtrp0(xN, _441062), szmzizndt0(sdtlpdtrp0(xN, _441062)))))], (1852 ^ _382164) ^ [] : [-(isCountable0(sdtlpdtrp0(xN, szszuzczcdt0(_441062))))], (1828 ^ _382164) ^ [_442597] : [-(aElementOf0(_442597, sdtmndt0(sdtlpdtrp0(xN, _441062), szmzizndt0(sdtlpdtrp0(xN, _441062))))), aElement0(_442597), aElementOf0(_442597, sdtlpdtrp0(xN, _441062)), -(_442597 = szmzizndt0(sdtlpdtrp0(xN, _441062)))], (1842 ^ _382164) ^ [] : [-(aSet0(sdtlpdtrp0(xN, szszuzczcdt0(_441062))))], (1818 ^ _382164) ^ [_442247] : [aElementOf0(_442247, sdtmndt0(sdtlpdtrp0(xN, _441062), szmzizndt0(sdtlpdtrp0(xN, _441062)))), 1821 ^ _382164 : [(1826 ^ _382164) ^ [] : [_442247 = szmzizndt0(sdtlpdtrp0(xN, _441062))], (1824 ^ _382164) ^ [] : [-(aElementOf0(_442247, sdtlpdtrp0(xN, _441062)))], (1822 ^ _382164) ^ [] : [-(aElement0(_442247))]]], (1816 ^ _382164) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _441062), szmzizndt0(sdtlpdtrp0(xN, _441062)))))]]], (853 ^ _382164) ^ [_408738] : [aSet0(_408738), 856 ^ _382164 : [(863 ^ _382164) ^ [] : [_408738 = slcrc0, -(sbrdtbr0(_408738) = sz00)], (857 ^ _382164) ^ [] : [sbrdtbr0(_408738) = sz00, -(_408738 = slcrc0)]]], (317 ^ _382164) ^ [_392439] : [isFinite0(_392439), aSet0(_392439), isCountable0(_392439)], (10 ^ _382164) ^ [_382599, _382601, _382603] : [-(_382603 = _382599), _382603 = _382601, _382601 = _382599], (2615 ^ _382164) ^ [] : [-(aElementOf0(xx, xO))], (1631 ^ _382164) ^ [_434389] : [aElementOf0(_434389, sdtlcdtrc0(xc, szDzozmdt0(xc))), -(aElementOf0(_434389, xT))], (1158 ^ _382164) ^ [_418151, _418153] : [aSet0(_418153), aElementOf0(_418151, szNzAzT0), 1165 ^ _382164 : [(1166 ^ _382164) ^ [_418431] : [_418431 = slbdtsldtrb0(_418153, _418151), 1169 ^ _382164 : [(1180 ^ _382164) ^ [_418954] : [-(aElementOf0(_418954, _418431)), aSubsetOf0(_418954, _418153), sbrdtbr0(_418954) = _418151], (1172 ^ _382164) ^ [_418691] : [aElementOf0(_418691, _418431), 1175 ^ _382164 : [(1178 ^ _382164) ^ [] : [-(sbrdtbr0(_418691) = _418151)], (1176 ^ _382164) ^ [] : [-(aSubsetOf0(_418691, _418153))]]], (1170 ^ _382164) ^ [] : [-(aSet0(_418431))]]], (1190 ^ _382164) ^ [_419244] : [-(_419244 = slbdtsldtrb0(_418153, _418151)), aSet0(_419244), 1206 ^ _382164 : [(1211 ^ _382164) ^ [] : [aElementOf0(1195 ^ [_418151, _418153, _419244], _419244)], (1209 ^ _382164) ^ [] : [-(sbrdtbr0(1195 ^ [_418151, _418153, _419244]) = _418151)], (1207 ^ _382164) ^ [] : [-(aSubsetOf0(1195 ^ [_418151, _418153, _419244], _418153))]], 1198 ^ _382164 : [(1201 ^ _382164) ^ [] : [aSubsetOf0(1195 ^ [_418151, _418153, _419244], _418153), sbrdtbr0(1195 ^ [_418151, _418153, _419244]) = _418151], (1199 ^ _382164) ^ [] : [-(aElementOf0(1195 ^ [_418151, _418153, _419244], _419244))]]]]], (1462 ^ _382164) ^ [_428544] : [aFunction0(_428544), 1465 ^ _382164 : [(1466 ^ _382164) ^ [_428685] : [aElementOf0(_428685, szDzozmdt0(_428544)), -(aElementOf0(sdtlpdtrp0(_428544, _428685), sdtlcdtrc0(_428544, szDzozmdt0(_428544))))]]], (54 ^ _382164) ^ [_383974, _383976, _383978, _383980] : [-(sdtlseqdt0(_383978, _383974)), sdtlseqdt0(_383980, _383976), _383980 = _383978, _383976 = _383974], (869 ^ _382164) ^ [_409172] : [aSet0(_409172), isFinite0(_409172), 876 ^ _382164 : [(877 ^ _382164) ^ [_409402] : [aElement0(_409402), -(aElementOf0(_409402, _409172)), -(sbrdtbr0(sdtpldt0(_409172, _409402)) = szszuzczcdt0(sbrdtbr0(_409172)))]]], (1032 ^ _382164) ^ [_414218] : [aElementOf0(_414218, szNzAzT0), 1035 ^ _382164 : [(1036 ^ _382164) ^ [_414406] : [_414406 = slbdtrb0(_414218), 1039 ^ _382164 : [(1050 ^ _382164) ^ [_414909] : [-(aElementOf0(_414909, _414406)), aElementOf0(_414909, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_414909), _414218)], (1042 ^ _382164) ^ [_414656] : [aElementOf0(_414656, _414406), 1045 ^ _382164 : [(1048 ^ _382164) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(_414656), _414218))], (1046 ^ _382164) ^ [] : [-(aElementOf0(_414656, szNzAzT0))]]], (1040 ^ _382164) ^ [] : [-(aSet0(_414406))]]], (1060 ^ _382164) ^ [_415187] : [-(_415187 = slbdtrb0(_414218)), aSet0(_415187), 1076 ^ _382164 : [(1081 ^ _382164) ^ [] : [aElementOf0(1065 ^ [_414218, _415187], _415187)], (1079 ^ _382164) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(1065 ^ [_414218, _415187]), _414218))], (1077 ^ _382164) ^ [] : [-(aElementOf0(1065 ^ [_414218, _415187], szNzAzT0))]], 1068 ^ _382164 : [(1071 ^ _382164) ^ [] : [aElementOf0(1065 ^ [_414218, _415187], szNzAzT0), sdtlseqdt0(szszuzczcdt0(1065 ^ [_414218, _415187]), _414218)], (1069 ^ _382164) ^ [] : [-(aElementOf0(1065 ^ [_414218, _415187], _415187))]]]]], (588 ^ _382164) ^ [_401024] : [aElement0(_401024), 591 ^ _382164 : [(592 ^ _382164) ^ [_401161] : [-(isCountable0(sdtpldt0(_401161, _401024))), aSet0(_401161), isCountable0(_401161)]]], (290 ^ _382164) ^ [_391716] : [-(_391716 = slcrc0), aSet0(_391716), -(aElementOf0(295 ^ [_391716], _391716))], (20 ^ _382164) ^ [_382912, _382914] : [-(isFinite0(_382912)), _382914 = _382912, isFinite0(_382914)], (2556 ^ _382164) ^ [_471397] : [-(aElementOf0(_471397, sdtlbdtrb0(xd, szDzizrdt0(xd)))), aElementOf0(_471397, szDzozmdt0(xd)), sdtlpdtrp0(xd, _471397) = szDzizrdt0(xd)], (2611 ^ _382164) ^ [] : [-(aElementOf0(2609 ^ [], sdtlbdtrb0(xd, szDzizrdt0(xd))))]], input).
% 54.61/53.07  ncf('1',plain,[-(aElementOf0(2620 ^ [], sdtlpdtrp0(xN, xi)))],start(2622 ^ 0)).
% 54.61/53.07  ncf('1.1',plain,[aElementOf0(2620 ^ [], sdtlpdtrp0(xN, xi)), 1882 : -(aElementOf0(2620 ^ [], sdtlpdtrp0(xN, sz00))), 1882 : aElementOf0(xi, szNzAzT0), 1882 : aElementOf0(sz00, szNzAzT0), 1882 : sdtlseqdt0(sz00, xi)],extension(1870 ^ 1,bind([[_444070, _444072, _444419], [sz00, xi, 2620 ^ []]]))).
% 54.61/53.07  ncf('1.1.1',plain,[aElementOf0(2620 ^ [], sdtlpdtrp0(xN, sz00)), -(aElementOf0(2620 ^ [], xS)), 2620 ^ [] = 2620 ^ [], sdtlpdtrp0(xN, sz00) = xS],extension(98 ^ 4,bind([[_385303, _385305, _385307, _385309], [xS, sdtlpdtrp0(xN, sz00), 2620 ^ [], 2620 ^ []]]))).
% 54.61/53.07  ncf('1.1.1.1',plain,[aElementOf0(2620 ^ [], xS)],extension(2624 ^ 5)).
% 54.61/53.07  ncf('1.1.1.2',plain,[-(2620 ^ [] = 2620 ^ [])],extension(2 ^ 5,bind([[_382288], [2620 ^ []]]))).
% 54.61/53.07  ncf('1.1.1.3',plain,[-(sdtlpdtrp0(xN, sz00) = xS)],extension(1785 ^ 5)).
% 54.61/53.07  ncf('1.1.2',plain,[-(aElementOf0(xi, szNzAzT0))],extension(2617 ^ 2)).
% 54.61/53.07  ncf('1.1.3',plain,[-(aElementOf0(sz00, szNzAzT0))],extension(648 ^ 2)).
% 54.61/53.07  ncf('1.1.4',plain,[-(sdtlseqdt0(sz00, xi)), aElementOf0(xi, szNzAzT0)],extension(709 ^ 2,bind([[_404647], [xi]]))).
% 54.61/53.07  ncf('1.1.4.1',plain,[-(aElementOf0(xi, szNzAzT0))],lemmata('[1].x')).
% 54.61/53.07  %-----------------------------------------------------
% 54.61/53.07  End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------