%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM539+2 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n029.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:44:56 EDT 2023
% Result : Theorem 0.36s 1.38s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM539+2 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n029.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 18 17:28:58 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.36/1.38
% 0.36/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.36/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.38 %-----------------------------------------------------
% 0.36/1.38 ncf(matrix, plain, [(987 ^ _114971) ^ [] : [-(aElementOf0(985 ^ [], xT))], (989 ^ _114971) ^ [] : [sdtlseqdt0(szmzizndt0(xS), 985 ^ [])], (991 ^ _114971) ^ [] : [szmzizndt0(xS) = szmzizndt0(xT)], (978 ^ _114971) ^ [] : [-(aElementOf0(szmzizndt0(xS), xS))], (980 ^ _114971) ^ [_145440] : [aElementOf0(_145440, xS), -(sdtlseqdt0(szmzizndt0(xS), _145440))], (116 ^ _114971) ^ [_118723, _118725, _118727, _118729] : [-(sdtpldt0(_118729, _118725) = sdtpldt0(_118727, _118723)), _118729 = _118727, _118725 = _118723], (126 ^ _114971) ^ [_119054, _119056] : [_119056 = _119054, -(szszuzczcdt0(_119056) = szszuzczcdt0(_119054))], (132 ^ _114971) ^ [_119300, _119302, _119304, _119306] : [-(sdtmndt0(_119306, _119302) = sdtmndt0(_119304, _119300)), _119306 = _119304, _119302 = _119300], (142 ^ _114971) ^ [_119631, _119633] : [_119633 = _119631, -(sbrdtbr0(_119633) = sbrdtbr0(_119631))], (148 ^ _114971) ^ [_119849, _119851] : [_119851 = _119849, -(szmzazxdt0(_119851) = szmzazxdt0(_119849))], (154 ^ _114971) ^ [_120047, _120049] : [_120049 = _120047, -(szmzizndt0(_120049) = szmzizndt0(_120047))], (2 ^ _114971) ^ [_115115] : [-(_115115 = _115115)], (4 ^ _114971) ^ [_115222, _115224] : [_115224 = _115222, -(_115222 = _115224)], (10 ^ _114971) ^ [_115426, _115428, _115430] : [-(_115430 = _115426), _115430 = _115428, _115428 = _115426], (20 ^ _114971) ^ [_115739, _115741] : [-(isCountable0(_115739)), _115741 = _115739, isCountable0(_115741)], (30 ^ _114971) ^ [_116062, _116064, _116066, _116068] : [-(iLess0(_116066, _116062)), iLess0(_116068, _116064), _116068 = _116066, _116064 = _116062], (44 ^ _114971) ^ [_116478, _116480] : [-(aElement0(_116478)), _116480 = _116478, aElement0(_116480)], (54 ^ _114971) ^ [_116773, _116775] : [-(isFinite0(_116773)), _116775 = _116773, isFinite0(_116775)], (64 ^ _114971) ^ [_117068, _117070] : [-(aSet0(_117068)), _117070 = _117068, aSet0(_117070)], (74 ^ _114971) ^ [_117391, _117393, _117395, _117397] : [-(aSubsetOf0(_117395, _117391)), aSubsetOf0(_117397, _117393), _117397 = _117395, _117393 = _117391], (88 ^ _114971) ^ [_117835, _117837, _117839, _117841] : [-(aElementOf0(_117839, _117835)), aElementOf0(_117841, _117837), _117841 = _117839, _117837 = _117835], (102 ^ _114971) ^ [_118259, _118261, _118263, _118265] : [-(sdtlseqdt0(_118263, _118259)), sdtlseqdt0(_118265, _118261), _118265 = _118263, _118261 = _118259], (160 ^ _114971) ^ [_120273] : [aSet0(_120273), true___, -(true___)], (170 ^ _114971) ^ [_120528] : [aElement0(_120528), true___, -(true___)], (180 ^ _114971) ^ [_120783] : [aSet0(_120783), 183 ^ _114971 : [(184 ^ _114971) ^ [_120913] : [aElementOf0(_120913, _120783), -(aElement0(_120913))]]], (190 ^ _114971) ^ [_121114] : [aSet0(_121114), isFinite0(_121114), true___, -(true___)], (204 ^ _114971) ^ [_121484] : [_121484 = slcrc0, 207 ^ _114971 : [(208 ^ _114971) ^ [] : [-(aSet0(_121484))], (210 ^ _114971) ^ [_121665] : [aElementOf0(_121665, _121484)]]], (212 ^ _114971) ^ [_121733] : [-(_121733 = slcrc0), aSet0(_121733), -(aElementOf0(217 ^ [_121733], _121733))], (223 ^ _114971) ^ [] : [-(isFinite0(slcrc0))], (225 ^ _114971) ^ [_122115] : [aSet0(_122115), isCountable0(_122115), true___, -(true___)], (239 ^ _114971) ^ [_122456] : [isFinite0(_122456), aSet0(_122456), isCountable0(_122456)], (249 ^ _114971) ^ [_122726] : [_122726 = slcrc0, aSet0(_122726), isCountable0(_122726)], (259 ^ _114971) ^ [_122998] : [aSet0(_122998), 262 ^ _114971 : [(263 ^ _114971) ^ [_123174] : [aSubsetOf0(_123174, _122998), 266 ^ _114971 : [(267 ^ _114971) ^ [] : [-(aSet0(_123174))], (269 ^ _114971) ^ [_123383] : [aElementOf0(_123383, _123174), -(aElementOf0(_123383, _122998))]]], (275 ^ _114971) ^ [_123562] : [-(aSubsetOf0(_123562, _122998)), aSet0(_123562), 281 ^ _114971 : [(282 ^ _114971) ^ [] : [-(aElementOf0(280 ^ [_122998, _123562], _123562))], (284 ^ _114971) ^ [] : [aElementOf0(280 ^ [_122998, _123562], _122998)]]]]], (288 ^ _114971) ^ [_123999] : [aSet0(_123999), isFinite0(_123999), 295 ^ _114971 : [(296 ^ _114971) ^ [_124212] : [aSubsetOf0(_124212, _123999), -(isFinite0(_124212))]]], (302 ^ _114971) ^ [_124415] : [aSet0(_124415), -(aSubsetOf0(_124415, _124415))], (308 ^ _114971) ^ [_124617, _124619] : [aSet0(_124619), aSet0(_124617), -(_124619 = _124617), aSubsetOf0(_124619, _124617), aSubsetOf0(_124617, _124619)], (326 ^ _114971) ^ [_125106, _125108, _125110] : [aSet0(_125110), aSet0(_125108), aSet0(_125106), -(aSubsetOf0(_125110, _125106)), aSubsetOf0(_125110, _125108), aSubsetOf0(_125108, _125106)], (348 ^ _114971) ^ [_125692, _125694] : [aSet0(_125694), aElement0(_125692), 355 ^ _114971 : [(386 ^ _114971) ^ [_126953] : [-(_126953 = sdtpldt0(_125694, _125692)), aSet0(_126953), 394 ^ _114971 : [(395 ^ _114971) ^ [] : [-(aElementOf0(391 ^ [_125692, _125694, _126953], _126953))], (397 ^ _114971) ^ [] : [aElement0(391 ^ [_125692, _125694, _126953]), 400 ^ _114971 : [(401 ^ _114971) ^ [] : [aElementOf0(391 ^ [_125692, _125694, _126953], _125694)], (403 ^ _114971) ^ [] : [391 ^ [_125692, _125694, _126953] = _125692]]]], 404 ^ _114971 : [(413 ^ _114971) ^ [] : [aElementOf0(391 ^ [_125692, _125694, _126953], _126953)], (405 ^ _114971) ^ [] : [-(aElement0(391 ^ [_125692, _125694, _126953]))], (407 ^ _114971) ^ [] : [-(aElementOf0(391 ^ [_125692, _125694, _126953], _125694)), -(391 ^ [_125692, _125694, _126953] = _125692)]]], (356 ^ _114971) ^ [_125973] : [_125973 = sdtpldt0(_125694, _125692), 359 ^ _114971 : [(360 ^ _114971) ^ [] : [-(aSet0(_125973))], (362 ^ _114971) ^ [_126236] : [aElementOf0(_126236, _125973), 365 ^ _114971 : [(366 ^ _114971) ^ [] : [-(aElement0(_126236))], (368 ^ _114971) ^ [] : [-(aElementOf0(_126236, _125694)), -(_126236 = _125692)]]], (374 ^ _114971) ^ [_126591] : [-(aElementOf0(_126591, _125973)), aElement0(_126591), 379 ^ _114971 : [(380 ^ _114971) ^ [] : [aElementOf0(_126591, _125694)], (382 ^ _114971) ^ [] : [_126591 = _125692]]]]]]], (417 ^ _114971) ^ [_127990, _127992] : [aSet0(_127992), aElement0(_127990), 424 ^ _114971 : [(455 ^ _114971) ^ [_129258] : [-(_129258 = sdtmndt0(_127992, _127990)), aSet0(_129258), 475 ^ _114971 : [(476 ^ _114971) ^ [] : [-(aElement0(460 ^ [_127990, _127992, _129258]))], (478 ^ _114971) ^ [] : [-(aElementOf0(460 ^ [_127990, _127992, _129258], _127992))], (480 ^ _114971) ^ [] : [460 ^ [_127990, _127992, _129258] = _127990], (482 ^ _114971) ^ [] : [aElementOf0(460 ^ [_127990, _127992, _129258], _129258)]], 463 ^ _114971 : [(464 ^ _114971) ^ [] : [-(aElementOf0(460 ^ [_127990, _127992, _129258], _129258))], (466 ^ _114971) ^ [] : [aElement0(460 ^ [_127990, _127992, _129258]), aElementOf0(460 ^ [_127990, _127992, _129258], _127992), -(460 ^ [_127990, _127992, _129258] = _127990)]]], (425 ^ _114971) ^ [_128273] : [_128273 = sdtmndt0(_127992, _127990), 428 ^ _114971 : [(429 ^ _114971) ^ [] : [-(aSet0(_128273))], (431 ^ _114971) ^ [_128538] : [aElementOf0(_128538, _128273), 434 ^ _114971 : [(435 ^ _114971) ^ [] : [-(aElement0(_128538))], (437 ^ _114971) ^ [] : [-(aElementOf0(_128538, _127992))], (439 ^ _114971) ^ [] : [_128538 = _127990]]], (441 ^ _114971) ^ [_128874] : [-(aElementOf0(_128874, _128273)), aElement0(_128874), aElementOf0(_128874, _127992), -(_128874 = _127990)]]]]], (486 ^ _114971) ^ [_130288] : [aSet0(_130288), 489 ^ _114971 : [(490 ^ _114971) ^ [_130425] : [aElementOf0(_130425, _130288), -(sdtpldt0(sdtmndt0(_130288, _130425), _130425) = _130288)]]], (496 ^ _114971) ^ [_130654, _130656] : [aElement0(_130656), aSet0(_130654), -(aElementOf0(_130656, _130654)), -(sdtmndt0(sdtpldt0(_130654, _130656), _130656) = _130654)], (510 ^ _114971) ^ [_131041] : [aElement0(_131041), 513 ^ _114971 : [(514 ^ _114971) ^ [_131178] : [-(isCountable0(sdtpldt0(_131178, _131041))), aSet0(_131178), isCountable0(_131178)]]], (524 ^ _114971) ^ [_131470] : [aElement0(_131470), 527 ^ _114971 : [(528 ^ _114971) ^ [_131607] : [-(isCountable0(sdtmndt0(_131607, _131470))), aSet0(_131607), isCountable0(_131607)]]], (538 ^ _114971) ^ [_131899] : [aElement0(_131899), 541 ^ _114971 : [(542 ^ _114971) ^ [_132036] : [-(isFinite0(sdtpldt0(_132036, _131899))), aSet0(_132036), isFinite0(_132036)]]], (552 ^ _114971) ^ [_132328] : [aElement0(_132328), 555 ^ _114971 : [(556 ^ _114971) ^ [_132465] : [-(isFinite0(sdtmndt0(_132465, _132328))), aSet0(_132465), isFinite0(_132465)]]], (566 ^ _114971) ^ [] : [-(aSet0(szNzAzT0))], (568 ^ _114971) ^ [] : [-(isCountable0(szNzAzT0))], (570 ^ _114971) ^ [] : [-(aElementOf0(sz00, szNzAzT0))], (572 ^ _114971) ^ [_132918] : [aElementOf0(_132918, szNzAzT0), 575 ^ _114971 : [(576 ^ _114971) ^ [] : [-(aElementOf0(szszuzczcdt0(_132918), szNzAzT0))], (578 ^ _114971) ^ [] : [szszuzczcdt0(_132918) = sz00]]], (580 ^ _114971) ^ [_133204, _133206] : [aElementOf0(_133206, szNzAzT0), aElementOf0(_133204, szNzAzT0), szszuzczcdt0(_133206) = szszuzczcdt0(_133204), -(_133206 = _133204)], (594 ^ _114971) ^ [_133588] : [aElementOf0(_133588, szNzAzT0), -(_133588 = sz00), 602 ^ _114971 : [(603 ^ _114971) ^ [] : [-(aElementOf0(601 ^ [_133588], szNzAzT0))], (605 ^ _114971) ^ [] : [-(_133588 = szszuzczcdt0(601 ^ [_133588]))]]], (607 ^ _114971) ^ [_134005] : [aElementOf0(_134005, szNzAzT0), _134005 = szszuzczcdt0(_134005)], (613 ^ _114971) ^ [_134214, _134216] : [aElementOf0(_134216, szNzAzT0), aElementOf0(_134214, szNzAzT0), sdtlseqdt0(_134216, _134214), true___, -(true___)], (631 ^ _114971) ^ [_134664] : [aElementOf0(_134664, szNzAzT0), -(sdtlseqdt0(sz00, _134664))], (637 ^ _114971) ^ [_134854] : [aElementOf0(_134854, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_134854), sz00)], (643 ^ _114971) ^ [_135063, _135065] : [aElementOf0(_135065, szNzAzT0), aElementOf0(_135063, szNzAzT0), 650 ^ _114971 : [(651 ^ _114971) ^ [] : [sdtlseqdt0(_135065, _135063), -(sdtlseqdt0(szszuzczcdt0(_135065), szszuzczcdt0(_135063)))], (657 ^ _114971) ^ [] : [sdtlseqdt0(szszuzczcdt0(_135065), szszuzczcdt0(_135063)), -(sdtlseqdt0(_135065, _135063))]]], (663 ^ _114971) ^ [_135612] : [aElementOf0(_135612, szNzAzT0), -(sdtlseqdt0(_135612, szszuzczcdt0(_135612)))], (669 ^ _114971) ^ [_135806] : [aElementOf0(_135806, szNzAzT0), -(sdtlseqdt0(_135806, _135806))], (675 ^ _114971) ^ [_136010, _136012] : [aElementOf0(_136012, szNzAzT0), aElementOf0(_136010, szNzAzT0), -(_136012 = _136010), sdtlseqdt0(_136012, _136010), sdtlseqdt0(_136010, _136012)], (693 ^ _114971) ^ [_136503, _136505, _136507] : [aElementOf0(_136507, szNzAzT0), aElementOf0(_136505, szNzAzT0), aElementOf0(_136503, szNzAzT0), -(sdtlseqdt0(_136507, _136503)), sdtlseqdt0(_136507, _136505), sdtlseqdt0(_136505, _136503)], (715 ^ _114971) ^ [_137095, _137097] : [aElementOf0(_137097, szNzAzT0), aElementOf0(_137095, szNzAzT0), -(sdtlseqdt0(_137097, _137095)), -(sdtlseqdt0(szszuzczcdt0(_137095), _137097))], (729 ^ _114971) ^ [_137490, _137492] : [aElementOf0(_137492, szNzAzT0), aElementOf0(_137490, szNzAzT0), iLess0(_137492, _137490), true___, -(true___)], (747 ^ _114971) ^ [_137940] : [aElementOf0(_137940, szNzAzT0), -(iLess0(_137940, szszuzczcdt0(_137940)))], (753 ^ _114971) ^ [_138134] : [aSet0(_138134), -(aElement0(sbrdtbr0(_138134)))], (759 ^ _114971) ^ [_138324] : [aSet0(_138324), 762 ^ _114971 : [(763 ^ _114971) ^ [] : [aElementOf0(sbrdtbr0(_138324), szNzAzT0), -(isFinite0(_138324))], (769 ^ _114971) ^ [] : [isFinite0(_138324), -(aElementOf0(sbrdtbr0(_138324), szNzAzT0))]]], (775 ^ _114971) ^ [_138755] : [aSet0(_138755), 778 ^ _114971 : [(779 ^ _114971) ^ [] : [sbrdtbr0(_138755) = sz00, -(_138755 = slcrc0)], (785 ^ _114971) ^ [] : [_138755 = slcrc0, -(sbrdtbr0(_138755) = sz00)]]], (791 ^ _114971) ^ [_139189] : [aSet0(_139189), isFinite0(_139189), 798 ^ _114971 : [(799 ^ _114971) ^ [_139419] : [aElement0(_139419), -(aElementOf0(_139419, _139189)), -(sbrdtbr0(sdtpldt0(_139189, _139419)) = szszuzczcdt0(sbrdtbr0(_139189)))]]], (809 ^ _114971) ^ [_139732] : [aSet0(_139732), 812 ^ _114971 : [(813 ^ _114971) ^ [_139877] : [-(szszuzczcdt0(sbrdtbr0(sdtmndt0(_139732, _139877))) = sbrdtbr0(_139732)), isFinite0(_139732), aElementOf0(_139877, _139732)]]], (823 ^ _114971) ^ [_140185] : [aSet0(_140185), 826 ^ _114971 : [(827 ^ _114971) ^ [_140325] : [-(sdtlseqdt0(sbrdtbr0(_140325), sbrdtbr0(_140185))), isFinite0(_140185), aSubsetOf0(_140325, _140185)]]], (837 ^ _114971) ^ [_140637, _140639] : [aSet0(_140639), aElementOf0(_140637, szNzAzT0), 853 ^ _114971 : [(854 ^ _114971) ^ [] : [-(aSubsetOf0(852 ^ [_140637, _140639], _140639))], (856 ^ _114971) ^ [] : [-(sbrdtbr0(852 ^ [_140637, _140639]) = _140637)]], isFinite0(_140639), sdtlseqdt0(_140637, sbrdtbr0(_140639))], (858 ^ _114971) ^ [_141253] : [aSubsetOf0(_141253, szNzAzT0), -(_141253 = slcrc0), 865 ^ _114971 : [(866 ^ _114971) ^ [_141522] : [_141522 = szmzizndt0(_141253), 869 ^ _114971 : [(870 ^ _114971) ^ [] : [-(aElementOf0(_141522, _141253))], (872 ^ _114971) ^ [_141737] : [aElementOf0(_141737, _141253), -(sdtlseqdt0(_141522, _141737))]]], (878 ^ _114971) ^ [_141916] : [-(_141916 = szmzizndt0(_141253)), aElementOf0(_141916, _141253), 884 ^ _114971 : [(885 ^ _114971) ^ [] : [-(aElementOf0(883 ^ [_141253, _141916], _141253))], (887 ^ _114971) ^ [] : [sdtlseqdt0(_141916, 883 ^ [_141253, _141916])]]]]], (891 ^ _114971) ^ [_142361] : [aSubsetOf0(_142361, szNzAzT0), isFinite0(_142361), -(_142361 = slcrc0), 902 ^ _114971 : [(903 ^ _114971) ^ [_142713] : [_142713 = szmzazxdt0(_142361), 906 ^ _114971 : [(907 ^ _114971) ^ [] : [-(aElementOf0(_142713, _142361))], (909 ^ _114971) ^ [_142928] : [aElementOf0(_142928, _142361), -(sdtlseqdt0(_142928, _142713))]]], (915 ^ _114971) ^ [_143107] : [-(_143107 = szmzazxdt0(_142361)), aElementOf0(_143107, _142361), 921 ^ _114971 : [(922 ^ _114971) ^ [] : [-(aElementOf0(920 ^ [_142361, _143107], _142361))], (924 ^ _114971) ^ [] : [sdtlseqdt0(920 ^ [_142361, _143107], _143107)]]]]], (928 ^ _114971) ^ [] : [-(aSet0(xS))], (930 ^ _114971) ^ [_143627] : [aElementOf0(_143627, xS), -(aElementOf0(_143627, szNzAzT0))], (936 ^ _114971) ^ [] : [-(aSubsetOf0(xS, szNzAzT0))], (938 ^ _114971) ^ [] : [-(aSet0(xT))], (946 ^ _114971) ^ [] : [-(aSubsetOf0(xT, szNzAzT0))], (949 ^ _114971) ^ [] : [-(aElementOf0(947 ^ [], xS))], (951 ^ _114971) ^ [] : [xS = slcrc0], (954 ^ _114971) ^ [] : [-(aElementOf0(952 ^ [], xT))], (956 ^ _114971) ^ [] : [xT = slcrc0], (940 ^ _114971) ^ [_143923] : [aElementOf0(_143923, xT), -(aElementOf0(_143923, szNzAzT0))], (958 ^ _114971) ^ [] : [-(aElementOf0(szmzizndt0(xS), xS))], (960 ^ _114971) ^ [_144511] : [aElementOf0(_144511, xS), -(sdtlseqdt0(szmzizndt0(xS), _144511))], (966 ^ _114971) ^ [] : [-(aElementOf0(szmzizndt0(xS), xT))], (968 ^ _114971) ^ [] : [-(aElementOf0(szmzizndt0(xT), xT))], (976 ^ _114971) ^ [] : [-(aElementOf0(szmzizndt0(xT), xS))], (970 ^ _114971) ^ [_144807] : [aElementOf0(_144807, xT), -(sdtlseqdt0(szmzizndt0(xT), _144807))]], input).
% 0.36/1.38 ncf('1',plain,[szmzizndt0(xS) = szmzizndt0(xT)],start(991 ^ 0)).
% 0.36/1.38 ncf('1.1',plain,[-(szmzizndt0(xS) = szmzizndt0(xT)), aElementOf0(szmzizndt0(xS), szNzAzT0), aElementOf0(szmzizndt0(xT), szNzAzT0), sdtlseqdt0(szmzizndt0(xS), szmzizndt0(xT)), sdtlseqdt0(szmzizndt0(xT), szmzizndt0(xS))],extension(675 ^ 1,bind([[_136010, _136012], [szmzizndt0(xT), szmzizndt0(xS)]]))).
% 0.36/1.38 ncf('1.1.1',plain,[-(aElementOf0(szmzizndt0(xS), szNzAzT0)), 269 : aElementOf0(szmzizndt0(xS), xS), 269 : aSubsetOf0(xS, szNzAzT0), 263 : aSet0(szNzAzT0)],extension(259 ^ 2,bind([[_122998, _123174, _123383], [szNzAzT0, xS, szmzizndt0(xS)]]))).
% 0.36/1.38 ncf('1.1.1.1',plain,[-(aElementOf0(szmzizndt0(xS), xS))],extension(978 ^ 7)).
% 0.36/1.38 ncf('1.1.1.2',plain,[-(aSubsetOf0(xS, szNzAzT0))],extension(936 ^ 5)).
% 0.36/1.38 ncf('1.1.1.3',plain,[-(aSet0(szNzAzT0))],extension(566 ^ 3)).
% 0.36/1.38 ncf('1.1.2',plain,[-(aElementOf0(szmzizndt0(xT), szNzAzT0)), 269 : aElementOf0(szmzizndt0(xT), xT), 269 : aSubsetOf0(xT, szNzAzT0), 263 : aSet0(szNzAzT0)],extension(259 ^ 2,bind([[_122998, _123174, _123383], [szNzAzT0, xT, szmzizndt0(xT)]]))).
% 0.36/1.38 ncf('1.1.2.1',plain,[-(aElementOf0(szmzizndt0(xT), xT))],extension(968 ^ 7)).
% 0.36/1.38 ncf('1.1.2.2',plain,[-(aSubsetOf0(xT, szNzAzT0))],extension(946 ^ 5)).
% 0.36/1.38 ncf('1.1.2.3',plain,[-(aSet0(szNzAzT0))],extension(566 ^ 3)).
% 0.36/1.38 ncf('1.1.3',plain,[-(sdtlseqdt0(szmzizndt0(xS), szmzizndt0(xT))), aElementOf0(szmzizndt0(xT), xS)],extension(980 ^ 2,bind([[_145440], [szmzizndt0(xT)]]))).
% 0.36/1.38 ncf('1.1.3.1',plain,[-(aElementOf0(szmzizndt0(xT), xS))],extension(976 ^ 3)).
% 0.36/1.38 ncf('1.1.4',plain,[-(sdtlseqdt0(szmzizndt0(xT), szmzizndt0(xS))), aElementOf0(szmzizndt0(xS), xT)],extension(970 ^ 2,bind([[_144807], [szmzizndt0(xS)]]))).
% 0.36/1.38 ncf('1.1.4.1',plain,[-(aElementOf0(szmzizndt0(xS), xT))],extension(966 ^ 3)).
% 0.36/1.38 %-----------------------------------------------------
% 0.36/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------