↑ Up

nanoCoP---2.0.THM-Prf.s

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

% Computer : n001.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Fri May 19 11:45:08 EDT 2023

% Result   : Theorem 48.27s 46.95s
% Output   : Proof 48.27s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : NUM605+3 : TPTP v8.1.2. Released v4.0.0.
% 0.07/0.13  % Command  : nanocop.sh %s %d
% 0.13/0.33  % Computer : n001.cluster.edu
% 0.13/0.33  % Model    : x86_64 x86_64
% 0.13/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33  % Memory   : 8042.1875MB
% 0.13/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33  % CPULimit : 300
% 0.13/0.33  % WCLimit  : 300
% 0.13/0.33  % DateTime : Thu May 18 17:02:35 EDT 2023
% 0.13/0.34  % CPUTime  : 
% 48.27/46.95  
% 48.27/46.95  /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 48.27/46.95  Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 48.27/46.95  %-----------------------------------------------------
% 48.27/46.95  ncf(matrix, plain, [(2634 ^ _476835) ^ [] : [-(xQ = slcrc0)], (2632 ^ _476835) ^ [_476898] : [aElementOf0(_476898, xQ)], !, (1775 ^ _384323) ^ [] : [xK = sz00], (1639 ^ _384323) ^ [_436787] : [aElementOf0(_436787, szNzAzT0), 1642 ^ _384323 : [(1643 ^ _384323) ^ [_437250] : [isCountable0(_437250), 1646 ^ _384323 : [(1647 ^ _384323) ^ [] : [aSet0(_437250), 1651 ^ _384323 : [(1654 ^ _384323) ^ [] : [aElementOf0(1650 ^ [_436787, _437250], szNzAzT0)], (1652 ^ _384323) ^ [] : [-(aElementOf0(1650 ^ [_436787, _437250], _437250))]]], (1656 ^ _384323) ^ [] : [aSubsetOf0(_437250, szNzAzT0)]], 1659 ^ _384323 : [(1660 ^ _384323) ^ [_438074] : [iLess0(_436787, xK), 1736 ^ _384323 : [(1740 ^ _384323) ^ [] : [-(aSet0(1738 ^ [_436787, _437250, _438074]))], (1737 ^ _384323) ^ [] : [-(aElementOf0(1735 ^ [_436787, _437250, _438074], xT))], (1752 ^ _384323) ^ [_441993] : [-(sdtlpdtrp0(_438074, _441993) = 1735 ^ [_436787, _437250, _438074]), 1753 ^ _384323 : [(1754 ^ _384323) ^ [] : [sbrdtbr0(_441993) = _436787, 1755 ^ _384323 : [(1756 ^ _384323) ^ [] : [aSet0(_441993), 1760 ^ _384323 : [(1763 ^ _384323) ^ [] : [aElementOf0(1759 ^ [_436787, _437250, _438074, _441993], 1738 ^ [_436787, _437250, _438074])], (1761 ^ _384323) ^ [] : [-(aElementOf0(1759 ^ [_436787, _437250, _438074, _441993], _441993))]]], (1765 ^ _384323) ^ [] : [aSubsetOf0(_441993, 1738 ^ [_436787, _437250, _438074])]]], (1769 ^ _384323) ^ [] : [aElementOf0(_441993, slbdtsldtrb0(1738 ^ [_436787, _437250, _438074], _436787))]]], (1748 ^ _384323) ^ [] : [-(aSubsetOf0(1738 ^ [_436787, _437250, _438074], _437250))], (1750 ^ _384323) ^ [] : [-(isCountable0(1738 ^ [_436787, _437250, _438074]))], (1742 ^ _384323) ^ [_441628] : [aElementOf0(_441628, 1738 ^ [_436787, _437250, _438074]), -(aElementOf0(_441628, _437250))]], aFunction0(_438074), 1668 ^ _384323 : [(1669 ^ _384323) ^ [] : [1687 ^ _384323 : [(1700 ^ _384323) ^ [] : [aElementOf0(1667 ^ [_436787, _437250, _438074], szDzozmdt0(_438074))], (1696 ^ _384323) ^ [] : [-(aSubsetOf0(1667 ^ [_436787, _437250, _438074], _437250))], (1690 ^ _384323) ^ [_439436] : [aElementOf0(_439436, 1667 ^ [_436787, _437250, _438074]), -(aElementOf0(_439436, _437250))], (1698 ^ _384323) ^ [] : [-(sbrdtbr0(1667 ^ [_436787, _437250, _438074]) = _436787)], (1688 ^ _384323) ^ [] : [-(aSet0(1667 ^ [_436787, _437250, _438074]))]], 1670 ^ _384323 : [(1673 ^ _384323) ^ [] : [sbrdtbr0(1667 ^ [_436787, _437250, _438074]) = _436787, 1674 ^ _384323 : [(1675 ^ _384323) ^ [] : [aSet0(1667 ^ [_436787, _437250, _438074]), 1679 ^ _384323 : [(1682 ^ _384323) ^ [] : [aElementOf0(1678 ^ [_436787, _437250, _438074], _437250)], (1680 ^ _384323) ^ [] : [-(aElementOf0(1678 ^ [_436787, _437250, _438074], 1667 ^ [_436787, _437250, _438074]))]]], (1684 ^ _384323) ^ [] : [aSubsetOf0(1667 ^ [_436787, _437250, _438074], _437250)]]], (1671 ^ _384323) ^ [] : [-(aElementOf0(1667 ^ [_436787, _437250, _438074], szDzozmdt0(_438074)))]]], (1702 ^ _384323) ^ [] : [szDzozmdt0(_438074) = slbdtsldtrb0(_437250, _436787)]], 1703 ^ _384323 : [(1728 ^ _384323) ^ [] : [aElementOf0(1724 ^ [_436787, _437250, _438074], xT)], (1726 ^ _384323) ^ [] : [-(aElementOf0(1724 ^ [_436787, _437250, _438074], sdtlcdtrc0(_438074, szDzozmdt0(_438074))))], (1715 ^ _384323) ^ [_440403] : [-(aElementOf0(_440403, sdtlcdtrc0(_438074, szDzozmdt0(_438074)))), 1716 ^ _384323 : [(1717 ^ _384323) ^ [_440515] : [aElementOf0(_440515, szDzozmdt0(_438074)), sdtlpdtrp0(_438074, _440515) = _440403]]], (1704 ^ _384323) ^ [] : [-(aSet0(sdtlcdtrc0(_438074, szDzozmdt0(_438074))))], (1706 ^ _384323) ^ [_440033] : [aElementOf0(_440033, sdtlcdtrc0(_438074, szDzozmdt0(_438074))), 1710 ^ _384323 : [(1713 ^ _384323) ^ [] : [-(sdtlpdtrp0(_438074, 1709 ^ [_436787, _437250, _438074, _440033]) = _440033)], (1711 ^ _384323) ^ [] : [-(aElementOf0(1709 ^ [_436787, _437250, _438074, _440033], szDzozmdt0(_438074)))]]], (1730 ^ _384323) ^ [] : [aSubsetOf0(sdtlcdtrc0(_438074, szDzozmdt0(_438074)), xT)]]]]]]], (148 ^ _384323) ^ [_389147, _389149, _389151, _389153] : [-(sdtpldt0(_389153, _389149) = sdtpldt0(_389151, _389147)), _389153 = _389151, _389149 = _389147], (2534 ^ _384323) ^ [_472879] : [-(aElementOf0(_472879, sdtlbdtrb0(xd, szDzizrdt0(xd)))), aElementOf0(_472879, szDzozmdt0(xd)), sdtlpdtrp0(xd, _472879) = szDzizrdt0(xd)], (650 ^ _384323) ^ [_405060] : [aElementOf0(_405060, szNzAzT0), 653 ^ _384323 : [(656 ^ _384323) ^ [] : [szszuzczcdt0(_405060) = sz00], (654 ^ _384323) ^ [] : [-(aElementOf0(szszuzczcdt0(_405060), szNzAzT0))]]], (1085 ^ _384323) ^ [_418149] : [aElementOf0(_418149, szNzAzT0), -(isFinite0(slbdtrb0(_418149)))], (2493 ^ _384323) ^ [] : [-(aSet0(sdtlcdtrc0(xd, szDzozmdt0(xd))))], (1403 ^ _384323) ^ [_428335] : [aFunction0(_428335), 1406 ^ _384323 : [(1407 ^ _384323) ^ [_428512] : [aSubsetOf0(_428512, szDzozmdt0(_428335)), 1410 ^ _384323 : [(1411 ^ _384323) ^ [_428717] : [_428717 = sdtlcdtrc0(_428335, _428512), 1414 ^ _384323 : [(1426 ^ _384323) ^ [_429337] : [-(aElementOf0(_429337, _428717)), 1427 ^ _384323 : [(1428 ^ _384323) ^ [_429442] : [aElementOf0(_429442, _428512), sdtlpdtrp0(_428335, _429442) = _429337]]], (1417 ^ _384323) ^ [_428983] : [aElementOf0(_428983, _428717), 1421 ^ _384323 : [(1424 ^ _384323) ^ [] : [-(sdtlpdtrp0(_428335, 1420 ^ [_428335, _428512, _428717, _428983]) = _428983)], (1422 ^ _384323) ^ [] : [-(aElementOf0(1420 ^ [_428335, _428512, _428717, _428983], _428512))]]], (1415 ^ _384323) ^ [] : [-(aSet0(_428717))]]], (1436 ^ _384323) ^ [_429699] : [-(_429699 = sdtlcdtrc0(_428335, _428512)), aSet0(_429699), 1453 ^ _384323 : [(1458 ^ _384323) ^ [] : [aElementOf0(1441 ^ [_428335, _428512, _429699], _429699)], (1456 ^ _384323) ^ [] : [-(sdtlpdtrp0(_428335, 1452 ^ [_428335, _428512, _429699]) = 1441 ^ [_428335, _428512, _429699])], (1454 ^ _384323) ^ [] : [-(aElementOf0(1452 ^ [_428335, _428512, _429699], _428512))]], 1444 ^ _384323 : [(1447 ^ _384323) ^ [_430092] : [aElementOf0(_430092, _428512), sdtlpdtrp0(_428335, _430092) = 1441 ^ [_428335, _428512, _429699]], (1445 ^ _384323) ^ [] : [-(aElementOf0(1441 ^ [_428335, _428512, _429699], _429699))]]]]]]], (1287 ^ _384323) ^ [_424442, _424444] : [aSet0(_424444), aElementOf0(_424442, szNzAzT0), 1294 ^ _384323 : [(1295 ^ _384323) ^ [_424693] : [1303 ^ _384323 : [(1308 ^ _384323) ^ [] : [-(aSubsetOf0(_424693, slbdtsldtrb0(1302 ^ [_424442, _424444, _424693], _424442)))], (1306 ^ _384323) ^ [] : [-(isFinite0(1302 ^ [_424442, _424444, _424693]))], (1304 ^ _384323) ^ [] : [-(aSubsetOf0(1302 ^ [_424442, _424444, _424693], _424444))]], aSubsetOf0(_424693, slbdtsldtrb0(_424444, _424442)), isFinite0(_424693)]]], (2225 ^ _384323) ^ [_460337] : [aElementOf0(_460337, szNzAzT0), 2228 ^ _384323 : [(2229 ^ _384323) ^ [_460836] : [isCountable0(_460836), 2232 ^ _384323 : [(2276 ^ _384323) ^ [] : [aSubsetOf0(_460836, sdtmndt0(sdtlpdtrp0(xN, _460337), szmzizndt0(sdtlpdtrp0(xN, _460337))))], (2243 ^ _384323) ^ [_461742] : [aElementOf0(_461742, sdtmndt0(sdtlpdtrp0(xN, _460337), szmzizndt0(sdtlpdtrp0(xN, _460337)))), 2246 ^ _384323 : [(2251 ^ _384323) ^ [] : [_461742 = szmzizndt0(sdtlpdtrp0(xN, _460337))], (2249 ^ _384323) ^ [] : [-(aElementOf0(_461742, sdtlpdtrp0(xN, _460337)))], (2247 ^ _384323) ^ [] : [-(aElement0(_461742))]]], (2253 ^ _384323) ^ [_462104] : [-(aElementOf0(_462104, sdtmndt0(sdtlpdtrp0(xN, _460337), szmzizndt0(sdtlpdtrp0(xN, _460337))))), aElement0(_462104), aElementOf0(_462104, sdtlpdtrp0(xN, _460337)), -(_462104 = szmzizndt0(sdtlpdtrp0(xN, _460337)))], (2267 ^ _384323) ^ [] : [aSet0(_460836), 2271 ^ _384323 : [(2274 ^ _384323) ^ [] : [aElementOf0(2270 ^ [_460337, _460836], sdtmndt0(sdtlpdtrp0(xN, _460337), szmzizndt0(sdtlpdtrp0(xN, _460337))))], (2272 ^ _384323) ^ [] : [-(aElementOf0(2270 ^ [_460337, _460836], _460836))]]], (2233 ^ _384323) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _460337)), sdtlpdtrp0(xN, _460337)))], (2235 ^ _384323) ^ [_461413] : [aElementOf0(_461413, sdtlpdtrp0(xN, _460337)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _460337)), _461413))], (2241 ^ _384323) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _460337), szmzizndt0(sdtlpdtrp0(xN, _460337)))))]], 2279 ^ _384323 : [(2280 ^ _384323) ^ [_462937] : [aSet0(_462937), 2285 ^ _384323 : [(2286 ^ _384323) ^ [] : [2288 ^ _384323 : [(2293 ^ _384323) ^ [] : [aSubsetOf0(_462937, _460836)], (2291 ^ _384323) ^ [] : [aElementOf0(2287 ^ [_460337, _460836, _462937], _460836)], (2289 ^ _384323) ^ [] : [-(aElementOf0(2287 ^ [_460337, _460836, _462937], _462937))]], sbrdtbr0(_462937) = xk], (2297 ^ _384323) ^ [] : [aElementOf0(_462937, slbdtsldtrb0(_460836, xk))]], 2298 ^ _384323 : [(2307 ^ _384323) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _460337), szmzizndt0(sdtlpdtrp0(xN, _460337)))))], (2333 ^ _384323) ^ [_464992] : [aElementOf0(_464992, _462937), -(aElementOf0(_464992, sdtmndt0(sdtlpdtrp0(xN, _460337), szmzizndt0(sdtlpdtrp0(xN, _460337)))))], (2299 ^ _384323) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _460337)), sdtlpdtrp0(xN, _460337)))], (2309 ^ _384323) ^ [_464169] : [aElementOf0(_464169, sdtmndt0(sdtlpdtrp0(xN, _460337), szmzizndt0(sdtlpdtrp0(xN, _460337)))), 2312 ^ _384323 : [(2317 ^ _384323) ^ [] : [_464169 = szmzizndt0(sdtlpdtrp0(xN, _460337))], (2315 ^ _384323) ^ [] : [-(aElementOf0(_464169, sdtlpdtrp0(xN, _460337)))], (2313 ^ _384323) ^ [] : [-(aElement0(_464169))]]], (2339 ^ _384323) ^ [] : [-(aSubsetOf0(_462937, sdtmndt0(sdtlpdtrp0(xN, _460337), szmzizndt0(sdtlpdtrp0(xN, _460337)))))], (2341 ^ _384323) ^ [] : [-(aElementOf0(_462937, slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _460337), szmzizndt0(sdtlpdtrp0(xN, _460337))), xk)))], (2319 ^ _384323) ^ [_464543] : [-(aElementOf0(_464543, sdtmndt0(sdtlpdtrp0(xN, _460337), szmzizndt0(sdtlpdtrp0(xN, _460337))))), aElement0(_464543), aElementOf0(_464543, sdtlpdtrp0(xN, _460337)), -(_464543 = szmzizndt0(sdtlpdtrp0(xN, _460337)))], (2301 ^ _384323) ^ [_463832] : [aElementOf0(_463832, sdtlpdtrp0(xN, _460337)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _460337)), _463832))]]]]]]], (1557 ^ _384323) ^ [] : [-(aElementOf0(xK, szNzAzT0))], (1091 ^ _384323) ^ [] : [-(slbdtrb0(sz00) = slcrc0)], (1472 ^ _384323) ^ [_431067] : [aFunction0(_431067), 1475 ^ _384323 : [(1476 ^ _384323) ^ [_431244] : [aSubsetOf0(_431244, szDzozmdt0(_431067)), 1479 ^ _384323 : [(1494 ^ _384323) ^ [_431957] : [-(_431957 = sdtexdt0(_431067, _431244)), aFunction0(_431957), szDzozmdt0(_431957) = _431244, 1504 ^ _384323 : [(1507 ^ _384323) ^ [] : [sdtlpdtrp0(_431957, 1503 ^ [_431067, _431244, _431957]) = sdtlpdtrp0(_431067, 1503 ^ [_431067, _431244, _431957])], (1505 ^ _384323) ^ [] : [-(aElementOf0(1503 ^ [_431067, _431244, _431957], _431244))]]], (1480 ^ _384323) ^ [_431449] : [_431449 = sdtexdt0(_431067, _431244), 1483 ^ _384323 : [(1488 ^ _384323) ^ [_431756] : [aElementOf0(_431756, _431244), -(sdtlpdtrp0(_431449, _431756) = sdtlpdtrp0(_431067, _431756))], (1486 ^ _384323) ^ [] : [-(szDzozmdt0(_431449) = _431244)], (1484 ^ _384323) ^ [] : [-(aFunction0(_431449))]]]]]]], (1139 ^ _384323) ^ [_419684] : [1147 ^ _384323 : [(1150 ^ _384323) ^ [] : [-(aSubsetOf0(_419684, slbdtrb0(1146 ^ [_419684])))], (1148 ^ _384323) ^ [] : [-(aElementOf0(1146 ^ [_419684], szNzAzT0))]], aSubsetOf0(_419684, szNzAzT0), isFinite0(_419684)], (301 ^ _384323) ^ [] : [-(isFinite0(slcrc0))], (1336 ^ _384323) ^ [_426060, _426062] : [aFunction0(_426062), aElement0(_426060), 1343 ^ _384323 : [(1344 ^ _384323) ^ [_426341] : [_426341 = sdtlbdtrb0(_426062, _426060), 1347 ^ _384323 : [(1358 ^ _384323) ^ [_426873] : [-(aElementOf0(_426873, _426341)), aElementOf0(_426873, szDzozmdt0(_426062)), sdtlpdtrp0(_426062, _426873) = _426060], (1350 ^ _384323) ^ [_426604] : [aElementOf0(_426604, _426341), 1353 ^ _384323 : [(1356 ^ _384323) ^ [] : [-(sdtlpdtrp0(_426062, _426604) = _426060)], (1354 ^ _384323) ^ [] : [-(aElementOf0(_426604, szDzozmdt0(_426062)))]]], (1348 ^ _384323) ^ [] : [-(aSet0(_426341))]]], (1368 ^ _384323) ^ [_427169] : [-(_427169 = sdtlbdtrb0(_426062, _426060)), aSet0(_427169), 1384 ^ _384323 : [(1389 ^ _384323) ^ [] : [aElementOf0(1373 ^ [_426060, _426062, _427169], _427169)], (1387 ^ _384323) ^ [] : [-(sdtlpdtrp0(_426062, 1373 ^ [_426060, _426062, _427169]) = _426060)], (1385 ^ _384323) ^ [] : [-(aElementOf0(1373 ^ [_426060, _426062, _427169], szDzozmdt0(_426062)))]], 1376 ^ _384323 : [(1379 ^ _384323) ^ [] : [aElementOf0(1373 ^ [_426060, _426062, _427169], szDzozmdt0(_426062)), sdtlpdtrp0(_426062, 1373 ^ [_426060, _426062, _427169]) = _426060], (1377 ^ _384323) ^ [] : [-(aElementOf0(1373 ^ [_426060, _426062, _427169], _427169))]]]]], (1243 ^ _384323) ^ [_423111] : [aSet0(_423111), isCountable0(_423111), 1250 ^ _384323 : [(1251 ^ _384323) ^ [_423335] : [-(isCountable0(slbdtsldtrb0(_423111, _423335))), aElementOf0(_423335, szNzAzT0), -(_423335 = sz00)]]], (1553 ^ _384323) ^ [] : [-(aSet0(xT))], (2626 ^ _384323) ^ [] : [-(aSubsetOf0(xQ, xO))], (1119 ^ _384323) ^ [_419135, _419137] : [aElementOf0(_419137, szNzAzT0), aElementOf0(_419135, szNzAzT0), 1126 ^ _384323 : [(1133 ^ _384323) ^ [] : [aSubsetOf0(slbdtrb0(_419137), slbdtrb0(_419135)), -(sdtlseqdt0(_419137, _419135))], (1127 ^ _384323) ^ [] : [sdtlseqdt0(_419137, _419135), -(aSubsetOf0(slbdtrb0(_419137), slbdtrb0(_419135)))]]], (915 ^ _384323) ^ [_412779, _412781] : [aSet0(_412781), aElementOf0(_412779, szNzAzT0), 931 ^ _384323 : [(934 ^ _384323) ^ [] : [-(sbrdtbr0(930 ^ [_412779, _412781]) = _412779)], (932 ^ _384323) ^ [] : [-(aSubsetOf0(930 ^ [_412779, _412781], _412781))]], isFinite0(_412781), sdtlseqdt0(_412779, sbrdtbr0(_412781))], (741 ^ _384323) ^ [_407754] : [aElementOf0(_407754, szNzAzT0), -(sdtlseqdt0(_407754, szszuzczcdt0(_407754)))], (2630 ^ _384323) ^ [] : [-(aElementOf0(xQ, slbdtsldtrb0(xO, xK)))], (602 ^ _384323) ^ [_403612] : [aElement0(_403612), 605 ^ _384323 : [(606 ^ _384323) ^ [_403749] : [-(isCountable0(sdtmndt0(_403749, _403612))), aSet0(_403749), isCountable0(_403749)]]], (380 ^ _384323) ^ [_396557] : [aSet0(_396557), -(aSubsetOf0(_396557, _396557))], (404 ^ _384323) ^ [_397248, _397250, _397252] : [aSet0(_397252), aSet0(_397250), aSet0(_397248), -(aSubsetOf0(_397252, _397248)), aSubsetOf0(_397252, _397250), aSubsetOf0(_397250, _397248)], (564 ^ _384323) ^ [_402430] : [aSet0(_402430), 567 ^ _384323 : [(568 ^ _384323) ^ [_402567] : [aElementOf0(_402567, _402430), -(sdtpldt0(sdtmndt0(_402430, _402567), _402567) = _402430)]]], (2522 ^ _384323) ^ [] : [-(aElementOf0(szDzizrdt0(xd), xT))], (1571 ^ _384323) ^ [] : [-(aFunction0(xc))], (771 ^ _384323) ^ [_408645, _408647, _408649] : [aElementOf0(_408649, szNzAzT0), aElementOf0(_408647, szNzAzT0), aElementOf0(_408645, szNzAzT0), -(sdtlseqdt0(_408649, _408645)), sdtlseqdt0(_408649, _408647), sdtlseqdt0(_408647, _408645)], (112 ^ _384323) ^ [_387886, _387888, _387890, _387892] : [-(aElementOf0(_387890, _387886)), aElementOf0(_387892, _387888), _387892 = _387890, _387888 = _387886], (2589 ^ _384323) ^ [] : [-(isCountable0(xO))], (2192 ^ _384323) ^ [_458928] : [aElementOf0(_458928, szNzAzT0), 2195 ^ _384323 : [(2196 ^ _384323) ^ [] : [-(aSet0(sdtlcdtrc0(sdtlpdtrp0(xC, _458928), szDzozmdt0(sdtlpdtrp0(xC, _458928)))))], (2217 ^ _384323) ^ [_460049] : [aElementOf0(_460049, sdtlcdtrc0(sdtlpdtrp0(xC, _458928), szDzozmdt0(sdtlpdtrp0(xC, _458928)))), -(aElementOf0(_460049, xT))], (2207 ^ _384323) ^ [_459642] : [-(aElementOf0(_459642, sdtlcdtrc0(sdtlpdtrp0(xC, _458928), szDzozmdt0(sdtlpdtrp0(xC, _458928))))), 2208 ^ _384323 : [(2209 ^ _384323) ^ [_459758] : [aElementOf0(_459758, szDzozmdt0(sdtlpdtrp0(xC, _458928))), sdtlpdtrp0(sdtlpdtrp0(xC, _458928), _459758) = _459642]]], (2198 ^ _384323) ^ [_459278] : [aElementOf0(_459278, sdtlcdtrc0(sdtlpdtrp0(xC, _458928), szDzozmdt0(sdtlpdtrp0(xC, _458928)))), 2202 ^ _384323 : [(2205 ^ _384323) ^ [] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _458928), 2201 ^ [_458928, _459278]) = _459278)], (2203 ^ _384323) ^ [] : [-(aElementOf0(2201 ^ [_458928, _459278], szDzozmdt0(sdtlpdtrp0(xC, _458928))))]]], (2223 ^ _384323) ^ [] : [-(aSubsetOf0(sdtlcdtrc0(sdtlpdtrp0(xC, _458928), szDzozmdt0(sdtlpdtrp0(xC, _458928))), xT))]]], (495 ^ _384323) ^ [_400132, _400134] : [aSet0(_400134), aElement0(_400132), 502 ^ _384323 : [(503 ^ _384323) ^ [_400415] : [_400415 = sdtmndt0(_400134, _400132), 506 ^ _384323 : [(519 ^ _384323) ^ [_401016] : [-(aElementOf0(_401016, _400415)), aElement0(_401016), aElementOf0(_401016, _400134), -(_401016 = _400132)], (509 ^ _384323) ^ [_400680] : [aElementOf0(_400680, _400415), 512 ^ _384323 : [(517 ^ _384323) ^ [] : [_400680 = _400132], (515 ^ _384323) ^ [] : [-(aElementOf0(_400680, _400134))], (513 ^ _384323) ^ [] : [-(aElement0(_400680))]]], (507 ^ _384323) ^ [] : [-(aSet0(_400415))]]], (533 ^ _384323) ^ [_401400] : [-(_401400 = sdtmndt0(_400134, _400132)), aSet0(_401400), 553 ^ _384323 : [(556 ^ _384323) ^ [] : [-(aElementOf0(538 ^ [_400132, _400134, _401400], _400134))], (558 ^ _384323) ^ [] : [538 ^ [_400132, _400134, _401400] = _400132], (560 ^ _384323) ^ [] : [aElementOf0(538 ^ [_400132, _400134, _401400], _401400)], (554 ^ _384323) ^ [] : [-(aElement0(538 ^ [_400132, _400134, _401400]))]], 541 ^ _384323 : [(544 ^ _384323) ^ [] : [aElement0(538 ^ [_400132, _400134, _401400]), aElementOf0(538 ^ [_400132, _400134, _401400], _400134), -(538 ^ [_400132, _400134, _401400] = _400132)], (542 ^ _384323) ^ [] : [-(aElementOf0(538 ^ [_400132, _400134, _401400], _401400))]]]]], (174 ^ _384323) ^ [_390055, _390057] : [_390057 = _390055, -(szszuzczcdt0(_390057) = szszuzczcdt0(_390055))], (837 ^ _384323) ^ [_410466] : [aSet0(_410466), 840 ^ _384323 : [(847 ^ _384323) ^ [] : [isFinite0(_410466), -(aElementOf0(sbrdtbr0(_410466), szNzAzT0))], (841 ^ _384323) ^ [] : [aElementOf0(sbrdtbr0(_410466), szNzAzT0), -(isFinite0(_410466))]]], (648 ^ _384323) ^ [] : [-(aElementOf0(sz00, szNzAzT0))], (2343 ^ _384323) ^ [_465406] : [aElementOf0(_465406, szNzAzT0), 2347 ^ _384323 : [(2371 ^ _384323) ^ [_467115] : [-(aElementOf0(_467115, sdtmndt0(sdtlpdtrp0(xN, _465406), szmzizndt0(sdtlpdtrp0(xN, _465406))))), aElement0(_467115), aElementOf0(_467115, sdtlpdtrp0(xN, _465406)), -(_467115 = szmzizndt0(sdtlpdtrp0(xN, _465406)))], (2395 ^ _384323) ^ [] : [-(isCountable0(2349 ^ [_465406]))], (2361 ^ _384323) ^ [_466765] : [aElementOf0(_466765, sdtmndt0(sdtlpdtrp0(xN, _465406), szmzizndt0(sdtlpdtrp0(xN, _465406)))), 2364 ^ _384323 : [(2369 ^ _384323) ^ [] : [_466765 = szmzizndt0(sdtlpdtrp0(xN, _465406))], (2367 ^ _384323) ^ [] : [-(aElementOf0(_466765, sdtlpdtrp0(xN, _465406)))], (2365 ^ _384323) ^ [] : [-(aElement0(_466765))]]], (2385 ^ _384323) ^ [] : [-(aSet0(2349 ^ [_465406]))], (2348 ^ _384323) ^ [] : [-(aElementOf0(2346 ^ [_465406], xT))], (2351 ^ _384323) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _465406)), sdtlpdtrp0(xN, _465406)))], (2353 ^ _384323) ^ [_466448] : [aElementOf0(_466448, sdtlpdtrp0(xN, _465406)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _465406)), _466448))], (2359 ^ _384323) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _465406), szmzizndt0(sdtlpdtrp0(xN, _465406)))))], (2387 ^ _384323) ^ [_467600] : [aElementOf0(_467600, 2349 ^ [_465406]), -(aElementOf0(_467600, sdtmndt0(sdtlpdtrp0(xN, _465406), szmzizndt0(sdtlpdtrp0(xN, _465406)))))], (2393 ^ _384323) ^ [] : [-(aSubsetOf0(2349 ^ [_465406], sdtmndt0(sdtlpdtrp0(xN, _465406), szmzizndt0(sdtlpdtrp0(xN, _465406)))))], (2397 ^ _384323) ^ [_467958] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _465406), _467958) = 2346 ^ [_465406]), aSet0(_467958), 2402 ^ _384323 : [(2403 ^ _384323) ^ [] : [2405 ^ _384323 : [(2410 ^ _384323) ^ [] : [aSubsetOf0(_467958, 2349 ^ [_465406])], (2408 ^ _384323) ^ [] : [aElementOf0(2404 ^ [_465406, _467958], 2349 ^ [_465406])], (2406 ^ _384323) ^ [] : [-(aElementOf0(2404 ^ [_465406, _467958], _467958))]], sbrdtbr0(_467958) = xk], (2414 ^ _384323) ^ [] : [aElementOf0(_467958, slbdtsldtrb0(2349 ^ [_465406], xk))]]]]], (1462 ^ _384323) ^ [_430703] : [aFunction0(_430703), 1465 ^ _384323 : [(1466 ^ _384323) ^ [_430844] : [aElementOf0(_430844, szDzozmdt0(_430703)), -(aElementOf0(sdtlpdtrp0(_430703, _430844), sdtlcdtrc0(_430703, szDzozmdt0(_430703))))]]], (2466 ^ _384323) ^ [] : [-(szDzozmdt0(xd) = szNzAzT0)], (10 ^ _384323) ^ [_384758, _384760, _384762] : [-(_384762 = _384758), _384762 = _384760, _384760 = _384758], (98 ^ _384323) ^ [_387462, _387464, _387466, _387468] : [-(aSubsetOf0(_387466, _387462)), aSubsetOf0(_387468, _387464), _387468 = _387466, _387464 = _387462], (1559 ^ _384323) ^ [] : [-(aSet0(xS))], (672 ^ _384323) ^ [_405730] : [aElementOf0(_405730, szNzAzT0), -(_405730 = sz00), 680 ^ _384323 : [(683 ^ _384323) ^ [] : [-(_405730 = szszuzczcdt0(679 ^ [_405730]))], (681 ^ _384323) ^ [] : [-(aElementOf0(679 ^ [_405730], szNzAzT0))]]], (1326 ^ _384323) ^ [_425700] : [aFunction0(_425700), 1329 ^ _384323 : [(1330 ^ _384323) ^ [_425835] : [aElementOf0(_425835, szDzozmdt0(_425700)), -(aElement0(sdtlpdtrp0(_425700, _425835)))]]], (2616 ^ _384323) ^ [] : [-(aSubsetOf0(xO, xS))], (685 ^ _384323) ^ [_406147] : [aElementOf0(_406147, szNzAzT0), _406147 = szszuzczcdt0(_406147)], (831 ^ _384323) ^ [_410276] : [aSet0(_410276), -(aElement0(sbrdtbr0(_410276)))], (630 ^ _384323) ^ [_404470] : [aElement0(_404470), 633 ^ _384323 : [(634 ^ _384323) ^ [_404607] : [-(isFinite0(sdtmndt0(_404607, _404470))), aSet0(_404607), isFinite0(_404607)]]], (2448 ^ _384323) ^ [] : [-(szDzozmdt0(xe) = szNzAzT0)], (936 ^ _384323) ^ [_413395] : [aSubsetOf0(_413395, szNzAzT0), -(_413395 = slcrc0), 943 ^ _384323 : [(956 ^ _384323) ^ [_414058] : [-(_414058 = szmzizndt0(_413395)), aElementOf0(_414058, _413395), 962 ^ _384323 : [(965 ^ _384323) ^ [] : [sdtlseqdt0(_414058, 961 ^ [_413395, _414058])], (963 ^ _384323) ^ [] : [-(aElementOf0(961 ^ [_413395, _414058], _413395))]]], (944 ^ _384323) ^ [_413664] : [_413664 = szmzizndt0(_413395), 947 ^ _384323 : [(950 ^ _384323) ^ [_413879] : [aElementOf0(_413879, _413395), -(sdtlseqdt0(_413664, _413879))], (948 ^ _384323) ^ [] : [-(aElementOf0(_413664, _413395))]]]]], (2546 ^ _384323) ^ [] : [-(aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd))))], (78 ^ _384323) ^ [_386844, _386846] : [-(isCountable0(_386844)), _386846 = _386844, isCountable0(_386846)], (1589 ^ _384323) ^ [_435195] : [-(aElementOf0(_435195, szDzozmdt0(xc))), sbrdtbr0(_435195) = xK, 1592 ^ _384323 : [(1593 ^ _384323) ^ [] : [aSet0(_435195), 1597 ^ _384323 : [(1600 ^ _384323) ^ [] : [aElementOf0(1596 ^ [_435195], xS)], (1598 ^ _384323) ^ [] : [-(aElementOf0(1596 ^ [_435195], _435195))]]], (1602 ^ _384323) ^ [] : [aSubsetOf0(_435195, xS)]]], (2585 ^ _384323) ^ [] : [-(xO = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))], (969 ^ _384323) ^ [_414503] : [aSubsetOf0(_414503, szNzAzT0), isFinite0(_414503), -(_414503 = slcrc0), 980 ^ _384323 : [(993 ^ _384323) ^ [_415249] : [-(_415249 = szmzazxdt0(_414503)), aElementOf0(_415249, _414503), 999 ^ _384323 : [(1002 ^ _384323) ^ [] : [sdtlseqdt0(998 ^ [_414503, _415249], _415249)], (1000 ^ _384323) ^ [] : [-(aElementOf0(998 ^ [_414503, _415249], _414503))]]], (981 ^ _384323) ^ [_414855] : [_414855 = szmzazxdt0(_414503), 984 ^ _384323 : [(987 ^ _384323) ^ [_415070] : [aElementOf0(_415070, _414503), -(sdtlseqdt0(_415070, _414855))], (985 ^ _384323) ^ [] : [-(aElementOf0(_414855, _414503))]]]]], (366 ^ _384323) ^ [_396141] : [aSet0(_396141), isFinite0(_396141), 373 ^ _384323 : [(374 ^ _384323) ^ [_396354] : [aSubsetOf0(_396354, _396141), -(isFinite0(_396354))]]], (901 ^ _384323) ^ [_412327] : [aSet0(_412327), 904 ^ _384323 : [(905 ^ _384323) ^ [_412467] : [-(sdtlseqdt0(sbrdtbr0(_412467), sbrdtbr0(_412327))), isFinite0(_412327), aSubsetOf0(_412467, _412327)]]], (132 ^ _384323) ^ [_388542, _388544] : [_388544 = _388542, -(slbdtrb0(_388544) = slbdtrb0(_388542))], (1310 ^ _384323) ^ [_425255] : [aFunction0(_425255), true___, -(true___)], (180 ^ _384323) ^ [_390273, _390275] : [_390275 = _390273, -(szDzozmdt0(_390275) = szDzozmdt0(_390273))], (1569 ^ _384323) ^ [] : [-(isCountable0(xS))], (228 ^ _384323) ^ [_392012, _392014, _392016, _392018] : [-(slbdtsldtrb0(_392018, _392014) = slbdtsldtrb0(_392016, _392012)), _392018 = _392016, _392014 = _392012], (1631 ^ _384323) ^ [_436548] : [aElementOf0(_436548, sdtlcdtrc0(xc, szDzozmdt0(xc))), -(aElementOf0(_436548, xT))], (1612 ^ _384323) ^ [_435901] : [aElementOf0(_435901, sdtlcdtrc0(xc, szDzozmdt0(xc))), 1616 ^ _384323 : [(1619 ^ _384323) ^ [] : [-(sdtlpdtrp0(xc, 1615 ^ [_435901]) = _435901)], (1617 ^ _384323) ^ [] : [-(aElementOf0(1615 ^ [_435901], szDzozmdt0(xc)))]]], (2610 ^ _384323) ^ [_475421] : [aElementOf0(_475421, xO), -(aElementOf0(_475421, xS))], (337 ^ _384323) ^ [_395140] : [aSet0(_395140), 340 ^ _384323 : [(353 ^ _384323) ^ [_395704] : [-(aSubsetOf0(_395704, _395140)), aSet0(_395704), 359 ^ _384323 : [(362 ^ _384323) ^ [] : [aElementOf0(358 ^ [_395140, _395704], _395140)], (360 ^ _384323) ^ [] : [-(aElementOf0(358 ^ [_395140, _395704], _395704))]]], (341 ^ _384323) ^ [_395316] : [aSubsetOf0(_395316, _395140), 344 ^ _384323 : [(347 ^ _384323) ^ [_395525] : [aElementOf0(_395525, _395316), -(aElementOf0(_395525, _395140))], (345 ^ _384323) ^ [] : [-(aSet0(_395316))]]]]], (1783 ^ _384323) ^ [] : [-(szDzozmdt0(xN) = szNzAzT0)], (1777 ^ _384323) ^ [] : [-(aElementOf0(xk, szNzAzT0))], (2587 ^ _384323) ^ [] : [-(aSet0(xO))], (1921 ^ _384323) ^ [_447966] : [aElementOf0(_447966, szNzAzT0), 1924 ^ _384323 : [(1925 ^ _384323) ^ [_448431] : [aSet0(_448431), 1930 ^ _384323 : [(1976 ^ _384323) ^ [] : [aElementOf0(_448431, slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _447966), szmzizndt0(sdtlpdtrp0(xN, _447966))), xk))], (1941 ^ _384323) ^ [_449347] : [aElementOf0(_449347, sdtmndt0(sdtlpdtrp0(xN, _447966), szmzizndt0(sdtlpdtrp0(xN, _447966)))), 1944 ^ _384323 : [(1949 ^ _384323) ^ [] : [_449347 = szmzizndt0(sdtlpdtrp0(xN, _447966))], (1947 ^ _384323) ^ [] : [-(aElementOf0(_449347, sdtlpdtrp0(xN, _447966)))], (1945 ^ _384323) ^ [] : [-(aElement0(_449347))]]], (1951 ^ _384323) ^ [_449709] : [-(aElementOf0(_449709, sdtmndt0(sdtlpdtrp0(xN, _447966), szmzizndt0(sdtlpdtrp0(xN, _447966))))), aElement0(_449709), aElementOf0(_449709, sdtlpdtrp0(xN, _447966)), -(_449709 = szmzizndt0(sdtlpdtrp0(xN, _447966)))], (1965 ^ _384323) ^ [] : [1967 ^ _384323 : [(1972 ^ _384323) ^ [] : [aSubsetOf0(_448431, sdtmndt0(sdtlpdtrp0(xN, _447966), szmzizndt0(sdtlpdtrp0(xN, _447966))))], (1970 ^ _384323) ^ [] : [aElementOf0(1966 ^ [_447966, _448431], sdtmndt0(sdtlpdtrp0(xN, _447966), szmzizndt0(sdtlpdtrp0(xN, _447966))))], (1968 ^ _384323) ^ [] : [-(aElementOf0(1966 ^ [_447966, _448431], _448431))]], sbrdtbr0(_448431) = xk], (1931 ^ _384323) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _447966)), sdtlpdtrp0(xN, _447966)))], (1933 ^ _384323) ^ [_449018] : [aElementOf0(_449018, sdtlpdtrp0(xN, _447966)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _447966)), _449018))], (1939 ^ _384323) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _447966), szmzizndt0(sdtlpdtrp0(xN, _447966)))))]], 1977 ^ _384323 : [(2020 ^ _384323) ^ [] : [-(sbrdtbr0(sdtpldt0(_448431, szmzizndt0(sdtlpdtrp0(xN, _447966)))) = xK)], (1978 ^ _384323) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _447966)), sdtlpdtrp0(xN, _447966)))], (1980 ^ _384323) ^ [_450678] : [aElementOf0(_450678, sdtlpdtrp0(xN, _447966)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _447966)), _450678))], (2012 ^ _384323) ^ [_451770] : [aElementOf0(_451770, sdtpldt0(_448431, szmzizndt0(sdtlpdtrp0(xN, _447966)))), -(aElementOf0(_451770, xS))], (2022 ^ _384323) ^ [] : [-(aElementOf0(sdtpldt0(_448431, szmzizndt0(sdtlpdtrp0(xN, _447966))), slbdtsldtrb0(xS, xK)))], (2000 ^ _384323) ^ [_451369] : [-(aElementOf0(_451369, sdtpldt0(_448431, szmzizndt0(sdtlpdtrp0(xN, _447966))))), aElement0(_451369), 2005 ^ _384323 : [(2008 ^ _384323) ^ [] : [_451369 = szmzizndt0(sdtlpdtrp0(xN, _447966))], (2006 ^ _384323) ^ [] : [aElementOf0(_451369, _448431)]]], (2018 ^ _384323) ^ [] : [-(aSubsetOf0(sdtpldt0(_448431, szmzizndt0(sdtlpdtrp0(xN, _447966))), xS))], (1988 ^ _384323) ^ [_451002] : [aElementOf0(_451002, sdtpldt0(_448431, szmzizndt0(sdtlpdtrp0(xN, _447966)))), 1991 ^ _384323 : [(1994 ^ _384323) ^ [] : [-(aElementOf0(_451002, _448431)), -(_451002 = szmzizndt0(sdtlpdtrp0(xN, _447966)))], (1992 ^ _384323) ^ [] : [-(aElement0(_451002))]]], (1986 ^ _384323) ^ [] : [-(aSet0(sdtpldt0(_448431, szmzizndt0(sdtlpdtrp0(xN, _447966)))))]]]]], (1621 ^ _384323) ^ [_436201] : [-(aElementOf0(_436201, sdtlcdtrc0(xc, szDzozmdt0(xc)))), 1622 ^ _384323 : [(1623 ^ _384323) ^ [_436294] : [aElementOf0(_436294, szDzozmdt0(xc)), sdtlpdtrp0(xc, _436294) = _436201]]], (212 ^ _384323) ^ [_391455, _391457, _391459, _391461] : [-(sdtlpdtrp0(_391461, _391457) = sdtlpdtrp0(_391459, _391455)), _391461 = _391459, _391457 = _391455], (186 ^ _384323) ^ [_390519, _390521, _390523, _390525] : [-(sdtlcdtrc0(_390525, _390521) = sdtlcdtrc0(_390523, _390519)), _390525 = _390523, _390521 = _390519], (303 ^ _384323) ^ [_394257] : [aSet0(_394257), isCountable0(_394257), true___, -(true___)], (290 ^ _384323) ^ [_393875] : [-(_393875 = slcrc0), aSet0(_393875), -(aElementOf0(295 ^ [_393875], _393875))], (1229 ^ _384323) ^ [_422677] : [aSet0(_422677), -(isFinite0(_422677)), 1236 ^ _384323 : [(1237 ^ _384323) ^ [_422899] : [aElementOf0(_422899, szNzAzT0), slbdtsldtrb0(_422677, _422899) = slcrc0]]], (68 ^ _384323) ^ [_386549, _386551] : [-(aFunction0(_386549)), _386551 = _386549, aFunction0(_386551)], (1854 ^ _384323) ^ [_445638] : [aElementOf0(_445638, szNzAzT0), 1857 ^ _384323 : [(1866 ^ _384323) ^ [] : [-(aSubsetOf0(sdtlpdtrp0(xN, _445638), szNzAzT0))], (1868 ^ _384323) ^ [] : [-(isCountable0(sdtlpdtrp0(xN, _445638)))], (1860 ^ _384323) ^ [_445885] : [aElementOf0(_445885, sdtlpdtrp0(xN, _445638)), -(aElementOf0(_445885, szNzAzT0))], (1858 ^ _384323) ^ [] : [-(aSet0(sdtlpdtrp0(xN, _445638)))]]], (238 ^ _384323) ^ [_392415] : [aSet0(_392415), true___, -(true___)], (853 ^ _384323) ^ [_410897] : [aSet0(_410897), 856 ^ _384323 : [(863 ^ _384323) ^ [] : [_410897 = slcrc0, -(sbrdtbr0(_410897) = sz00)], (857 ^ _384323) ^ [] : [sbrdtbr0(_410897) = sz00, -(_410897 = slcrc0)]]], (138 ^ _384323) ^ [_388788, _388790, _388792, _388794] : [-(sdtexdt0(_388794, _388790) = sdtexdt0(_388792, _388788)), _388794 = _388792, _388790 = _388788], (2591 ^ _384323) ^ [_474666] : [2601 ^ _384323 : [(2604 ^ _384323) ^ [] : [-(sdtlpdtrp0(xd, 2600 ^ [_474666]) = szDzizrdt0(xd))], (2606 ^ _384323) ^ [] : [-(aElementOf0(2600 ^ [_474666], sdtlbdtrb0(xd, szDzizrdt0(xd))))], (2608 ^ _384323) ^ [] : [-(sdtlpdtrp0(xe, 2600 ^ [_474666]) = _474666)], (2602 ^ _384323) ^ [] : [-(aElementOf0(2600 ^ [_474666], szNzAzT0))]], 2592 ^ _384323 : [(2593 ^ _384323) ^ [_474814] : [aElementOf0(_474814, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlpdtrp0(xe, _474814) = _474666], (2599 ^ _384323) ^ [] : [aElementOf0(_474666, xO)]]], (807 ^ _384323) ^ [_409632, _409634] : [aElementOf0(_409634, szNzAzT0), aElementOf0(_409632, szNzAzT0), iLess0(_409634, _409632), true___, -(true___)], (2520 ^ _384323) ^ [] : [-(aSubsetOf0(sdtlcdtrc0(xd, szDzozmdt0(xd)), xT))], (327 ^ _384323) ^ [_394868] : [_394868 = slcrc0, aSet0(_394868), isCountable0(_394868)], (222 ^ _384323) ^ [_391786, _391788] : [_391788 = _391786, -(sbrdtbr0(_391788) = sbrdtbr0(_391786))], (1561 ^ _384323) ^ [_434296] : [aElementOf0(_434296, xS), -(aElementOf0(_434296, szNzAzT0))], (709 ^ _384323) ^ [_406806] : [aElementOf0(_406806, szNzAzT0), -(sdtlseqdt0(sz00, _406806))], (2514 ^ _384323) ^ [_472278] : [aElementOf0(_472278, sdtlcdtrc0(xd, szDzozmdt0(xd))), -(aElementOf0(_472278, xT))], (2548 ^ _384323) ^ [_473321] : [aElementOf0(_473321, sdtlbdtrb0(xd, szDzizrdt0(xd))), 2551 ^ _384323 : [(2554 ^ _384323) ^ [] : [-(sdtlpdtrp0(xd, _473321) = szDzizrdt0(xd))], (2552 ^ _384323) ^ [] : [-(aElementOf0(_473321, szDzozmdt0(xd)))]]], (386 ^ _384323) ^ [_396759, _396761] : [aSet0(_396761), aSet0(_396759), -(_396761 = _396759), aSubsetOf0(_396761, _396759), aSubsetOf0(_396759, _396761)], (1787 ^ _384323) ^ [_443221] : [aElementOf0(_443221, szNzAzT0), isCountable0(sdtlpdtrp0(xN, _443221)), 1794 ^ _384323 : [(1795 ^ _384323) ^ [] : [aSet0(sdtlpdtrp0(xN, _443221)), 1799 ^ _384323 : [(1802 ^ _384323) ^ [] : [aElementOf0(1798 ^ [_443221], szNzAzT0)], (1800 ^ _384323) ^ [] : [-(aElementOf0(1798 ^ [_443221], sdtlpdtrp0(xN, _443221)))]]], (1804 ^ _384323) ^ [] : [aSubsetOf0(sdtlpdtrp0(xN, _443221), szNzAzT0)]], 1807 ^ _384323 : [(1850 ^ _384323) ^ [] : [-(aSubsetOf0(sdtlpdtrp0(xN, szszuzczcdt0(_443221)), sdtmndt0(sdtlpdtrp0(xN, _443221), szmzizndt0(sdtlpdtrp0(xN, _443221)))))], (1808 ^ _384323) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _443221)), sdtlpdtrp0(xN, _443221)))], (1810 ^ _384323) ^ [_444089] : [aElementOf0(_444089, sdtlpdtrp0(xN, _443221)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _443221)), _444089))], (1844 ^ _384323) ^ [_445241] : [aElementOf0(_445241, sdtlpdtrp0(xN, szszuzczcdt0(_443221))), -(aElementOf0(_445241, sdtmndt0(sdtlpdtrp0(xN, _443221), szmzizndt0(sdtlpdtrp0(xN, _443221)))))], (1852 ^ _384323) ^ [] : [-(isCountable0(sdtlpdtrp0(xN, szszuzczcdt0(_443221))))], (1828 ^ _384323) ^ [_444756] : [-(aElementOf0(_444756, sdtmndt0(sdtlpdtrp0(xN, _443221), szmzizndt0(sdtlpdtrp0(xN, _443221))))), aElement0(_444756), aElementOf0(_444756, sdtlpdtrp0(xN, _443221)), -(_444756 = szmzizndt0(sdtlpdtrp0(xN, _443221)))], (1842 ^ _384323) ^ [] : [-(aSet0(sdtlpdtrp0(xN, szszuzczcdt0(_443221))))], (1818 ^ _384323) ^ [_444406] : [aElementOf0(_444406, sdtmndt0(sdtlpdtrp0(xN, _443221), szmzizndt0(sdtlpdtrp0(xN, _443221)))), 1821 ^ _384323 : [(1826 ^ _384323) ^ [] : [_444406 = szmzizndt0(sdtlpdtrp0(xN, _443221))], (1824 ^ _384323) ^ [] : [-(aElementOf0(_444406, sdtlpdtrp0(xN, _443221)))], (1822 ^ _384323) ^ [] : [-(aElement0(_444406))]]], (1816 ^ _384323) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _443221), szmzizndt0(sdtlpdtrp0(xN, _443221)))))]]], (1032 ^ _384323) ^ [_416377] : [aElementOf0(_416377, szNzAzT0), 1035 ^ _384323 : [(1036 ^ _384323) ^ [_416565] : [_416565 = slbdtrb0(_416377), 1039 ^ _384323 : [(1050 ^ _384323) ^ [_417068] : [-(aElementOf0(_417068, _416565)), aElementOf0(_417068, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_417068), _416377)], (1042 ^ _384323) ^ [_416815] : [aElementOf0(_416815, _416565), 1045 ^ _384323 : [(1048 ^ _384323) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(_416815), _416377))], (1046 ^ _384323) ^ [] : [-(aElementOf0(_416815, szNzAzT0))]]], (1040 ^ _384323) ^ [] : [-(aSet0(_416565))]]], (1060 ^ _384323) ^ [_417346] : [-(_417346 = slbdtrb0(_416377)), aSet0(_417346), 1076 ^ _384323 : [(1081 ^ _384323) ^ [] : [aElementOf0(1065 ^ [_416377, _417346], _417346)], (1079 ^ _384323) ^ [] : [-(sdtlseqdt0(szszuzczcdt0(1065 ^ [_416377, _417346]), _416377))], (1077 ^ _384323) ^ [] : [-(aElementOf0(1065 ^ [_416377, _417346], szNzAzT0))]], 1068 ^ _384323 : [(1071 ^ _384323) ^ [] : [aElementOf0(1065 ^ [_416377, _417346], szNzAzT0), sdtlseqdt0(szszuzczcdt0(1065 ^ [_416377, _417346]), _416377)], (1069 ^ _384323) ^ [] : [-(aElementOf0(1065 ^ [_416377, _417346], _417346))]]]]], (2028 ^ _384323) ^ [_452338] : [aElementOf0(_452338, szNzAzT0), 2031 ^ _384323 : [(2042 ^ _384323) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _452338), szmzizndt0(sdtlpdtrp0(xN, _452338)))))], (2105 ^ _384323) ^ [_455620] : [2157 ^ _384323 : [(2158 ^ _384323) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _452338)), sdtlpdtrp0(xN, _452338)))], (2190 ^ _384323) ^ [] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _452338), _455620) = sdtlpdtrp0(xc, sdtpldt0(_455620, szmzizndt0(sdtlpdtrp0(xN, _452338)))))], (2178 ^ _384323) ^ [_458426] : [-(aElementOf0(_458426, sdtpldt0(_455620, szmzizndt0(sdtlpdtrp0(xN, _452338))))), aElement0(_458426), 2183 ^ _384323 : [(2186 ^ _384323) ^ [] : [_458426 = szmzizndt0(sdtlpdtrp0(xN, _452338))], (2184 ^ _384323) ^ [] : [aElementOf0(_458426, _455620)]]], (2166 ^ _384323) ^ [_458059] : [aElementOf0(_458059, sdtpldt0(_455620, szmzizndt0(sdtlpdtrp0(xN, _452338)))), 2169 ^ _384323 : [(2172 ^ _384323) ^ [] : [-(aElementOf0(_458059, _455620)), -(_458059 = szmzizndt0(sdtlpdtrp0(xN, _452338)))], (2170 ^ _384323) ^ [] : [-(aElement0(_458059))]]], (2160 ^ _384323) ^ [_457808] : [aElementOf0(_457808, sdtlpdtrp0(xN, _452338)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _452338)), _457808))]], aSet0(_455620), 2110 ^ _384323 : [(2156 ^ _384323) ^ [] : [aElementOf0(_455620, slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _452338), szmzizndt0(sdtlpdtrp0(xN, _452338))), xk))], (2121 ^ _384323) ^ [_456477] : [aElementOf0(_456477, sdtmndt0(sdtlpdtrp0(xN, _452338), szmzizndt0(sdtlpdtrp0(xN, _452338)))), 2124 ^ _384323 : [(2129 ^ _384323) ^ [] : [_456477 = szmzizndt0(sdtlpdtrp0(xN, _452338))], (2127 ^ _384323) ^ [] : [-(aElementOf0(_456477, sdtlpdtrp0(xN, _452338)))], (2125 ^ _384323) ^ [] : [-(aElement0(_456477))]]], (2131 ^ _384323) ^ [_456839] : [-(aElementOf0(_456839, sdtmndt0(sdtlpdtrp0(xN, _452338), szmzizndt0(sdtlpdtrp0(xN, _452338))))), aElement0(_456839), aElementOf0(_456839, sdtlpdtrp0(xN, _452338)), -(_456839 = szmzizndt0(sdtlpdtrp0(xN, _452338)))], (2145 ^ _384323) ^ [] : [2147 ^ _384323 : [(2152 ^ _384323) ^ [] : [aSubsetOf0(_455620, sdtmndt0(sdtlpdtrp0(xN, _452338), szmzizndt0(sdtlpdtrp0(xN, _452338))))], (2150 ^ _384323) ^ [] : [aElementOf0(2146 ^ [_452338, _455620], sdtmndt0(sdtlpdtrp0(xN, _452338), szmzizndt0(sdtlpdtrp0(xN, _452338))))], (2148 ^ _384323) ^ [] : [-(aElementOf0(2146 ^ [_452338, _455620], _455620))]], sbrdtbr0(_455620) = xk], (2111 ^ _384323) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _452338)), sdtlpdtrp0(xN, _452338)))], (2113 ^ _384323) ^ [_456148] : [aElementOf0(_456148, sdtlpdtrp0(xN, _452338)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _452338)), _456148))], (2119 ^ _384323) ^ [] : [-(aSet0(sdtmndt0(sdtlpdtrp0(xN, _452338), szmzizndt0(sdtlpdtrp0(xN, _452338)))))]]], (2034 ^ _384323) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _452338)), sdtlpdtrp0(xN, _452338)))], (2032 ^ _384323) ^ [] : [-(aFunction0(sdtlpdtrp0(xC, _452338)))], (2054 ^ _384323) ^ [_453849] : [-(aElementOf0(_453849, sdtmndt0(sdtlpdtrp0(xN, _452338), szmzizndt0(sdtlpdtrp0(xN, _452338))))), aElement0(_453849), aElementOf0(_453849, sdtlpdtrp0(xN, _452338)), -(_453849 = szmzizndt0(sdtlpdtrp0(xN, _452338)))], (2103 ^ _384323) ^ [] : [-(szDzozmdt0(sdtlpdtrp0(xC, _452338)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN, _452338), szmzizndt0(sdtlpdtrp0(xN, _452338))), xk))], (2036 ^ _384323) ^ [_453182] : [aElementOf0(_453182, sdtlpdtrp0(xN, _452338)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _452338)), _453182))], (2084 ^ _384323) ^ [_454893] : [-(aElementOf0(_454893, szDzozmdt0(sdtlpdtrp0(xC, _452338)))), sbrdtbr0(_454893) = xk, 2087 ^ _384323 : [(2088 ^ _384323) ^ [] : [aSet0(_454893), 2092 ^ _384323 : [(2095 ^ _384323) ^ [] : [aElementOf0(2091 ^ [_452338, _454893], sdtmndt0(sdtlpdtrp0(xN, _452338), szmzizndt0(sdtlpdtrp0(xN, _452338))))], (2093 ^ _384323) ^ [] : [-(aElementOf0(2091 ^ [_452338, _454893], _454893))]]], (2097 ^ _384323) ^ [] : [aSubsetOf0(_454893, sdtmndt0(sdtlpdtrp0(xN, _452338), szmzizndt0(sdtlpdtrp0(xN, _452338))))]]], (2044 ^ _384323) ^ [_453499] : [aElementOf0(_453499, sdtmndt0(sdtlpdtrp0(xN, _452338), szmzizndt0(sdtlpdtrp0(xN, _452338)))), 2047 ^ _384323 : [(2052 ^ _384323) ^ [] : [_453499 = szmzizndt0(sdtlpdtrp0(xN, _452338))], (2050 ^ _384323) ^ [] : [-(aElementOf0(_453499, sdtlpdtrp0(xN, _452338)))], (2048 ^ _384323) ^ [] : [-(aElement0(_453499))]]], (2068 ^ _384323) ^ [_454286] : [aElementOf0(_454286, szDzozmdt0(sdtlpdtrp0(xC, _452338))), 2071 ^ _384323 : [(2080 ^ _384323) ^ [] : [-(aSubsetOf0(_454286, sdtmndt0(sdtlpdtrp0(xN, _452338), szmzizndt0(sdtlpdtrp0(xN, _452338)))))], (2082 ^ _384323) ^ [] : [-(sbrdtbr0(_454286) = xk)], (2074 ^ _384323) ^ [_454561] : [aElementOf0(_454561, _454286), -(aElementOf0(_454561, sdtmndt0(sdtlpdtrp0(xN, _452338), szmzizndt0(sdtlpdtrp0(xN, _452338)))))], (2072 ^ _384323) ^ [] : [-(aSet0(_454286))]]]]], (1779 ^ _384323) ^ [] : [-(szszuzczcdt0(xk) = xK)], (825 ^ _384323) ^ [_410082] : [aElementOf0(_410082, szNzAzT0), -(iLess0(_410082, szszuzczcdt0(_410082)))], (2024 ^ _384323) ^ [] : [-(aFunction0(xC))], (2620 ^ _384323) ^ [_475699] : [aElementOf0(_475699, xQ), -(aElementOf0(_475699, xO))], (616 ^ _384323) ^ [_404041] : [aElement0(_404041), 619 ^ _384323 : [(620 ^ _384323) ^ [_404178] : [-(isFinite0(sdtpldt0(_404178, _404041))), aSet0(_404178), isFinite0(_404178)]]], (426 ^ _384323) ^ [_397834, _397836] : [aSet0(_397836), aElement0(_397834), 433 ^ _384323 : [(434 ^ _384323) ^ [_398115] : [_398115 = sdtpldt0(_397836, _397834), 437 ^ _384323 : [(452 ^ _384323) ^ [_398733] : [-(aElementOf0(_398733, _398115)), aElement0(_398733), 457 ^ _384323 : [(460 ^ _384323) ^ [] : [_398733 = _397834], (458 ^ _384323) ^ [] : [aElementOf0(_398733, _397836)]]], (440 ^ _384323) ^ [_398378] : [aElementOf0(_398378, _398115), 443 ^ _384323 : [(446 ^ _384323) ^ [] : [-(aElementOf0(_398378, _397836)), -(_398378 = _397834)], (444 ^ _384323) ^ [] : [-(aElement0(_398378))]]], (438 ^ _384323) ^ [] : [-(aSet0(_398115))]]], (464 ^ _384323) ^ [_399095] : [-(_399095 = sdtpldt0(_397836, _397834)), aSet0(_399095), 472 ^ _384323 : [(475 ^ _384323) ^ [] : [aElement0(469 ^ [_397834, _397836, _399095]), 478 ^ _384323 : [(481 ^ _384323) ^ [] : [469 ^ [_397834, _397836, _399095] = _397834], (479 ^ _384323) ^ [] : [aElementOf0(469 ^ [_397834, _397836, _399095], _397836)]]], (473 ^ _384323) ^ [] : [-(aElementOf0(469 ^ [_397834, _397836, _399095], _399095))]], 482 ^ _384323 : [(485 ^ _384323) ^ [] : [-(aElementOf0(469 ^ [_397834, _397836, _399095], _397836)), -(469 ^ [_397834, _397836, _399095] = _397834)], (483 ^ _384323) ^ [] : [-(aElement0(469 ^ [_397834, _397836, _399095]))], (491 ^ _384323) ^ [] : [aElementOf0(469 ^ [_397834, _397836, _399095], _399095)]]]]], (1093 ^ _384323) ^ [_418408, _418410] : [aElementOf0(_418410, szNzAzT0), aElementOf0(_418408, szNzAzT0), 1100 ^ _384323 : [(1101 ^ _384323) ^ [] : [aElementOf0(_418410, slbdtrb0(szszuzczcdt0(_418408))), -(aElementOf0(_418410, slbdtrb0(_418408))), -(_418410 = _418408)], (1111 ^ _384323) ^ [] : [1112 ^ _384323 : [(1115 ^ _384323) ^ [] : [_418410 = _418408], (1113 ^ _384323) ^ [] : [aElementOf0(_418410, slbdtrb0(_418408))]], -(aElementOf0(_418410, slbdtrb0(szszuzczcdt0(_418408))))]]], (1781 ^ _384323) ^ [] : [-(aFunction0(xN))], (1610 ^ _384323) ^ [] : [-(aSet0(sdtlcdtrc0(xc, szDzozmdt0(xc))))], (248 ^ _384323) ^ [_392670] : [aElement0(_392670), true___, -(true___)], (691 ^ _384323) ^ [_406356, _406358] : [aElementOf0(_406358, szNzAzT0), aElementOf0(_406356, szNzAzT0), sdtlseqdt0(_406358, _406356), true___, -(true___)], (2544 ^ _384323) ^ [] : [-(aSet0(xO))], (258 ^ _384323) ^ [_392925] : [aSet0(_392925), 261 ^ _384323 : [(262 ^ _384323) ^ [_393055] : [aElementOf0(_393055, _392925), -(aElement0(_393055))]]], (1773 ^ _384323) ^ [] : [xK = sz00], (30 ^ _384323) ^ [_385394, _385396, _385398, _385400] : [-(iLess0(_385398, _385394)), iLess0(_385400, _385396), _385400 = _385398, _385396 = _385394], (715 ^ _384323) ^ [_406996] : [aElementOf0(_406996, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_406996), sz00)], (2556 ^ _384323) ^ [_473556] : [-(aElementOf0(_473556, sdtlbdtrb0(xd, szDzizrdt0(xd)))), aElementOf0(_473556, szDzozmdt0(xd)), sdtlpdtrp0(xd, _473556) = szDzizrdt0(xd)], (1870 ^ _384323) ^ [_446229, _446231] : [aElementOf0(_446231, szNzAzT0), aElementOf0(_446229, szNzAzT0), sdtlseqdt0(_446229, _446231), 1881 ^ _384323 : [(1882 ^ _384323) ^ [_446578] : [aElementOf0(_446578, sdtlpdtrp0(xN, _446231)), -(aElementOf0(_446578, sdtlpdtrp0(xN, _446229)))], (1888 ^ _384323) ^ [] : [-(aSubsetOf0(sdtlpdtrp0(xN, _446231), sdtlpdtrp0(xN, _446229)))]]], (1890 ^ _384323) ^ [_446875, _446877] : [aElementOf0(_446877, szNzAzT0), aElementOf0(_446875, szNzAzT0), -(_446877 = _446875), 1901 ^ _384323 : [(1904 ^ _384323) ^ [_447366] : [aElementOf0(_447366, sdtlpdtrp0(xN, _446877)), -(sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _446877)), _447366))], (1919 ^ _384323) ^ [] : [szmzizndt0(sdtlpdtrp0(xN, _446877)) = szmzizndt0(sdtlpdtrp0(xN, _446875))], (1910 ^ _384323) ^ [] : [aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _446877)), sdtlpdtrp0(xN, _446875)), 1914 ^ _384323 : [(1917 ^ _384323) ^ [] : [sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN, _446877)), 1913 ^ [_446875, _446877])], (1915 ^ _384323) ^ [] : [-(aElementOf0(1913 ^ [_446875, _446877], sdtlpdtrp0(xN, _446875)))]]], (1902 ^ _384323) ^ [] : [-(aElementOf0(szmzizndt0(sdtlpdtrp0(xN, _446877)), sdtlpdtrp0(xN, _446877)))]]], (2618 ^ _384323) ^ [] : [-(aSet0(xQ))], (2450 ^ _384323) ^ [_469957] : [aElementOf0(_469957, szNzAzT0), 2453 ^ _384323 : [(2456 ^ _384323) ^ [_470212] : [aElementOf0(_470212, sdtlpdtrp0(xN, _469957)), -(sdtlseqdt0(sdtlpdtrp0(xe, _469957), _470212))], (2462 ^ _384323) ^ [] : [-(sdtlpdtrp0(xe, _469957) = szmzizndt0(sdtlpdtrp0(xN, _469957)))], (2454 ^ _384323) ^ [] : [-(aElementOf0(sdtlpdtrp0(xe, _469957), sdtlpdtrp0(xN, _469957)))]]], (2464 ^ _384323) ^ [] : [-(aFunction0(xd))], (1567 ^ _384323) ^ [] : [-(aSubsetOf0(xS, szNzAzT0))], (54 ^ _384323) ^ [_386133, _386135, _386137, _386139] : [-(sdtlseqdt0(_386137, _386133)), sdtlseqdt0(_386139, _386135), _386139 = _386137, _386135 = _386133], (2628 ^ _384323) ^ [] : [-(sbrdtbr0(xQ) = xK)], (1573 ^ _384323) ^ [_434673] : [aElementOf0(_434673, szDzozmdt0(xc)), 1576 ^ _384323 : [(1585 ^ _384323) ^ [] : [-(aSubsetOf0(_434673, xS))], (1587 ^ _384323) ^ [] : [-(sbrdtbr0(_434673) = xK)], (1579 ^ _384323) ^ [_434908] : [aElementOf0(_434908, _434673), -(aElementOf0(_434908, xS))], (1577 ^ _384323) ^ [] : [-(aSet0(_434673))]]], (1320 ^ _384323) ^ [_425510] : [aFunction0(_425510), -(aSet0(szDzozmdt0(_425510)))], (1785 ^ _384323) ^ [] : [-(sdtlpdtrp0(xN, sz00) = xS)], (1261 ^ _384323) ^ [_423636] : [aElementOf0(_423636, szNzAzT0), 1264 ^ _384323 : [(1265 ^ _384323) ^ [_423823, _423825] : [aSet0(_423825), aSet0(_423823), -(_423636 = sz00), -(aSubsetOf0(_423825, _423823)), aSubsetOf0(slbdtsldtrb0(_423825, _423636), slbdtsldtrb0(_423823, _423636)), -(slbdtsldtrb0(_423825, _423636) = slcrc0)]]], (2418 ^ _384323) ^ [_468718] : [aElementOf0(_468718, szNzAzT0), 2422 ^ _384323 : [(2425 ^ _384323) ^ [_469109] : [-(sdtlpdtrp0(sdtlpdtrp0(xC, _468718), _469109) = 2421 ^ [_468718]), aSet0(_469109), 2430 ^ _384323 : [(2431 ^ _384323) ^ [] : [2433 ^ _384323 : [(2438 ^ _384323) ^ [] : [aSubsetOf0(_469109, sdtlpdtrp0(xN, szszuzczcdt0(_468718)))], (2436 ^ _384323) ^ [] : [aElementOf0(2432 ^ [_468718, _469109], sdtlpdtrp0(xN, szszuzczcdt0(_468718)))], (2434 ^ _384323) ^ [] : [-(aElementOf0(2432 ^ [_468718, _469109], _469109))]], sbrdtbr0(_469109) = xk], (2442 ^ _384323) ^ [] : [aElementOf0(_469109, slbdtsldtrb0(sdtlpdtrp0(xN, szszuzczcdt0(_468718)), xk))]]], (2423 ^ _384323) ^ [] : [-(aElementOf0(2421 ^ [_468718], xT))]]], (88 ^ _384323) ^ [_387139, _387141] : [-(aSet0(_387139)), _387141 = _387139, aSet0(_387141)], (2504 ^ _384323) ^ [_471931] : [-(aElementOf0(_471931, sdtlcdtrc0(xd, szDzozmdt0(xd)))), 2505 ^ _384323 : [(2506 ^ _384323) ^ [_472024] : [aElementOf0(_472024, szDzozmdt0(xd)), sdtlpdtrp0(xd, _472024) = _471931]]], (658 ^ _384323) ^ [_405346, _405348] : [aElementOf0(_405348, szNzAzT0), aElementOf0(_405346, szNzAzT0), szszuzczcdt0(_405348) = szszuzczcdt0(_405346), -(_405348 = _405346)], (1637 ^ _384323) ^ [] : [-(aSubsetOf0(sdtlcdtrc0(xc, szDzozmdt0(xc)), xT))], (2575 ^ _384323) ^ [_474168] : [-(aElementOf0(_474168, xO)), 2576 ^ _384323 : [(2577 ^ _384323) ^ [_474261] : [aElementOf0(_474261, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlpdtrp0(xe, _474261) = _474168]]], (282 ^ _384323) ^ [_393626] : [_393626 = slcrc0, 285 ^ _384323 : [(288 ^ _384323) ^ [_393807] : [aElementOf0(_393807, _393626)], (286 ^ _384323) ^ [] : [-(aSet0(_393626))]]], (2468 ^ _384323) ^ [_470593] : [aElementOf0(_470593, szNzAzT0), 2471 ^ _384323 : [(2472 ^ _384323) ^ [_470789] : [-(sdtlpdtrp0(xd, _470593) = sdtlpdtrp0(sdtlpdtrp0(xC, _470593), _470789)), aSet0(_470789), 2477 ^ _384323 : [(2478 ^ _384323) ^ [] : [2480 ^ _384323 : [(2485 ^ _384323) ^ [] : [aSubsetOf0(_470789, sdtlpdtrp0(xN, szszuzczcdt0(_470593)))], (2483 ^ _384323) ^ [] : [aElementOf0(2479 ^ [_470593, _470789], sdtlpdtrp0(xN, szszuzczcdt0(_470593)))], (2481 ^ _384323) ^ [] : [-(aElementOf0(2479 ^ [_470593, _470789], _470789))]], sbrdtbr0(_470789) = xk], (2489 ^ _384323) ^ [] : [aElementOf0(_470789, slbdtsldtrb0(sdtlpdtrp0(xN, szszuzczcdt0(_470593)), xk))]]]]], (196 ^ _384323) ^ [_390878, _390880, _390882, _390884] : [-(sdtlbdtrb0(_390884, _390880) = sdtlbdtrb0(_390882, _390878)), _390884 = _390882, _390880 = _390878], (1511 ^ _384323) ^ [_432551] : [aFunction0(_432551), 1514 ^ _384323 : [(1515 ^ _384323) ^ [_432739] : [aSubsetOf0(_432739, szDzozmdt0(_432551)), isCountable0(_432739), 1526 ^ _384323 : [(1529 ^ _384323) ^ [] : [-(aElementOf0(1525 ^ [_432551, _432739], szDzozmdt0(_432551)))], (1531 ^ _384323) ^ [] : [1524 ^ [_432551, _432739] = 1525 ^ [_432551, _432739]], (1533 ^ _384323) ^ [] : [-(sdtlpdtrp0(_432551, 1524 ^ [_432551, _432739]) = sdtlpdtrp0(_432551, 1525 ^ [_432551, _432739]))], (1527 ^ _384323) ^ [] : [-(aElementOf0(1524 ^ [_432551, _432739], szDzozmdt0(_432551)))]], -(isCountable0(sdtlcdtrc0(_432551, _432739)))]]], (721 ^ _384323) ^ [_407205, _407207] : [aElementOf0(_407207, szNzAzT0), aElementOf0(_407205, szNzAzT0), 728 ^ _384323 : [(735 ^ _384323) ^ [] : [sdtlseqdt0(szszuzczcdt0(_407207), szszuzczcdt0(_407205)), -(sdtlseqdt0(_407207, _407205))], (729 ^ _384323) ^ [] : [sdtlseqdt0(_407207, _407205), -(sdtlseqdt0(szszuzczcdt0(_407207), szszuzczcdt0(_407205)))]]], (2 ^ _384323) ^ [_384447] : [-(_384447 = _384447)], (1608 ^ _384323) ^ [] : [-(szDzozmdt0(xc) = slbdtsldtrb0(xS, xK))], (1393 ^ _384323) ^ [_428044, _428046] : [-(aSubsetOf0(sdtlbdtrb0(_428046, _428044), szDzozmdt0(_428046))), aFunction0(_428046), aElement0(_428044)], (646 ^ _384323) ^ [] : [-(isCountable0(szNzAzT0))], (268 ^ _384323) ^ [_393256] : [aSet0(_393256), isFinite0(_393256), true___, -(true___)], (44 ^ _384323) ^ [_385810, _385812] : [-(aElement0(_385810)), _385812 = _385810, aElement0(_385812)], (588 ^ _384323) ^ [_403183] : [aElement0(_403183), 591 ^ _384323 : [(592 ^ _384323) ^ [_403320] : [-(isCountable0(sdtpldt0(_403320, _403183))), aSet0(_403320), isCountable0(_403320)]]], (1158 ^ _384323) ^ [_420310, _420312] : [aSet0(_420312), aElementOf0(_420310, szNzAzT0), 1165 ^ _384323 : [(1166 ^ _384323) ^ [_420590] : [_420590 = slbdtsldtrb0(_420312, _420310), 1169 ^ _384323 : [(1180 ^ _384323) ^ [_421113] : [-(aElementOf0(_421113, _420590)), aSubsetOf0(_421113, _420312), sbrdtbr0(_421113) = _420310], (1172 ^ _384323) ^ [_420850] : [aElementOf0(_420850, _420590), 1175 ^ _384323 : [(1178 ^ _384323) ^ [] : [-(sbrdtbr0(_420850) = _420310)], (1176 ^ _384323) ^ [] : [-(aSubsetOf0(_420850, _420312))]]], (1170 ^ _384323) ^ [] : [-(aSet0(_420590))]]], (1190 ^ _384323) ^ [_421403] : [-(_421403 = slbdtsldtrb0(_420312, _420310)), aSet0(_421403), 1206 ^ _384323 : [(1211 ^ _384323) ^ [] : [aElementOf0(1195 ^ [_420310, _420312, _421403], _421403)], (1209 ^ _384323) ^ [] : [-(sbrdtbr0(1195 ^ [_420310, _420312, _421403]) = _420310)], (1207 ^ _384323) ^ [] : [-(aSubsetOf0(1195 ^ [_420310, _420312, _421403], _420312))]], 1198 ^ _384323 : [(1201 ^ _384323) ^ [] : [aSubsetOf0(1195 ^ [_420310, _420312, _421403], _420312), sbrdtbr0(1195 ^ [_420310, _420312, _421403]) = _420310], (1199 ^ _384323) ^ [] : [-(aElementOf0(1195 ^ [_420310, _420312, _421403], _421403))]]]]], (317 ^ _384323) ^ [_394598] : [isFinite0(_394598), aSet0(_394598), isCountable0(_394598)], (168 ^ _384323) ^ [_389837, _389839] : [_389839 = _389837, -(szmzizndt0(_389839) = szmzizndt0(_389837))], (574 ^ _384323) ^ [_402796, _402798] : [aElement0(_402798), aSet0(_402796), -(aElementOf0(_402798, _402796)), -(sdtmndt0(sdtpldt0(_402796, _402798), _402798) = _402796)], (4 ^ _384323) ^ [_384554, _384556] : [_384556 = _384554, -(_384554 = _384556)], (2524 ^ _384323) ^ [] : [-(aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd))))], (2495 ^ _384323) ^ [_471631] : [aElementOf0(_471631, sdtlcdtrc0(xd, szDzozmdt0(xd))), 2499 ^ _384323 : [(2502 ^ _384323) ^ [] : [-(sdtlpdtrp0(xd, 2498 ^ [_471631]) = _471631)], (2500 ^ _384323) ^ [] : [-(aElementOf0(2498 ^ [_471631], szDzozmdt0(xd)))]]], (2526 ^ _384323) ^ [_472644] : [aElementOf0(_472644, sdtlbdtrb0(xd, szDzizrdt0(xd))), 2529 ^ _384323 : [(2532 ^ _384323) ^ [] : [-(sdtlpdtrp0(xd, _472644) = szDzizrdt0(xd))], (2530 ^ _384323) ^ [] : [-(aElementOf0(_472644, szDzozmdt0(xd)))]]], (1555 ^ _384323) ^ [] : [-(isFinite0(xT))], (887 ^ _384323) ^ [_411874] : [aSet0(_411874), 890 ^ _384323 : [(891 ^ _384323) ^ [_412019] : [-(szszuzczcdt0(sbrdtbr0(sdtmndt0(_411874, _412019))) = sbrdtbr0(_411874)), isFinite0(_411874), aElementOf0(_412019, _411874)]]], (644 ^ _384323) ^ [] : [-(aSet0(szNzAzT0))], (126 ^ _384323) ^ [_388324, _388326] : [_388326 = _388324, -(szmzazxdt0(_388326) = szmzazxdt0(_388324))], (747 ^ _384323) ^ [_407948] : [aElementOf0(_407948, szNzAzT0), -(sdtlseqdt0(_407948, _407948))], (206 ^ _384323) ^ [_391209, _391211] : [_391211 = _391209, -(szDzizrdt0(_391211) = szDzizrdt0(_391209))], (869 ^ _384323) ^ [_411331] : [aSet0(_411331), isFinite0(_411331), 876 ^ _384323 : [(877 ^ _384323) ^ [_411561] : [aElement0(_411561), -(aElementOf0(_411561, _411331)), -(sbrdtbr0(sdtpldt0(_411331, _411561)) = szszuzczcdt0(sbrdtbr0(_411331)))]]], (20 ^ _384323) ^ [_385071, _385073] : [-(isFinite0(_385071)), _385073 = _385071, isFinite0(_385073)], (2026 ^ _384323) ^ [] : [-(szDzozmdt0(xC) = szNzAzT0)], (1215 ^ _384323) ^ [_422252] : [aSet0(_422252), isFinite0(_422252), 1222 ^ _384323 : [(1223 ^ _384323) ^ [_422468] : [aElementOf0(_422468, szNzAzT0), -(isFinite0(slbdtsldtrb0(_422252, _422468)))]]], (793 ^ _384323) ^ [_409237, _409239] : [aElementOf0(_409239, szNzAzT0), aElementOf0(_409237, szNzAzT0), -(sdtlseqdt0(_409239, _409237)), -(sdtlseqdt0(szszuzczcdt0(_409237), _409239))], (2566 ^ _384323) ^ [_473868] : [aElementOf0(_473868, xO), 2570 ^ _384323 : [(2573 ^ _384323) ^ [] : [-(sdtlpdtrp0(xe, 2569 ^ [_473868]) = _473868)], (2571 ^ _384323) ^ [] : [-(aElementOf0(2569 ^ [_473868], sdtlbdtrb0(xd, szDzizrdt0(xd))))]]], (2446 ^ _384323) ^ [] : [-(aFunction0(xe))], (753 ^ _384323) ^ [_408152, _408154] : [aElementOf0(_408154, szNzAzT0), aElementOf0(_408152, szNzAzT0), -(_408154 = _408152), sdtlseqdt0(_408154, _408152), sdtlseqdt0(_408152, _408154)], (1537 ^ _384323) ^ [_433611] : [aFunction0(_433611), 1548 ^ _384323 : [(1551 ^ _384323) ^ [] : [-(isCountable0(sdtlbdtrb0(_433611, szDzizrdt0(_433611))))], (1549 ^ _384323) ^ [] : [-(aElement0(szDzizrdt0(_433611)))]], isCountable0(szDzozmdt0(_433611)), isFinite0(sdtlcdtrc0(_433611, szDzozmdt0(_433611)))], (1006 ^ _384323) ^ [_415710, _415712] : [-(szmzizndt0(_415712) = szmzizndt0(_415710)), aElementOf0(szmzizndt0(_415712), _415710), aElementOf0(szmzizndt0(_415710), _415712), aSubsetOf0(_415712, szNzAzT0), aSubsetOf0(_415710, szNzAzT0), -(_415712 = slcrc0), -(_415710 = slcrc0)], (1152 ^ _384323) ^ [_420098] : [aElementOf0(_420098, szNzAzT0), -(sbrdtbr0(slbdtrb0(_420098)) = _420098)], (158 ^ _384323) ^ [_389506, _389508, _389510, _389512] : [-(sdtmndt0(_389512, _389508) = sdtmndt0(_389510, _389506)), _389512 = _389510, _389508 = _389506]], input).
% 48.27/46.95  ncf('1',plain,[-(xQ = slcrc0)],start(2634 ^ 0)).
% 48.27/46.95  ncf('1.1',plain,[xQ = slcrc0, 863 : -(sbrdtbr0(xQ) = sz00), 863 : aSet0(xQ)],extension(853 ^ 1,bind([[_410897], [xQ]]))).
% 48.27/46.95  ncf('1.1.1',plain,[sbrdtbr0(xQ) = sz00, -(xK = sz00), xK = sbrdtbr0(xQ)],extension(10 ^ 4,bind([[_384758, _384760, _384762], [sz00, sbrdtbr0(xQ), xK]]))).
% 48.27/46.95  ncf('1.1.1.1',plain,[xK = sz00],extension(1775 ^ 5)).
% 48.27/46.95  ncf('1.1.1.2',plain,[-(xK = sbrdtbr0(xQ)), sbrdtbr0(xQ) = xK],extension(4 ^ 5,bind([[_384554, _384556], [xK, sbrdtbr0(xQ)]]))).
% 48.27/46.95  ncf('1.1.1.2.1',plain,[-(sbrdtbr0(xQ) = xK)],extension(2628 ^ 6)).
% 48.27/46.95  ncf('1.1.2',plain,[-(aSet0(xQ)), 341 : aSubsetOf0(xQ, xO), 341 : aSet0(xO)],extension(337 ^ 2,bind([[_395140, _395316], [xO, xQ]]))).
% 48.27/46.95  ncf('1.1.2.1',plain,[-(aSubsetOf0(xQ, xO))],extension(2626 ^ 5)).
% 48.27/46.95  ncf('1.1.2.2',plain,[-(aSet0(xO)), 341 : aSubsetOf0(xO, xS), 341 : aSet0(xS)],extension(337 ^ 3,bind([[_395140, _395316], [xS, xO]]))).
% 48.27/46.95  ncf('1.1.2.2.1',plain,[-(aSubsetOf0(xO, xS))],extension(2616 ^ 6)).
% 48.27/46.95  ncf('1.1.2.2.2',plain,[-(aSet0(xS))],extension(1559 ^ 4)).
% 48.27/46.95  %-----------------------------------------------------
% 48.27/46.95  End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------