%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : RNG061+2 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n011.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:49:42 EDT 2023
% Result : Theorem 5.18s 5.49s
% Output : Proof 5.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : RNG061+2 : TPTP v8.1.2. Released v4.0.0.
% 0.10/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n011.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 20:27:18 EDT 2023
% 0.12/0.33 % CPUTime :
% 5.18/5.49
% 5.18/5.49 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 5.18/5.49 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.18/5.49 %-----------------------------------------------------
% 5.18/5.49 ncf(matrix, plain, [(778 ^ _114949) ^ [] : [sdtasdt0(sdtpldt0(xR, smndt0(xS)), sdtpldt0(xR, smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(sdtasdt0(xS, xS), smndt0(xN)))], (78 ^ _114949) ^ [_117484, _117486] : [_117486 = _117484, -(szszuzczcdt0(_117486) = szszuzczcdt0(_117484))], (84 ^ _114949) ^ [_117702, _117704] : [_117704 = _117702, -(sziznziztdt0(_117704) = sziznziztdt0(_117702))], (90 ^ _114949) ^ [_117948, _117950, _117952, _117954] : [-(sdtlbdtrb0(_117954, _117950) = sdtlbdtrb0(_117952, _117948)), _117954 = _117952, _117950 = _117948], (100 ^ _114949) ^ [_118279, _118281] : [_118281 = _118279, -(aDimensionOf0(_118281) = aDimensionOf0(_118279))], (106 ^ _114949) ^ [_118525, _118527, _118529, _118531] : [-(sdtasasdt0(_118531, _118527) = sdtasasdt0(_118529, _118525)), _118531 = _118529, _118527 = _118525], (116 ^ _114949) ^ [_118884, _118886, _118888, _118890] : [-(sdtpldt0(_118890, _118886) = sdtpldt0(_118888, _118884)), _118890 = _118888, _118886 = _118884], (136 ^ _114949) ^ [_119554, _119556] : [_119556 = _119554, -(smndt0(_119556) = smndt0(_119554))], (126 ^ _114949) ^ [_119243, _119245, _119247, _119249] : [-(sdtasdt0(_119249, _119245) = sdtasdt0(_119247, _119243)), _119249 = _119247, _119245 = _119243], (2 ^ _114949) ^ [_115093] : [-(_115093 = _115093)], (4 ^ _114949) ^ [_115200, _115202] : [_115202 = _115200, -(_115200 = _115202)], (10 ^ _114949) ^ [_115404, _115406, _115408] : [-(_115408 = _115404), _115408 = _115406, _115406 = _115404], (20 ^ _114949) ^ [_115745, _115747, _115749, _115751] : [-(iLess0(_115749, _115745)), iLess0(_115751, _115747), _115751 = _115749, _115747 = _115745], (34 ^ _114949) ^ [_116161, _116163] : [-(aVector0(_116161)), _116163 = _116161, aVector0(_116163)], (44 ^ _114949) ^ [_116456, _116458] : [-(aNaturalNumber0(_116456)), _116458 = _116456, aNaturalNumber0(_116458)], (54 ^ _114949) ^ [_116751, _116753] : [-(aScalar0(_116751)), _116753 = _116751, aScalar0(_116753)], (64 ^ _114949) ^ [_117054, _117056, _117058, _117060] : [-(sdtlseqdt0(_117058, _117054)), sdtlseqdt0(_117060, _117056), _117060 = _117058, _117056 = _117054], (142 ^ _114949) ^ [_119788] : [aNaturalNumber0(_119788), true___, -(true___)], (152 ^ _114949) ^ [] : [-(aNaturalNumber0(sz00))], (154 ^ _114949) ^ [_120096] : [aNaturalNumber0(_120096), 157 ^ _114949 : [(158 ^ _114949) ^ [] : [-(aNaturalNumber0(szszuzczcdt0(_120096)))], (160 ^ _114949) ^ [] : [szszuzczcdt0(_120096) = sz00]]], (162 ^ _114949) ^ [_120364] : [170 ^ _114949 : [(171 ^ _114949) ^ [] : [-(aNaturalNumber0(169 ^ [_120364]))], (173 ^ _114949) ^ [] : [-(_120364 = szszuzczcdt0(169 ^ [_120364]))]], aNaturalNumber0(_120364), -(_120364 = sz00)], (175 ^ _114949) ^ [_120792, _120794] : [aNaturalNumber0(_120794), aNaturalNumber0(_120792), szszuzczcdt0(_120794) = szszuzczcdt0(_120792), -(_120794 = _120792)], (189 ^ _114949) ^ [_121186, _121188] : [aNaturalNumber0(_121188), aNaturalNumber0(_121186), iLess0(_121188, _121186), true___, -(true___)], (207 ^ _114949) ^ [_121632] : [aNaturalNumber0(_121632), -(iLess0(_121632, szszuzczcdt0(_121632)))], (213 ^ _114949) ^ [_121824] : [aScalar0(_121824), true___, -(true___)], (223 ^ _114949) ^ [] : [-(aScalar0(sz0z00))], (225 ^ _114949) ^ [_122146, _122148] : [-(aScalar0(sdtpldt0(_122148, _122146))), aScalar0(_122148), aScalar0(_122146)], (235 ^ _114949) ^ [_122445, _122447] : [-(aScalar0(sdtasdt0(_122447, _122445))), aScalar0(_122447), aScalar0(_122445)], (245 ^ _114949) ^ [_122730] : [aScalar0(_122730), -(aScalar0(smndt0(_122730)))], (251 ^ _114949) ^ [_122920] : [aScalar0(_122920), 254 ^ _114949 : [(255 ^ _114949) ^ [] : [-(sdtpldt0(_122920, sz0z00) = _122920)], (257 ^ _114949) ^ [] : [-(sdtpldt0(sz0z00, _122920) = _122920)], (259 ^ _114949) ^ [] : [-(sdtasdt0(_122920, sz0z00) = sz0z00)], (261 ^ _114949) ^ [] : [-(sdtasdt0(sz0z00, _122920) = sz0z00)], (263 ^ _114949) ^ [] : [-(sdtpldt0(_122920, smndt0(_122920)) = sz0z00)], (265 ^ _114949) ^ [] : [-(sdtpldt0(smndt0(_122920), _122920) = sz0z00)], (267 ^ _114949) ^ [] : [-(smndt0(smndt0(_122920)) = _122920)], (269 ^ _114949) ^ [] : [-(smndt0(sz0z00) = sz0z00)]]], (271 ^ _114949) ^ [_123687, _123689, _123691] : [282 ^ _114949 : [(283 ^ _114949) ^ [] : [-(sdtpldt0(sdtpldt0(_123691, _123689), _123687) = sdtpldt0(_123691, sdtpldt0(_123689, _123687)))], (285 ^ _114949) ^ [] : [-(sdtpldt0(_123691, _123689) = sdtpldt0(_123689, _123691))], (287 ^ _114949) ^ [] : [-(sdtasdt0(sdtasdt0(_123691, _123689), _123687) = sdtasdt0(_123691, sdtasdt0(_123689, _123687)))], (289 ^ _114949) ^ [] : [-(sdtasdt0(_123691, _123689) = sdtasdt0(_123689, _123691))]], aScalar0(_123691), aScalar0(_123689), aScalar0(_123687)], (291 ^ _114949) ^ [_124398, _124400, _124402] : [302 ^ _114949 : [(303 ^ _114949) ^ [] : [-(sdtasdt0(_124402, sdtpldt0(_124400, _124398)) = sdtpldt0(sdtasdt0(_124402, _124400), sdtasdt0(_124402, _124398)))], (305 ^ _114949) ^ [] : [-(sdtasdt0(sdtpldt0(_124402, _124400), _124398) = sdtpldt0(sdtasdt0(_124402, _124398), sdtasdt0(_124400, _124398)))]], aScalar0(_124402), aScalar0(_124400), aScalar0(_124398)], (307 ^ _114949) ^ [_124959, _124961, _124963, _124965] : [-(sdtasdt0(sdtpldt0(_124965, _124963), sdtpldt0(_124961, _124959)) = sdtpldt0(sdtpldt0(sdtasdt0(_124965, _124961), sdtasdt0(_124965, _124959)), sdtpldt0(sdtasdt0(_124963, _124961), sdtasdt0(_124963, _124959)))), aScalar0(_124965), aScalar0(_124963), aScalar0(_124961), aScalar0(_124959)], (325 ^ _114949) ^ [_125524, _125526] : [332 ^ _114949 : [(333 ^ _114949) ^ [] : [-(sdtasdt0(_125526, smndt0(_125524)) = smndt0(sdtasdt0(_125526, _125524)))], (335 ^ _114949) ^ [] : [-(sdtasdt0(smndt0(_125526), _125524) = smndt0(sdtasdt0(_125526, _125524)))]], aScalar0(_125526), aScalar0(_125524)], (337 ^ _114949) ^ [_125934, _125936] : [-(sdtasdt0(smndt0(_125936), smndt0(_125934)) = sdtasdt0(_125936, _125934)), aScalar0(_125936), aScalar0(_125934)], (347 ^ _114949) ^ [_126249, _126251] : [aScalar0(_126251), aScalar0(_126249), sdtlseqdt0(_126251, _126249), true___, -(true___)], (365 ^ _114949) ^ [_126695] : [aScalar0(_126695), -(sdtlseqdt0(_126695, _126695))], (371 ^ _114949) ^ [_126897, _126899] : [aScalar0(_126899), aScalar0(_126897), -(_126899 = _126897), sdtlseqdt0(_126899, _126897), sdtlseqdt0(_126897, _126899)], (389 ^ _114949) ^ [_127386, _127388, _127390] : [aScalar0(_127390), aScalar0(_127388), aScalar0(_127386), -(sdtlseqdt0(_127390, _127386)), sdtlseqdt0(_127390, _127388), sdtlseqdt0(_127388, _127386)], (411 ^ _114949) ^ [_128000, _128002, _128004, _128006] : [-(sdtlseqdt0(sdtpldt0(_128006, _128002), sdtpldt0(_128004, _128000))), sdtlseqdt0(_128006, _128004), sdtlseqdt0(_128002, _128000), aScalar0(_128006), aScalar0(_128004), aScalar0(_128002), aScalar0(_128000)], (437 ^ _114949) ^ [_128743, _128745, _128747, _128749] : [aScalar0(_128749), aScalar0(_128747), aScalar0(_128745), aScalar0(_128743), -(sdtlseqdt0(sdtasdt0(_128749, _128745), sdtasdt0(_128747, _128743))), sdtlseqdt0(_128749, _128747), sdtlseqdt0(sz0z00, _128745), sdtlseqdt0(_128745, _128743)], (467 ^ _114949) ^ [_129557, _129559] : [aScalar0(_129559), aScalar0(_129557), -(sdtlseqdt0(_129559, _129557)), -(sdtlseqdt0(_129557, _129559))], (481 ^ _114949) ^ [_129944, _129946] : [aScalar0(_129946), aScalar0(_129944), 496 ^ _114949 : [(497 ^ _114949) ^ [] : [-(sdtlseqdt0(sz0z00, sdtpldt0(_129946, _129944)))], (499 ^ _114949) ^ [] : [-(sdtlseqdt0(sz0z00, sdtasdt0(_129946, _129944)))]], sdtlseqdt0(sz0z00, _129946), sdtlseqdt0(sz0z00, _129944)], (501 ^ _114949) ^ [_130492] : [aScalar0(_130492), -(sdtlseqdt0(sz0z00, sdtasdt0(_130492, _130492)))], (507 ^ _114949) ^ [_130700, _130702] : [aScalar0(_130702), aScalar0(_130700), -(_130702 = _130700), sdtlseqdt0(sz0z00, _130702), sdtlseqdt0(sz0z00, _130700), sdtasdt0(_130702, _130702) = sdtasdt0(_130700, _130700)], (529 ^ _114949) ^ [_131262] : [aVector0(_131262), true___, -(true___)], (539 ^ _114949) ^ [_131517] : [aVector0(_131517), -(aNaturalNumber0(aDimensionOf0(_131517)))], (545 ^ _114949) ^ [_131721, _131723] : [-(aScalar0(sdtlbdtrb0(_131723, _131721))), aVector0(_131723), aNaturalNumber0(_131721)], (555 ^ _114949) ^ [_132006] : [aVector0(_132006), -(aDimensionOf0(_132006) = sz00), 562 ^ _114949 : [(563 ^ _114949) ^ [_132289] : [_132289 = sziznziztdt0(_132006), 566 ^ _114949 : [(567 ^ _114949) ^ [] : [-(aVector0(_132289))], (569 ^ _114949) ^ [] : [-(szszuzczcdt0(aDimensionOf0(_132289)) = aDimensionOf0(_132006))], (571 ^ _114949) ^ [_132591] : [aNaturalNumber0(_132591), -(sdtlbdtrb0(_132289, _132591) = sdtlbdtrb0(_132006, _132591))]]], (577 ^ _114949) ^ [_132782] : [-(_132782 = sziznziztdt0(_132006)), aVector0(_132782), szszuzczcdt0(aDimensionOf0(_132782)) = aDimensionOf0(_132006), 587 ^ _114949 : [(588 ^ _114949) ^ [] : [-(aNaturalNumber0(586 ^ [_132006, _132782]))], (590 ^ _114949) ^ [] : [sdtlbdtrb0(_132782, 586 ^ [_132006, _132782]) = sdtlbdtrb0(_132006, 586 ^ [_132006, _132782])]]]]], (594 ^ _114949) ^ [_133364, _133366] : [aVector0(_133366), aVector0(_133364), -(aDimensionOf0(sziznziztdt0(_133366)) = aDimensionOf0(sziznziztdt0(_133364))), aDimensionOf0(_133366) = aDimensionOf0(_133364), -(aDimensionOf0(_133364) = sz00)], (612 ^ _114949) ^ [_133870, _133872] : [aVector0(_133872), aVector0(_133870), aDimensionOf0(_133872) = aDimensionOf0(_133870), -(aScalar0(sdtasasdt0(_133872, _133870)))], (626 ^ _114949) ^ [_134268, _134270] : [aVector0(_134270), aVector0(_134268), -(sdtasasdt0(_134270, _134268) = sz0z00), aDimensionOf0(_134270) = aDimensionOf0(_134268), aDimensionOf0(_134268) = sz00], (644 ^ _114949) ^ [_134761, _134763] : [aVector0(_134763), aVector0(_134761), -(sdtasasdt0(_134763, _134761) = sdtpldt0(sdtasasdt0(sziznziztdt0(_134763), sziznziztdt0(_134761)), sdtasdt0(sdtlbdtrb0(_134763, aDimensionOf0(_134763)), sdtlbdtrb0(_134761, aDimensionOf0(_134761))))), aDimensionOf0(_134763) = aDimensionOf0(_134761), -(aDimensionOf0(_134761) = sz00)], (662 ^ _114949) ^ [_135289] : [aVector0(_135289), -(sdtlseqdt0(sz0z00, sdtasasdt0(_135289, _135289)))], (668 ^ _114949) ^ [] : [-(aVector0(xs))], (670 ^ _114949) ^ [] : [-(aVector0(xt))], (690 ^ _114949) ^ [] : [-(aDimensionOf0(xs) = aDimensionOf0(xt))], (692 ^ _114949) ^ [] : [aDimensionOf0(xs) = sz00], (694 ^ _114949) ^ [] : [-(aVector0(xp))], (696 ^ _114949) ^ [] : [-(szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs))], (704 ^ _114949) ^ [] : [-(xp = sziznziztdt0(xs))], (698 ^ _114949) ^ [_136345] : [aNaturalNumber0(_136345), -(sdtlbdtrb0(xp, _136345) = sdtlbdtrb0(xs, _136345))], (718 ^ _114949) ^ [] : [-(aScalar0(xA))], (720 ^ _114949) ^ [] : [-(xA = sdtlbdtrb0(xs, aDimensionOf0(xs)))], (722 ^ _114949) ^ [] : [-(aScalar0(xB))], (724 ^ _114949) ^ [] : [-(xB = sdtlbdtrb0(xt, aDimensionOf0(xt)))], (726 ^ _114949) ^ [] : [-(aScalar0(xC))], (728 ^ _114949) ^ [] : [-(xC = sdtasasdt0(xp, xp))], (730 ^ _114949) ^ [] : [-(aScalar0(xD))], (732 ^ _114949) ^ [] : [-(xD = sdtasasdt0(xq, xq))], (734 ^ _114949) ^ [] : [-(aScalar0(xE))], (736 ^ _114949) ^ [] : [-(xE = sdtasasdt0(xp, xq))], (738 ^ _114949) ^ [] : [-(aScalar0(xF))], (740 ^ _114949) ^ [] : [-(xF = sdtasdt0(xA, xA))], (742 ^ _114949) ^ [] : [-(aScalar0(xG))], (744 ^ _114949) ^ [] : [-(xG = sdtasdt0(xB, xB))], (746 ^ _114949) ^ [] : [-(aScalar0(xH))], (748 ^ _114949) ^ [] : [-(xH = sdtasdt0(xA, xB))], (750 ^ _114949) ^ [] : [-(aScalar0(xR))], (752 ^ _114949) ^ [] : [-(xR = sdtasdt0(xC, xG))], (754 ^ _114949) ^ [] : [-(aScalar0(xP))], (756 ^ _114949) ^ [] : [-(xP = sdtasdt0(xE, xH))], (758 ^ _114949) ^ [] : [-(aScalar0(xS))], (760 ^ _114949) ^ [] : [-(xS = sdtasdt0(xF, xD))], (762 ^ _114949) ^ [] : [-(aScalar0(xN))], (764 ^ _114949) ^ [] : [-(xN = sdtasdt0(xR, xS))], (766 ^ _114949) ^ [] : [-(sdtlseqdt0(sdtasdt0(xE, xE), sdtasdt0(xC, xD)))], (768 ^ _114949) ^ [] : [-(sdtlseqdt0(sdtasdt0(xP, xP), xN))], (770 ^ _114949) ^ [] : [-(sdtasdt0(xR, smndt0(xS)) = smndt0(xN))], (772 ^ _114949) ^ [] : [-(sdtasdt0(smndt0(xS), xR) = smndt0(xN))], (774 ^ _114949) ^ [] : [-(sdtasdt0(smndt0(xS), smndt0(xS)) = sdtasdt0(xS, xS))], (776 ^ _114949) ^ [] : [-(sdtasdt0(sdtpldt0(xR, smndt0(xS)), sdtpldt0(xR, smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(smndt0(xN), sdtasdt0(xS, xS))))], (706 ^ _114949) ^ [] : [-(aVector0(xq))], (708 ^ _114949) ^ [] : [-(szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt))], (716 ^ _114949) ^ [] : [-(xq = sziznziztdt0(xt))], (710 ^ _114949) ^ [_136710] : [aNaturalNumber0(_136710), -(sdtlbdtrb0(xq, _136710) = sdtlbdtrb0(xt, _136710))], (672 ^ _114949) ^ [_135605, _135607] : [aVector0(_135607), aVector0(_135605), aDimensionOf0(_135607) = aDimensionOf0(_135605), iLess0(aDimensionOf0(_135607), aDimensionOf0(xs)), -(sdtlseqdt0(sdtasdt0(sdtasasdt0(_135607, _135605), sdtasasdt0(_135607, _135605)), sdtasdt0(sdtasasdt0(_135607, _135607), sdtasasdt0(_135605, _135605))))]], input).
% 5.18/5.49 ncf('1',plain,[aNaturalNumber0(sz00), 160 : szszuzczcdt0(sz00) = sz00],start(154 ^ 0,bind([[_120096], [sz00]]))).
% 5.18/5.49 ncf('1.1',plain,[-(aNaturalNumber0(sz00))],extension(152 ^ 1)).
% 5.18/5.49 ncf('1.2',plain,[-(szszuzczcdt0(sz00) = sz00), 171 : -(aNaturalNumber0(169 ^ [szszuzczcdt0(sz00)])), 171 : aNaturalNumber0(szszuzczcdt0(sz00))],extension(162 ^ 3,bind([[_120364], [szszuzczcdt0(sz00)]]))).
% 5.18/5.49 ncf('1.2.1',plain,[aNaturalNumber0(169 ^ [szszuzczcdt0(sz00)]), -(aScalar0(sdtlbdtrb0(xs, 169 ^ [szszuzczcdt0(sz00)]))), aVector0(xs)],extension(545 ^ 6,bind([[_131721, _131723], [169 ^ [szszuzczcdt0(sz00)], xs]]))).
% 5.18/5.49 ncf('1.2.1.1',plain,[aScalar0(sdtlbdtrb0(xs, 169 ^ [szszuzczcdt0(sz00)])), 285 : -(sdtpldt0(smndt0(xN), sdtasdt0(xS, xS)) = sdtpldt0(sdtasdt0(xS, xS), smndt0(xN))), 285 : aScalar0(smndt0(xN)), 285 : aScalar0(sdtasdt0(xS, xS))],extension(271 ^ 7,bind([[_123687, _123689, _123691], [sdtlbdtrb0(xs, 169 ^ [szszuzczcdt0(sz00)]), sdtasdt0(xS, xS), smndt0(xN)]]))).
% 5.18/5.49 ncf('1.2.1.1.1',plain,[sdtpldt0(smndt0(xN), sdtasdt0(xS, xS)) = sdtpldt0(sdtasdt0(xS, xS), smndt0(xN)), -(sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(smndt0(xN), sdtasdt0(xS, xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(sdtasdt0(xS, xS), smndt0(xN)))), sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)) = sdtpldt0(sdtasdt0(xR, xR), smndt0(xN))],extension(116 ^ 10,bind([[_118884, _118886, _118888, _118890], [sdtpldt0(sdtasdt0(xS, xS), smndt0(xN)), sdtpldt0(smndt0(xN), sdtasdt0(xS, xS)), sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(sdtasdt0(xR, xR), smndt0(xN))]]))).
% 5.18/5.49 ncf('1.2.1.1.1.1',plain,[sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(smndt0(xN), sdtasdt0(xS, xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(sdtasdt0(xS, xS), smndt0(xN))), -(sdtasdt0(sdtpldt0(xR, smndt0(xS)), sdtpldt0(xR, smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(sdtasdt0(xS, xS), smndt0(xN)))), sdtasdt0(sdtpldt0(xR, smndt0(xS)), sdtpldt0(xR, smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(smndt0(xN), sdtasdt0(xS, xS)))],extension(10 ^ 11,bind([[_115404, _115406, _115408], [sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(sdtasdt0(xS, xS), smndt0(xN))), sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(smndt0(xN), sdtasdt0(xS, xS))), sdtasdt0(sdtpldt0(xR, smndt0(xS)), sdtpldt0(xR, smndt0(xS)))]]))).
% 5.18/5.49 ncf('1.2.1.1.1.1.1',plain,[sdtasdt0(sdtpldt0(xR, smndt0(xS)), sdtpldt0(xR, smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(sdtasdt0(xS, xS), smndt0(xN)))],extension(778 ^ 12)).
% 5.18/5.49 ncf('1.2.1.1.1.1.2',plain,[-(sdtasdt0(sdtpldt0(xR, smndt0(xS)), sdtpldt0(xR, smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(smndt0(xN), sdtasdt0(xS, xS))))],extension(776 ^ 12)).
% 5.18/5.49 ncf('1.2.1.1.1.2',plain,[-(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)) = sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)))],extension(2 ^ 11,bind([[_115093], [sdtpldt0(sdtasdt0(xR, xR), smndt0(xN))]]))).
% 5.18/5.49 ncf('1.2.1.1.2',plain,[-(aScalar0(smndt0(xN))), aScalar0(xN)],extension(245 ^ 8,bind([[_122730], [xN]]))).
% 5.18/5.49 ncf('1.2.1.1.2.1',plain,[-(aScalar0(xN))],extension(762 ^ 9)).
% 5.18/5.49 ncf('1.2.1.1.3',plain,[-(aScalar0(sdtasdt0(xS, xS))), aScalar0(xS), aScalar0(xS)],extension(235 ^ 8,bind([[_122445, _122447], [xS, xS]]))).
% 5.18/5.49 ncf('1.2.1.1.3.1',plain,[-(aScalar0(xS))],extension(758 ^ 9)).
% 5.18/5.49 ncf('1.2.1.1.3.2',plain,[-(aScalar0(xS))],lemmata('[1, 1, 2, 1].x')).
% 5.18/5.49 ncf('1.2.1.2',plain,[-(aVector0(xs))],extension(668 ^ 7)).
% 5.18/5.49 ncf('1.2.2',plain,[-(aNaturalNumber0(szszuzczcdt0(sz00)))],extension(158 ^ 4)).
% 5.18/5.49 %-----------------------------------------------------
% 5.18/5.49 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------