%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM538+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n002.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 166.85s 161.72s
% Output : Proof 166.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM538+1 : TPTP v8.1.2. Released v4.0.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n002.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:33:34 EDT 2023
% 0.12/0.33 % CPUTime :
% 166.85/161.72
% 166.85/161.72 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 166.85/161.72 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 166.85/161.72 %-----------------------------------------------------
% 166.85/161.72 ncf(matrix, plain, [(803 ^ _123446) ^ [] : [szszuzczcdt0(sbrdtbr0(sdtmndt0(xS, xx))) = sbrdtbr0(xS)], !, (601 ^ _98814) ^ [_117593, _117595] : [aElementOf0(_117595, szNzAzT0), aElementOf0(_117593, szNzAzT0), sdtlseqdt0(_117595, _117593), true___, -(true___)], (276 ^ _98814) ^ [_107378] : [aSet0(_107378), isFinite0(_107378), 283 ^ _98814 : [(284 ^ _98814) ^ [_107591] : [aSubsetOf0(_107591, _107378), -(isFinite0(_107591))]]], (142 ^ _98814) ^ [_103434, _103436] : [_103436 = _103434, -(sbrdtbr0(_103436) = sbrdtbr0(_103434))], (526 ^ _98814) ^ [_115278] : [aElement0(_115278), 529 ^ _98814 : [(530 ^ _98814) ^ [_115415] : [-(isFinite0(sdtpldt0(_115415, _115278))), aSet0(_115415), isFinite0(_115415)]]], (211 ^ _98814) ^ [] : [-(isFinite0(slcrc0))], (568 ^ _98814) ^ [_116583, _116585] : [aElementOf0(_116585, szNzAzT0), aElementOf0(_116583, szNzAzT0), szszuzczcdt0(_116585) = szszuzczcdt0(_116583), -(_116585 = _116583)], (148 ^ _98814) ^ [_103652] : [aSet0(_103652), true___, -(true___)], (227 ^ _98814) ^ [_105835] : [isFinite0(_105835), aSet0(_105835), isCountable0(_105835)], (556 ^ _98814) ^ [] : [-(isCountable0(szNzAzT0))], (797 ^ _98814) ^ [] : [-(aSet0(xS))], (779 ^ _98814) ^ [_122568] : [aSet0(_122568), isFinite0(_122568), 786 ^ _98814 : [(787 ^ _98814) ^ [_122798] : [aElement0(_122798), -(aElementOf0(_122798, _122568)), -(sbrdtbr0(sdtpldt0(_122568, _122798)) = szszuzczcdt0(sbrdtbr0(_122568)))]]], (34 ^ _98814) ^ [_100006, _100008] : [-(isCountable0(_100006)), _100008 = _100006, isCountable0(_100008)], (44 ^ _98814) ^ [_100329, _100331, _100333, _100335] : [-(sdtlseqdt0(_100333, _100329)), sdtlseqdt0(_100335, _100331), _100335 = _100333, _100331 = _100329], (405 ^ _98814) ^ [_111369, _111371] : [aSet0(_111371), aElement0(_111369), 412 ^ _98814 : [(443 ^ _98814) ^ [_112637] : [-(_112637 = sdtmndt0(_111371, _111369)), aSet0(_112637), 463 ^ _98814 : [(464 ^ _98814) ^ [] : [-(aElement0(448 ^ [_111369, _111371, _112637]))], (470 ^ _98814) ^ [] : [aElementOf0(448 ^ [_111369, _111371, _112637], _112637)], (468 ^ _98814) ^ [] : [448 ^ [_111369, _111371, _112637] = _111369], (466 ^ _98814) ^ [] : [-(aElementOf0(448 ^ [_111369, _111371, _112637], _111371))]], 451 ^ _98814 : [(452 ^ _98814) ^ [] : [-(aElementOf0(448 ^ [_111369, _111371, _112637], _112637))], (454 ^ _98814) ^ [] : [aElement0(448 ^ [_111369, _111371, _112637]), aElementOf0(448 ^ [_111369, _111371, _112637], _111371), -(448 ^ [_111369, _111371, _112637] = _111369)]]], (413 ^ _98814) ^ [_111652] : [_111652 = sdtmndt0(_111371, _111369), 416 ^ _98814 : [(429 ^ _98814) ^ [_112253] : [-(aElementOf0(_112253, _111652)), aElement0(_112253), aElementOf0(_112253, _111371), -(_112253 = _111369)], (419 ^ _98814) ^ [_111917] : [aElementOf0(_111917, _111652), 422 ^ _98814 : [(427 ^ _98814) ^ [] : [_111917 = _111369], (425 ^ _98814) ^ [] : [-(aElementOf0(_111917, _111371))], (423 ^ _98814) ^ [] : [-(aElement0(_111917))]]], (417 ^ _98814) ^ [] : [-(aSet0(_111652))]]]]], (631 ^ _98814) ^ [_118442, _118444] : [aElementOf0(_118444, szNzAzT0), aElementOf0(_118442, szNzAzT0), 638 ^ _98814 : [(639 ^ _98814) ^ [] : [sdtlseqdt0(_118444, _118442), -(sdtlseqdt0(szszuzczcdt0(_118444), szszuzczcdt0(_118442)))], (645 ^ _98814) ^ [] : [sdtlseqdt0(szszuzczcdt0(_118444), szszuzczcdt0(_118442)), -(sdtlseqdt0(_118444, _118442))]]], (582 ^ _98814) ^ [_116967] : [aElementOf0(_116967, szNzAzT0), -(_116967 = sz00), 590 ^ _98814 : [(591 ^ _98814) ^ [] : [-(aElementOf0(589 ^ [_116967], szNzAzT0))], (593 ^ _98814) ^ [] : [-(_116967 = szszuzczcdt0(589 ^ [_116967]))]]], (619 ^ _98814) ^ [_118043] : [aElementOf0(_118043, szNzAzT0), -(sdtlseqdt0(sz00, _118043))], (10 ^ _98814) ^ [_99249, _99251, _99253] : [-(_99253 = _99249), _99253 = _99251, _99251 = _99249], (116 ^ _98814) ^ [_102546, _102548, _102550, _102552] : [-(sdtpldt0(_102552, _102548) = sdtpldt0(_102550, _102546)), _102552 = _102550, _102548 = _102546], (474 ^ _98814) ^ [_113667] : [aSet0(_113667), 477 ^ _98814 : [(478 ^ _98814) ^ [_113804] : [aElementOf0(_113804, _113667), -(sdtpldt0(sdtmndt0(_113667, _113804), _113804) = _113667)]]], (58 ^ _98814) ^ [_100773, _100775, _100777, _100779] : [-(iLess0(_100777, _100773)), iLess0(_100779, _100775), _100779 = _100777, _100775 = _100773], (168 ^ _98814) ^ [_104162] : [aSet0(_104162), 171 ^ _98814 : [(172 ^ _98814) ^ [_104292] : [aElementOf0(_104292, _104162), -(aElement0(_104292))]]], (799 ^ _98814) ^ [] : [-(isFinite0(xS))], (558 ^ _98814) ^ [] : [-(aElementOf0(sz00, szNzAzT0))], (512 ^ _98814) ^ [_114849] : [aElement0(_114849), 515 ^ _98814 : [(516 ^ _98814) ^ [_114986] : [-(isCountable0(sdtmndt0(_114986, _114849))), aSet0(_114986), isCountable0(_114986)]]], (554 ^ _98814) ^ [] : [-(aSet0(szNzAzT0))], (237 ^ _98814) ^ [_106105] : [_106105 = slcrc0, aSet0(_106105), isCountable0(_106105)], (158 ^ _98814) ^ [_103907] : [aElement0(_103907), true___, -(true___)], (72 ^ _98814) ^ [_101189, _101191] : [-(aElement0(_101189)), _101191 = _101189, aElement0(_101191)], (540 ^ _98814) ^ [_115707] : [aElement0(_115707), 543 ^ _98814 : [(544 ^ _98814) ^ [_115844] : [-(isFinite0(sdtmndt0(_115844, _115707))), aSet0(_115844), isFinite0(_115844)]]], (4 ^ _98814) ^ [_99045, _99047] : [_99047 = _99045, -(_99045 = _99047)], (735 ^ _98814) ^ [_121319] : [aElementOf0(_121319, szNzAzT0), -(iLess0(_121319, szszuzczcdt0(_121319)))], (336 ^ _98814) ^ [_109071, _109073] : [aSet0(_109073), aElement0(_109071), 343 ^ _98814 : [(374 ^ _98814) ^ [_110332] : [-(_110332 = sdtpldt0(_109073, _109071)), aSet0(_110332), 382 ^ _98814 : [(383 ^ _98814) ^ [] : [-(aElementOf0(379 ^ [_109071, _109073, _110332], _110332))], (385 ^ _98814) ^ [] : [aElement0(379 ^ [_109071, _109073, _110332]), 388 ^ _98814 : [(389 ^ _98814) ^ [] : [aElementOf0(379 ^ [_109071, _109073, _110332], _109073)], (391 ^ _98814) ^ [] : [379 ^ [_109071, _109073, _110332] = _109071]]]], 392 ^ _98814 : [(395 ^ _98814) ^ [] : [-(aElementOf0(379 ^ [_109071, _109073, _110332], _109073)), -(379 ^ [_109071, _109073, _110332] = _109071)], (393 ^ _98814) ^ [] : [-(aElement0(379 ^ [_109071, _109073, _110332]))], (401 ^ _98814) ^ [] : [aElementOf0(379 ^ [_109071, _109073, _110332], _110332)]]], (344 ^ _98814) ^ [_109352] : [_109352 = sdtpldt0(_109073, _109071), 347 ^ _98814 : [(362 ^ _98814) ^ [_109970] : [-(aElementOf0(_109970, _109352)), aElement0(_109970), 367 ^ _98814 : [(368 ^ _98814) ^ [] : [aElementOf0(_109970, _109073)], (370 ^ _98814) ^ [] : [_109970 = _109071]]], (350 ^ _98814) ^ [_109615] : [aElementOf0(_109615, _109352), 353 ^ _98814 : [(354 ^ _98814) ^ [] : [-(aElement0(_109615))], (356 ^ _98814) ^ [] : [-(aElementOf0(_109615, _109073)), -(_109615 = _109071)]]], (348 ^ _98814) ^ [] : [-(aSet0(_109352))]]]]], (82 ^ _98814) ^ [_101484, _101486] : [-(aSet0(_101484)), _101486 = _101484, aSet0(_101486)], (247 ^ _98814) ^ [_106377] : [aSet0(_106377), 250 ^ _98814 : [(251 ^ _98814) ^ [_106553] : [aSubsetOf0(_106553, _106377), 254 ^ _98814 : [(255 ^ _98814) ^ [] : [-(aSet0(_106553))], (257 ^ _98814) ^ [_106762] : [aElementOf0(_106762, _106553), -(aElementOf0(_106762, _106377))]]], (263 ^ _98814) ^ [_106941] : [-(aSubsetOf0(_106941, _106377)), aSet0(_106941), 269 ^ _98814 : [(270 ^ _98814) ^ [] : [-(aElementOf0(268 ^ [_106377, _106941], _106941))], (272 ^ _98814) ^ [] : [aElementOf0(268 ^ [_106377, _106941], _106377)]]]]], (651 ^ _98814) ^ [_118991] : [aElementOf0(_118991, szNzAzT0), -(sdtlseqdt0(_118991, szszuzczcdt0(_118991)))], (717 ^ _98814) ^ [_120869, _120871] : [aElementOf0(_120871, szNzAzT0), aElementOf0(_120869, szNzAzT0), iLess0(_120871, _120869), true___, -(true___)], (126 ^ _98814) ^ [_102877, _102879] : [_102879 = _102877, -(szszuzczcdt0(_102879) = szszuzczcdt0(_102877))], (213 ^ _98814) ^ [_105494] : [aSet0(_105494), isCountable0(_105494), true___, -(true___)], (681 ^ _98814) ^ [_119882, _119884, _119886] : [aElementOf0(_119886, szNzAzT0), aElementOf0(_119884, szNzAzT0), aElementOf0(_119882, szNzAzT0), -(sdtlseqdt0(_119886, _119882)), sdtlseqdt0(_119886, _119884), sdtlseqdt0(_119884, _119882)], (498 ^ _98814) ^ [_114420] : [aElement0(_114420), 501 ^ _98814 : [(502 ^ _98814) ^ [_114557] : [-(isCountable0(sdtpldt0(_114557, _114420))), aSet0(_114557), isCountable0(_114557)]]], (178 ^ _98814) ^ [_104493] : [aSet0(_104493), isFinite0(_104493), true___, -(true___)], (484 ^ _98814) ^ [_114033, _114035] : [aElement0(_114035), aSet0(_114033), -(aElementOf0(_114035, _114033)), -(sdtmndt0(sdtpldt0(_114033, _114035), _114035) = _114033)], (801 ^ _98814) ^ [] : [-(aElementOf0(xx, xS))], (2 ^ _98814) ^ [_98938] : [-(_98938 = _98938)], (290 ^ _98814) ^ [_107794] : [aSet0(_107794), -(aSubsetOf0(_107794, _107794))], (560 ^ _98814) ^ [_116297] : [aElementOf0(_116297, szNzAzT0), 563 ^ _98814 : [(564 ^ _98814) ^ [] : [-(aElementOf0(szszuzczcdt0(_116297), szNzAzT0))], (566 ^ _98814) ^ [] : [szszuzczcdt0(_116297) = sz00]]], (625 ^ _98814) ^ [_118233] : [aElementOf0(_118233, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_118233), sz00)], (200 ^ _98814) ^ [_105112] : [-(_105112 = slcrc0), aSet0(_105112), -(aElementOf0(205 ^ [_105112], _105112))], (741 ^ _98814) ^ [_121513] : [aSet0(_121513), -(aElement0(sbrdtbr0(_121513)))], (20 ^ _98814) ^ [_99590, _99592, _99594, _99596] : [-(aSubsetOf0(_99594, _99590)), aSubsetOf0(_99596, _99592), _99596 = _99594, _99592 = _99590], (595 ^ _98814) ^ [_117384] : [aElementOf0(_117384, szNzAzT0), _117384 = szszuzczcdt0(_117384)], (703 ^ _98814) ^ [_120474, _120476] : [aElementOf0(_120476, szNzAzT0), aElementOf0(_120474, szNzAzT0), -(sdtlseqdt0(_120476, _120474)), -(sdtlseqdt0(szszuzczcdt0(_120474), _120476))], (747 ^ _98814) ^ [_121703] : [aSet0(_121703), 750 ^ _98814 : [(751 ^ _98814) ^ [] : [aElementOf0(sbrdtbr0(_121703), szNzAzT0), -(isFinite0(_121703))], (757 ^ _98814) ^ [] : [isFinite0(_121703), -(aElementOf0(sbrdtbr0(_121703), szNzAzT0))]]], (132 ^ _98814) ^ [_103123, _103125, _103127, _103129] : [-(sdtmndt0(_103129, _103125) = sdtmndt0(_103127, _103123)), _103129 = _103127, _103125 = _103123], (192 ^ _98814) ^ [_104863] : [_104863 = slcrc0, 195 ^ _98814 : [(196 ^ _98814) ^ [] : [-(aSet0(_104863))], (198 ^ _98814) ^ [_105044] : [aElementOf0(_105044, _104863)]]], (296 ^ _98814) ^ [_107996, _107998] : [aSet0(_107998), aSet0(_107996), -(_107998 = _107996), aSubsetOf0(_107998, _107996), aSubsetOf0(_107996, _107998)], (663 ^ _98814) ^ [_119389, _119391] : [aElementOf0(_119391, szNzAzT0), aElementOf0(_119389, szNzAzT0), -(_119391 = _119389), sdtlseqdt0(_119391, _119389), sdtlseqdt0(_119389, _119391)], (92 ^ _98814) ^ [_101779, _101781] : [-(isFinite0(_101779)), _101781 = _101779, isFinite0(_101781)], (657 ^ _98814) ^ [_119185] : [aElementOf0(_119185, szNzAzT0), -(sdtlseqdt0(_119185, _119185))], (102 ^ _98814) ^ [_102082, _102084, _102086, _102088] : [-(aElementOf0(_102086, _102082)), aElementOf0(_102088, _102084), _102088 = _102086, _102084 = _102082], (314 ^ _98814) ^ [_108485, _108487, _108489] : [aSet0(_108489), aSet0(_108487), aSet0(_108485), -(aSubsetOf0(_108489, _108485)), aSubsetOf0(_108489, _108487), aSubsetOf0(_108487, _108485)], (763 ^ _98814) ^ [_122134] : [aSet0(_122134), 766 ^ _98814 : [(767 ^ _98814) ^ [] : [sbrdtbr0(_122134) = sz00, -(_122134 = slcrc0)], (773 ^ _98814) ^ [] : [_122134 = slcrc0, -(sbrdtbr0(_122134) = sz00)]]]], input).
% 166.85/161.72 ncf('1',plain,[szszuzczcdt0(sbrdtbr0(sdtmndt0(xS, xx))) = sbrdtbr0(xS)],start(803 ^ 0)).
% 166.85/161.72 ncf('1.1',plain,[-(szszuzczcdt0(sbrdtbr0(sdtmndt0(xS, xx))) = sbrdtbr0(xS)), sbrdtbr0(xS) = szszuzczcdt0(sbrdtbr0(sdtmndt0(xS, xx)))],extension(4 ^ 1,bind([[_99045, _99047], [szszuzczcdt0(sbrdtbr0(sdtmndt0(xS, xx))), sbrdtbr0(xS)]]))).
% 166.85/161.72 ncf('1.1.1',plain,[-(sbrdtbr0(xS) = szszuzczcdt0(sbrdtbr0(sdtmndt0(xS, xx)))), sbrdtbr0(xS) = sbrdtbr0(sdtpldt0(sdtmndt0(xS, xx), xx)), sbrdtbr0(sdtpldt0(sdtmndt0(xS, xx), xx)) = szszuzczcdt0(sbrdtbr0(sdtmndt0(xS, xx)))],extension(10 ^ 2,bind([[_99249, _99251, _99253], [szszuzczcdt0(sbrdtbr0(sdtmndt0(xS, xx))), sbrdtbr0(sdtpldt0(sdtmndt0(xS, xx), xx)), sbrdtbr0(xS)]]))).
% 166.85/161.72 ncf('1.1.1.1',plain,[-(sbrdtbr0(xS) = sbrdtbr0(sdtpldt0(sdtmndt0(xS, xx), xx))), xS = sdtpldt0(sdtmndt0(xS, xx), xx)],extension(142 ^ 3,bind([[_103434, _103436], [sdtpldt0(sdtmndt0(xS, xx), xx), xS]]))).
% 166.85/161.72 ncf('1.1.1.1.1',plain,[-(xS = sdtpldt0(sdtmndt0(xS, xx), xx)), sdtpldt0(sdtmndt0(xS, xx), xx) = xS],extension(4 ^ 4,bind([[_99045, _99047], [xS, sdtpldt0(sdtmndt0(xS, xx), xx)]]))).
% 166.85/161.72 ncf('1.1.1.1.1.1',plain,[-(sdtpldt0(sdtmndt0(xS, xx), xx) = xS), 478 : aElementOf0(xx, xS), 478 : aSet0(xS)],extension(474 ^ 5,bind([[_113667, _113804], [xS, xx]]))).
% 166.85/161.72 ncf('1.1.1.1.1.1.1',plain,[-(aElementOf0(xx, xS))],extension(801 ^ 8)).
% 166.85/161.72 ncf('1.1.1.1.1.1.2',plain,[-(aSet0(xS))],extension(797 ^ 6)).
% 166.85/161.72 ncf('1.1.1.2',plain,[-(sbrdtbr0(sdtpldt0(sdtmndt0(xS, xx), xx)) = szszuzczcdt0(sbrdtbr0(sdtmndt0(xS, xx)))), 787 : aElement0(xx), 787 : -(aElementOf0(xx, sdtmndt0(xS, xx))), 787 : aSet0(sdtmndt0(xS, xx)), 787 : isFinite0(sdtmndt0(xS, xx))],extension(779 ^ 3,bind([[_122568, _122798], [sdtmndt0(xS, xx), xx]]))).
% 166.85/161.72 ncf('1.1.1.2.1',plain,[-(aElement0(xx)), 172 : aElementOf0(xx, xS), 172 : aSet0(xS)],extension(168 ^ 6,bind([[_104162, _104292], [xS, xx]]))).
% 166.85/161.72 ncf('1.1.1.2.1.1',plain,[-(aElementOf0(xx, xS))],extension(801 ^ 9)).
% 166.85/161.72 ncf('1.1.1.2.1.2',plain,[-(aSet0(xS))],extension(797 ^ 7)).
% 166.85/161.72 ncf('1.1.1.2.2',plain,[aElementOf0(xx, sdtmndt0(xS, xx)), 427 : xx = xx, 419 : sdtmndt0(xS, xx) = sdtmndt0(xS, xx), 413 : aSet0(xS), 413 : aElement0(xx)],extension(405 ^ 6,bind([[_111369, _111371, _111652, _111917], [xx, xS, sdtmndt0(xS, xx), xx]]))).
% 166.85/161.72 ncf('1.1.1.2.2.1',plain,[-(xx = xx)],extension(2 ^ 13,bind([[_98938], [xx]]))).
% 166.85/161.72 ncf('1.1.1.2.2.2',plain,[-(sdtmndt0(xS, xx) = sdtmndt0(xS, xx))],extension(2 ^ 9,bind([[_98938], [sdtmndt0(xS, xx)]]))).
% 166.85/161.72 ncf('1.1.1.2.2.3',plain,[-(aSet0(xS))],extension(797 ^ 7)).
% 166.85/161.72 ncf('1.1.1.2.2.4',plain,[-(aElement0(xx))],lemmata('[1, 1, 1].x')).
% 166.85/161.72 ncf('1.1.1.2.3',plain,[-(aSet0(sdtmndt0(xS, xx))), 413 : sdtmndt0(xS, xx) = sdtmndt0(xS, xx), 413 : aSet0(xS), 413 : aElement0(xx)],extension(405 ^ 4,bind([[_111369, _111371, _111652], [xx, xS, sdtmndt0(xS, xx)]]))).
% 166.85/161.72 ncf('1.1.1.2.3.1',plain,[-(sdtmndt0(xS, xx) = sdtmndt0(xS, xx))],extension(2 ^ 7,bind([[_98938], [sdtmndt0(xS, xx)]]))).
% 166.85/161.72 ncf('1.1.1.2.3.2',plain,[-(aSet0(xS))],extension(797 ^ 5)).
% 166.85/161.72 ncf('1.1.1.2.3.3',plain,[-(aElement0(xx)), 172 : aElementOf0(xx, xS), 172 : aSet0(xS)],extension(168 ^ 5,bind([[_104162, _104292], [xS, xx]]))).
% 166.85/161.72 ncf('1.1.1.2.3.3.1',plain,[-(aElementOf0(xx, xS))],extension(801 ^ 8)).
% 166.85/161.72 ncf('1.1.1.2.3.3.2',plain,[-(aSet0(xS))],lemmata('[2, 1, 1, 1].x')).
% 166.85/161.72 ncf('1.1.1.2.4',plain,[-(isFinite0(sdtmndt0(xS, xx))), 544 : aSet0(xS), 544 : isFinite0(xS), 544 : aElement0(xx)],extension(540 ^ 4,bind([[_115707, _115844], [xx, xS]]))).
% 166.85/161.72 ncf('1.1.1.2.4.1',plain,[-(aSet0(xS))],extension(797 ^ 7)).
% 166.85/161.72 ncf('1.1.1.2.4.2',plain,[-(isFinite0(xS))],extension(799 ^ 7)).
% 166.85/161.72 ncf('1.1.1.2.4.3',plain,[-(aElement0(xx)), 172 : aElementOf0(xx, xS), 172 : aSet0(xS)],extension(168 ^ 5,bind([[_104162, _104292], [xS, xx]]))).
% 166.85/161.72 ncf('1.1.1.2.4.3.1',plain,[-(aElementOf0(xx, xS))],extension(801 ^ 8)).
% 166.85/161.72 ncf('1.1.1.2.4.3.2',plain,[-(aSet0(xS))],extension(797 ^ 6)).
% 166.85/161.72 %-----------------------------------------------------
% 166.85/161.72 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------