%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM491+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n032.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:46 EDT 2023
% Result : Theorem 22.37s 21.94s
% Output : Proof 22.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.09 % Problem : NUM491+1 : TPTP v8.1.2. Released v4.0.0.
% 0.08/0.09 % Command : nanocop.sh %s %d
% 0.09/0.28 % Computer : n032.cluster.edu
% 0.09/0.28 % Model : x86_64 x86_64
% 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.28 % Memory : 8042.1875MB
% 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.28 % CPULimit : 300
% 0.09/0.28 % WCLimit : 300
% 0.09/0.28 % DateTime : Thu May 18 17:20:04 EDT 2023
% 0.09/0.28 % CPUTime :
% 22.37/21.94
% 22.37/21.94 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 22.37/21.94 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.37/21.94 %-----------------------------------------------------
% 22.37/21.94 ncf(matrix, plain, [(856 ^ _113477) ^ [] : [doDivides0(xp, sdtasdt0(xp, xm))], (82 ^ _113477) ^ [_116189, _116191, _116193, _116195] : [-(sdtsldt0(_116195, _116191) = sdtsldt0(_116193, _116189)), _116195 = _116193, _116191 = _116189], (92 ^ _113477) ^ [_116548, _116550, _116552, _116554] : [-(sdtpldt0(_116554, _116550) = sdtpldt0(_116552, _116548)), _116554 = _116552, _116550 = _116548], (102 ^ _113477) ^ [_116907, _116909, _116911, _116913] : [-(sdtmndt0(_116913, _116909) = sdtmndt0(_116911, _116907)), _116913 = _116911, _116909 = _116907], (112 ^ _113477) ^ [_117246, _117248, _117250, _117252] : [-(sdtasdt0(_117252, _117248) = sdtasdt0(_117250, _117246)), _117252 = _117250, _117248 = _117246], (2 ^ _113477) ^ [_113621] : [-(_113621 = _113621)], (4 ^ _113477) ^ [_113728, _113730] : [_113730 = _113728, -(_113728 = _113730)], (10 ^ _113477) ^ [_113932, _113934, _113936] : [-(_113936 = _113932), _113936 = _113934, _113934 = _113932], (20 ^ _113477) ^ [_114245, _114247] : [-(aNaturalNumber0(_114245)), _114247 = _114245, aNaturalNumber0(_114247)], (30 ^ _113477) ^ [_114568, _114570, _114572, _114574] : [-(iLess0(_114572, _114568)), iLess0(_114574, _114570), _114574 = _114572, _114570 = _114568], (44 ^ _113477) ^ [_114984, _114986] : [-(isPrime0(_114984)), _114986 = _114984, isPrime0(_114986)], (54 ^ _113477) ^ [_115307, _115309, _115311, _115313] : [-(sdtlseqdt0(_115311, _115307)), sdtlseqdt0(_115313, _115309), _115313 = _115311, _115309 = _115307], (68 ^ _113477) ^ [_115731, _115733, _115735, _115737] : [-(doDivides0(_115735, _115731)), doDivides0(_115737, _115733), _115737 = _115735, _115733 = _115731], (122 ^ _113477) ^ [_117577] : [aNaturalNumber0(_117577), true___, -(true___)], (132 ^ _113477) ^ [] : [-(aNaturalNumber0(sz00))], (134 ^ _113477) ^ [] : [-(aNaturalNumber0(sz10))], (136 ^ _113477) ^ [] : [sz10 = sz00], (138 ^ _113477) ^ [_118006, _118008] : [-(aNaturalNumber0(sdtpldt0(_118008, _118006))), aNaturalNumber0(_118008), aNaturalNumber0(_118006)], (148 ^ _113477) ^ [_118305, _118307] : [-(aNaturalNumber0(sdtasdt0(_118307, _118305))), aNaturalNumber0(_118307), aNaturalNumber0(_118305)], (158 ^ _113477) ^ [_118604, _118606] : [-(sdtpldt0(_118606, _118604) = sdtpldt0(_118604, _118606)), aNaturalNumber0(_118606), aNaturalNumber0(_118604)], (168 ^ _113477) ^ [_118925, _118927, _118929] : [-(sdtpldt0(sdtpldt0(_118929, _118927), _118925) = sdtpldt0(_118929, sdtpldt0(_118927, _118925))), aNaturalNumber0(_118929), aNaturalNumber0(_118927), aNaturalNumber0(_118925)], (182 ^ _113477) ^ [_119331] : [aNaturalNumber0(_119331), 185 ^ _113477 : [(186 ^ _113477) ^ [] : [-(sdtpldt0(_119331, sz00) = _119331)], (188 ^ _113477) ^ [] : [-(_119331 = sdtpldt0(sz00, _119331))]]], (190 ^ _113477) ^ [_119618, _119620] : [-(sdtasdt0(_119620, _119618) = sdtasdt0(_119618, _119620)), aNaturalNumber0(_119620), aNaturalNumber0(_119618)], (200 ^ _113477) ^ [_119939, _119941, _119943] : [-(sdtasdt0(sdtasdt0(_119943, _119941), _119939) = sdtasdt0(_119943, sdtasdt0(_119941, _119939))), aNaturalNumber0(_119943), aNaturalNumber0(_119941), aNaturalNumber0(_119939)], (214 ^ _113477) ^ [_120345] : [aNaturalNumber0(_120345), 217 ^ _113477 : [(218 ^ _113477) ^ [] : [-(sdtasdt0(_120345, sz10) = _120345)], (220 ^ _113477) ^ [] : [-(_120345 = sdtasdt0(sz10, _120345))]]], (222 ^ _113477) ^ [_120618] : [aNaturalNumber0(_120618), 225 ^ _113477 : [(226 ^ _113477) ^ [] : [-(sdtasdt0(_120618, sz00) = sz00)], (228 ^ _113477) ^ [] : [-(sz00 = sdtasdt0(sz00, _120618))]]], (230 ^ _113477) ^ [_120919, _120921, _120923] : [241 ^ _113477 : [(242 ^ _113477) ^ [] : [-(sdtasdt0(_120923, sdtpldt0(_120921, _120919)) = sdtpldt0(sdtasdt0(_120923, _120921), sdtasdt0(_120923, _120919)))], (244 ^ _113477) ^ [] : [-(sdtasdt0(sdtpldt0(_120921, _120919), _120923) = sdtpldt0(sdtasdt0(_120921, _120923), sdtasdt0(_120919, _120923)))]], aNaturalNumber0(_120923), aNaturalNumber0(_120921), aNaturalNumber0(_120919)], (246 ^ _113477) ^ [_121466, _121468, _121470] : [259 ^ _113477 : [(260 ^ _113477) ^ [] : [sdtpldt0(_121470, _121468) = sdtpldt0(_121470, _121466)], (262 ^ _113477) ^ [] : [sdtpldt0(_121468, _121470) = sdtpldt0(_121466, _121470)]], -(_121468 = _121466), aNaturalNumber0(_121470), aNaturalNumber0(_121468), aNaturalNumber0(_121466)], (266 ^ _113477) ^ [_122043] : [aNaturalNumber0(_122043), -(_122043 = sz00), 273 ^ _113477 : [(274 ^ _113477) ^ [_122305, _122307] : [aNaturalNumber0(_122307), aNaturalNumber0(_122305), 283 ^ _113477 : [(284 ^ _113477) ^ [] : [sdtasdt0(_122043, _122307) = sdtasdt0(_122043, _122305)], (286 ^ _113477) ^ [] : [sdtasdt0(_122307, _122043) = sdtasdt0(_122305, _122043)]], -(_122307 = _122305)]]], (290 ^ _113477) ^ [_122816, _122818] : [aNaturalNumber0(_122818), aNaturalNumber0(_122816), sdtpldt0(_122818, _122816) = sz00, 301 ^ _113477 : [(302 ^ _113477) ^ [] : [-(_122818 = sz00)], (304 ^ _113477) ^ [] : [-(_122816 = sz00)]]], (306 ^ _113477) ^ [_123283, _123285] : [aNaturalNumber0(_123285), aNaturalNumber0(_123283), sdtasdt0(_123285, _123283) = sz00, -(_123285 = sz00), -(_123283 = sz00)], (324 ^ _113477) ^ [_123765, _123767] : [aNaturalNumber0(_123767), aNaturalNumber0(_123765), 331 ^ _113477 : [(332 ^ _113477) ^ [] : [sdtlseqdt0(_123767, _123765), 336 ^ _113477 : [(337 ^ _113477) ^ [] : [-(aNaturalNumber0(335 ^ [_123765, _123767]))], (339 ^ _113477) ^ [] : [-(sdtpldt0(_123767, 335 ^ [_123765, _123767]) = _123765)]]], (341 ^ _113477) ^ [] : [-(sdtlseqdt0(_123767, _123765)), 342 ^ _113477 : [(343 ^ _113477) ^ [_124325] : [aNaturalNumber0(_124325), sdtpldt0(_123767, _124325) = _123765]]]]], (351 ^ _113477) ^ [_124608, _124610] : [aNaturalNumber0(_124610), aNaturalNumber0(_124608), sdtlseqdt0(_124610, _124608), 362 ^ _113477 : [(363 ^ _113477) ^ [_124955] : [_124955 = sdtmndt0(_124608, _124610), 366 ^ _113477 : [(367 ^ _113477) ^ [] : [-(aNaturalNumber0(_124955))], (369 ^ _113477) ^ [] : [-(sdtpldt0(_124610, _124955) = _124608)]]], (371 ^ _113477) ^ [_125214] : [-(_125214 = sdtmndt0(_124608, _124610)), aNaturalNumber0(_125214), sdtpldt0(_124610, _125214) = _124608]]], (381 ^ _113477) ^ [_125536] : [aNaturalNumber0(_125536), -(sdtlseqdt0(_125536, _125536))], (387 ^ _113477) ^ [_125738, _125740] : [aNaturalNumber0(_125740), aNaturalNumber0(_125738), -(_125740 = _125738), sdtlseqdt0(_125740, _125738), sdtlseqdt0(_125738, _125740)], (405 ^ _113477) ^ [_126227, _126229, _126231] : [aNaturalNumber0(_126231), aNaturalNumber0(_126229), aNaturalNumber0(_126227), -(sdtlseqdt0(_126231, _126227)), sdtlseqdt0(_126231, _126229), sdtlseqdt0(_126229, _126227)], (427 ^ _113477) ^ [_126813, _126815] : [aNaturalNumber0(_126815), aNaturalNumber0(_126813), -(sdtlseqdt0(_126815, _126813)), 438 ^ _113477 : [(439 ^ _113477) ^ [] : [_126813 = _126815], (441 ^ _113477) ^ [] : [-(sdtlseqdt0(_126813, _126815))]]], (443 ^ _113477) ^ [_127276, _127278] : [aNaturalNumber0(_127278), aNaturalNumber0(_127276), -(_127278 = _127276), sdtlseqdt0(_127278, _127276), 458 ^ _113477 : [(459 ^ _113477) ^ [_127720] : [aNaturalNumber0(_127720), 462 ^ _113477 : [(463 ^ _113477) ^ [] : [sdtpldt0(_127720, _127278) = sdtpldt0(_127720, _127276)], (465 ^ _113477) ^ [] : [-(sdtlseqdt0(sdtpldt0(_127720, _127278), sdtpldt0(_127720, _127276)))], (467 ^ _113477) ^ [] : [sdtpldt0(_127278, _127720) = sdtpldt0(_127276, _127720)], (469 ^ _113477) ^ [] : [-(sdtlseqdt0(sdtpldt0(_127278, _127720), sdtpldt0(_127276, _127720)))]]]]], (471 ^ _113477) ^ [_128244, _128246, _128248] : [aNaturalNumber0(_128248), aNaturalNumber0(_128246), aNaturalNumber0(_128244), 494 ^ _113477 : [(495 ^ _113477) ^ [] : [sdtasdt0(_128248, _128246) = sdtasdt0(_128248, _128244)], (497 ^ _113477) ^ [] : [-(sdtlseqdt0(sdtasdt0(_128248, _128246), sdtasdt0(_128248, _128244)))], (499 ^ _113477) ^ [] : [sdtasdt0(_128246, _128248) = sdtasdt0(_128244, _128248)], (501 ^ _113477) ^ [] : [-(sdtlseqdt0(sdtasdt0(_128246, _128248), sdtasdt0(_128244, _128248)))]], -(_128248 = sz00), -(_128246 = _128244), sdtlseqdt0(_128246, _128244)], (503 ^ _113477) ^ [_129194] : [aNaturalNumber0(_129194), -(_129194 = sz00), -(_129194 = sz10), 514 ^ _113477 : [(515 ^ _113477) ^ [] : [sz10 = _129194], (517 ^ _113477) ^ [] : [-(sdtlseqdt0(sz10, _129194))]]], (519 ^ _113477) ^ [_129642, _129644] : [aNaturalNumber0(_129644), aNaturalNumber0(_129642), -(_129644 = sz00), -(sdtlseqdt0(_129642, sdtasdt0(_129642, _129644)))], (533 ^ _113477) ^ [_130037, _130039] : [aNaturalNumber0(_130039), aNaturalNumber0(_130037), iLess0(_130039, _130037), true___, -(true___)], (551 ^ _113477) ^ [_130497, _130499] : [aNaturalNumber0(_130499), aNaturalNumber0(_130497), -(iLess0(_130499, _130497)), -(_130499 = _130497), sdtlseqdt0(_130499, _130497)], (569 ^ _113477) ^ [_130975, _130977] : [aNaturalNumber0(_130977), aNaturalNumber0(_130975), 576 ^ _113477 : [(577 ^ _113477) ^ [] : [doDivides0(_130977, _130975), 581 ^ _113477 : [(582 ^ _113477) ^ [] : [-(aNaturalNumber0(580 ^ [_130975, _130977]))], (584 ^ _113477) ^ [] : [-(_130975 = sdtasdt0(_130977, 580 ^ [_130975, _130977]))]]], (586 ^ _113477) ^ [] : [-(doDivides0(_130977, _130975)), 587 ^ _113477 : [(588 ^ _113477) ^ [_131535] : [aNaturalNumber0(_131535), _130975 = sdtasdt0(_130977, _131535)]]]]], (596 ^ _113477) ^ [_131818, _131820] : [aNaturalNumber0(_131820), aNaturalNumber0(_131818), -(_131820 = sz00), doDivides0(_131820, _131818), 611 ^ _113477 : [(612 ^ _113477) ^ [_132257] : [_132257 = sdtsldt0(_131818, _131820), 615 ^ _113477 : [(616 ^ _113477) ^ [] : [-(aNaturalNumber0(_132257))], (618 ^ _113477) ^ [] : [-(_131818 = sdtasdt0(_131820, _132257))]]], (620 ^ _113477) ^ [_132516] : [-(_132516 = sdtsldt0(_131818, _131820)), aNaturalNumber0(_132516), _131818 = sdtasdt0(_131820, _132516)]]], (630 ^ _113477) ^ [_132868, _132870, _132872] : [aNaturalNumber0(_132872), aNaturalNumber0(_132870), aNaturalNumber0(_132868), -(doDivides0(_132872, _132868)), doDivides0(_132872, _132870), doDivides0(_132870, _132868)], (652 ^ _113477) ^ [_133468, _133470, _133472] : [aNaturalNumber0(_133472), aNaturalNumber0(_133470), aNaturalNumber0(_133468), -(doDivides0(_133472, sdtpldt0(_133470, _133468))), doDivides0(_133472, _133470), doDivides0(_133472, _133468)], (674 ^ _113477) ^ [_134074, _134076, _134078] : [aNaturalNumber0(_134078), aNaturalNumber0(_134076), aNaturalNumber0(_134074), -(doDivides0(_134078, _134074)), doDivides0(_134078, _134076), doDivides0(_134078, sdtpldt0(_134076, _134074))], (696 ^ _113477) ^ [_134666, _134668] : [aNaturalNumber0(_134668), aNaturalNumber0(_134666), -(sdtlseqdt0(_134668, _134666)), doDivides0(_134668, _134666), -(_134666 = sz00)], (714 ^ _113477) ^ [_135144, _135146] : [aNaturalNumber0(_135146), aNaturalNumber0(_135144), -(_135146 = sz00), doDivides0(_135146, _135144), 729 ^ _113477 : [(730 ^ _113477) ^ [_135554] : [aNaturalNumber0(_135554), -(sdtasdt0(_135554, sdtsldt0(_135144, _135146)) = sdtsldt0(sdtasdt0(_135554, _135144), _135146))]]], (736 ^ _113477) ^ [_135795] : [aNaturalNumber0(_135795), 739 ^ _113477 : [(762 ^ _113477) ^ [] : [-(isPrime0(_135795)), -(_135795 = sz00), -(_135795 = sz10), 772 ^ _113477 : [(773 ^ _113477) ^ [] : [-(aNaturalNumber0(771 ^ [_135795]))], (775 ^ _113477) ^ [] : [-(doDivides0(771 ^ [_135795], _135795))], (777 ^ _113477) ^ [] : [771 ^ [_135795] = sz10], (779 ^ _113477) ^ [] : [771 ^ [_135795] = _135795]]], (740 ^ _113477) ^ [] : [isPrime0(_135795), 743 ^ _113477 : [(744 ^ _113477) ^ [] : [_135795 = sz00], (746 ^ _113477) ^ [] : [_135795 = sz10], (748 ^ _113477) ^ [_136187] : [aNaturalNumber0(_136187), doDivides0(_136187, _135795), -(_136187 = sz10), -(_136187 = _135795)]]]]], (783 ^ _113477) ^ [_137139] : [795 ^ _113477 : [(796 ^ _113477) ^ [] : [-(aNaturalNumber0(794 ^ [_137139]))], (798 ^ _113477) ^ [] : [-(doDivides0(794 ^ [_137139], _137139))], (800 ^ _113477) ^ [] : [-(isPrime0(794 ^ [_137139]))]], aNaturalNumber0(_137139), -(_137139 = sz00), -(_137139 = sz10)], (802 ^ _113477) ^ [] : [-(aNaturalNumber0(xn))], (804 ^ _113477) ^ [] : [-(aNaturalNumber0(xm))], (806 ^ _113477) ^ [] : [-(aNaturalNumber0(xp))], (838 ^ _113477) ^ [] : [-(isPrime0(xp))], (840 ^ _113477) ^ [] : [-(doDivides0(xp, sdtasdt0(xn, xm)))], (842 ^ _113477) ^ [] : [-(sdtlseqdt0(xp, xn))], (844 ^ _113477) ^ [] : [-(xr = sdtmndt0(xn, xp))], (846 ^ _113477) ^ [] : [xr = xn], (848 ^ _113477) ^ [] : [-(sdtlseqdt0(xr, xn))], (850 ^ _113477) ^ [] : [-(xn = sdtpldt0(xp, xr))], (852 ^ _113477) ^ [] : [-(sdtasdt0(xn, xm) = sdtpldt0(sdtasdt0(xp, xm), sdtasdt0(xr, xm)))], (854 ^ _113477) ^ [] : [-(sdtasdt0(xr, xm) = sdtmndt0(sdtasdt0(xn, xm), sdtasdt0(xp, xm)))], (808 ^ _113477) ^ [_137906, _137908, _137910] : [aNaturalNumber0(_137910), aNaturalNumber0(_137908), aNaturalNumber0(_137906), isPrime0(_137906), doDivides0(_137906, sdtasdt0(_137910, _137908)), iLess0(sdtpldt0(sdtpldt0(_137910, _137908), _137906), sdtpldt0(sdtpldt0(xn, xm), xp)), -(doDivides0(_137906, _137910)), -(doDivides0(_137906, _137908))]], input).
% 22.37/21.94 ncf('1',plain,[doDivides0(xp, sdtasdt0(xp, xm))],start(856 ^ 0)).
% 22.37/21.94 ncf('1.1',plain,[-(doDivides0(xp, sdtasdt0(xp, xm))), 588 : aNaturalNumber0(sz00), 588 : sdtasdt0(xp, xm) = sdtasdt0(xp, sz00), 586 : aNaturalNumber0(xp), 586 : aNaturalNumber0(sdtasdt0(xp, xm))],extension(569 ^ 1,bind([[_130975, _130977, _131535], [sdtasdt0(xp, xm), xp, sz00]]))).
% 22.37/21.94 ncf('1.1.1',plain,[-(aNaturalNumber0(sz00))],extension(132 ^ 6)).
% 22.37/21.94 ncf('1.1.2',plain,[-(sdtasdt0(xp, xm) = sdtasdt0(xp, sz00)), xp = xp, xm = sz00],extension(112 ^ 6,bind([[_117246, _117248, _117250, _117252], [sz00, xm, xp, xp]]))).
% 22.37/21.94 ncf('1.1.2.1',plain,[-(xp = xp)],extension(2 ^ 7,bind([[_113621], [xp]]))).
% 22.37/21.94 ncf('1.1.2.2',plain,[-(xm = sz00), 796 : -(aNaturalNumber0(794 ^ [xm])), 796 : aNaturalNumber0(xm), 796 : -(xm = sz10)],extension(783 ^ 7,bind([[_137139], [xm]]))).
% 22.37/21.94 ncf('1.1.2.2.1',plain,[aNaturalNumber0(794 ^ [xm]), 260 : sdtpldt0(794 ^ [xm], sdtasdt0(xp, xm)) = sdtpldt0(794 ^ [xm], sdtasdt0(xp, xm)), 260 : -(sdtasdt0(xp, xm) = sdtasdt0(xp, xm)), 260 : aNaturalNumber0(sdtasdt0(xp, xm)), 260 : aNaturalNumber0(sdtasdt0(xp, xm))],extension(246 ^ 10,bind([[_121466, _121468, _121470], [sdtasdt0(xp, xm), sdtasdt0(xp, xm), 794 ^ [xm]]]))).
% 22.37/21.94 ncf('1.1.2.2.1.1',plain,[-(sdtpldt0(794 ^ [xm], sdtasdt0(xp, xm)) = sdtpldt0(794 ^ [xm], sdtasdt0(xp, xm)))],extension(2 ^ 13,bind([[_113621], [sdtpldt0(794 ^ [xm], sdtasdt0(xp, xm))]]))).
% 22.37/21.94 ncf('1.1.2.2.1.2',plain,[sdtasdt0(xp, xm) = sdtasdt0(xp, xm), aNaturalNumber0(xm)],extension(588 ^ 11,bind([[_131535], [xm]]))).
% 22.37/21.94 ncf('1.1.2.2.1.2.1',plain,[-(aNaturalNumber0(xm))],extension(804 ^ 12)).
% 22.37/21.94 ncf('1.1.2.2.1.3',plain,[-(aNaturalNumber0(sdtasdt0(xp, xm))), aNaturalNumber0(xp), aNaturalNumber0(xm)],extension(148 ^ 11,bind([[_118305, _118307], [xm, xp]]))).
% 22.37/21.94 ncf('1.1.2.2.1.3.1',plain,[-(aNaturalNumber0(xp))],extension(806 ^ 12)).
% 22.37/21.94 ncf('1.1.2.2.1.3.2',plain,[-(aNaturalNumber0(xm))],extension(804 ^ 12)).
% 22.37/21.94 ncf('1.1.2.2.1.4',plain,[-(aNaturalNumber0(sdtasdt0(xp, xm)))],lemmata('[2, 2, 1, 1].x')).
% 22.37/21.94 ncf('1.1.2.2.2',plain,[-(aNaturalNumber0(xm))],extension(804 ^ 8)).
% 22.37/21.94 ncf('1.1.2.2.3',plain,[xm = sz10, -(sdtasdt0(xp, xm) = sdtasdt0(xp, sz10)), xp = xp],extension(112 ^ 8,bind([[_117246, _117248, _117250, _117252], [sz10, xm, xp, xp]]))).
% 22.37/21.94 ncf('1.1.2.2.3.1',plain,[sdtasdt0(xp, xm) = sdtasdt0(xp, sz10), aNaturalNumber0(sz10)],extension(588 ^ 9,bind([[_131535], [sz10]]))).
% 22.37/21.94 ncf('1.1.2.2.3.1.1',plain,[-(aNaturalNumber0(sz10))],extension(134 ^ 10)).
% 22.37/21.94 ncf('1.1.2.2.3.2',plain,[-(xp = xp)],lemmata('[1, 1].x')).
% 22.37/21.94 ncf('1.1.3',plain,[-(aNaturalNumber0(xp))],extension(806 ^ 2)).
% 22.37/21.94 ncf('1.1.4',plain,[-(aNaturalNumber0(sdtasdt0(xp, xm))), aNaturalNumber0(xp), aNaturalNumber0(xm)],extension(148 ^ 2,bind([[_118305, _118307], [xm, xp]]))).
% 22.37/21.94 ncf('1.1.4.1',plain,[-(aNaturalNumber0(xp))],lemmata('[1].x')).
% 22.37/21.94 ncf('1.1.4.2',plain,[-(aNaturalNumber0(xm))],extension(804 ^ 3)).
% 22.37/21.94 %-----------------------------------------------------
% 22.37/21.94 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------