%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : RNG061+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:49:42 EDT 2023
% Result : Theorem 4.87s 5.43s
% Output : Proof 4.87s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.09 % Problem : RNG061+1 : TPTP v8.1.2. Released v4.0.0.
% 0.05/0.09 % Command : nanocop.sh %s %d
% 0.08/0.28 % Computer : n032.cluster.edu
% 0.08/0.28 % Model : x86_64 x86_64
% 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.28 % Memory : 8042.1875MB
% 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.28 % CPULimit : 300
% 0.08/0.28 % WCLimit : 300
% 0.08/0.28 % DateTime : Thu May 18 20:24:19 EDT 2023
% 0.08/0.28 % CPUTime :
% 4.87/5.43
% 4.87/5.43 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 4.87/5.43 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.87/5.43 %-----------------------------------------------------
% 4.87/5.43 ncf(matrix, plain, [(762 ^ _111906) ^ [] : [sdtasdt0(sdtpldt0(xR, smndt0(xS)), sdtpldt0(xR, smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(sdtasdt0(xS, xS), smndt0(xN)))], (78 ^ _111906) ^ [_114441, _114443] : [_114443 = _114441, -(szszuzczcdt0(_114443) = szszuzczcdt0(_114441))], (84 ^ _111906) ^ [_114659, _114661] : [_114661 = _114659, -(sziznziztdt0(_114661) = sziznziztdt0(_114659))], (90 ^ _111906) ^ [_114905, _114907, _114909, _114911] : [-(sdtlbdtrb0(_114911, _114907) = sdtlbdtrb0(_114909, _114905)), _114911 = _114909, _114907 = _114905], (100 ^ _111906) ^ [_115236, _115238] : [_115238 = _115236, -(aDimensionOf0(_115238) = aDimensionOf0(_115236))], (106 ^ _111906) ^ [_115482, _115484, _115486, _115488] : [-(sdtasasdt0(_115488, _115484) = sdtasasdt0(_115486, _115482)), _115488 = _115486, _115484 = _115482], (116 ^ _111906) ^ [_115841, _115843, _115845, _115847] : [-(sdtpldt0(_115847, _115843) = sdtpldt0(_115845, _115841)), _115847 = _115845, _115843 = _115841], (136 ^ _111906) ^ [_116511, _116513] : [_116513 = _116511, -(smndt0(_116513) = smndt0(_116511))], (126 ^ _111906) ^ [_116200, _116202, _116204, _116206] : [-(sdtasdt0(_116206, _116202) = sdtasdt0(_116204, _116200)), _116206 = _116204, _116202 = _116200], (2 ^ _111906) ^ [_112050] : [-(_112050 = _112050)], (4 ^ _111906) ^ [_112157, _112159] : [_112159 = _112157, -(_112157 = _112159)], (10 ^ _111906) ^ [_112361, _112363, _112365] : [-(_112365 = _112361), _112365 = _112363, _112363 = _112361], (20 ^ _111906) ^ [_112674, _112676] : [-(aNaturalNumber0(_112674)), _112676 = _112674, aNaturalNumber0(_112676)], (30 ^ _111906) ^ [_112997, _112999, _113001, _113003] : [-(iLess0(_113001, _112997)), iLess0(_113003, _112999), _113003 = _113001, _112999 = _112997], (44 ^ _111906) ^ [_113413, _113415] : [-(aVector0(_113413)), _113415 = _113413, aVector0(_113415)], (54 ^ _111906) ^ [_113708, _113710] : [-(aScalar0(_113708)), _113710 = _113708, aScalar0(_113710)], (64 ^ _111906) ^ [_114011, _114013, _114015, _114017] : [-(sdtlseqdt0(_114015, _114011)), sdtlseqdt0(_114017, _114013), _114017 = _114015, _114013 = _114011], (142 ^ _111906) ^ [_116745] : [aNaturalNumber0(_116745), true___, -(true___)], (152 ^ _111906) ^ [] : [-(aNaturalNumber0(sz00))], (154 ^ _111906) ^ [_117053] : [aNaturalNumber0(_117053), 157 ^ _111906 : [(158 ^ _111906) ^ [] : [-(aNaturalNumber0(szszuzczcdt0(_117053)))], (160 ^ _111906) ^ [] : [szszuzczcdt0(_117053) = sz00]]], (162 ^ _111906) ^ [_117321] : [170 ^ _111906 : [(171 ^ _111906) ^ [] : [-(aNaturalNumber0(169 ^ [_117321]))], (173 ^ _111906) ^ [] : [-(_117321 = szszuzczcdt0(169 ^ [_117321]))]], aNaturalNumber0(_117321), -(_117321 = sz00)], (175 ^ _111906) ^ [_117749, _117751] : [aNaturalNumber0(_117751), aNaturalNumber0(_117749), szszuzczcdt0(_117751) = szszuzczcdt0(_117749), -(_117751 = _117749)], (189 ^ _111906) ^ [_118143, _118145] : [aNaturalNumber0(_118145), aNaturalNumber0(_118143), iLess0(_118145, _118143), true___, -(true___)], (207 ^ _111906) ^ [_118589] : [aNaturalNumber0(_118589), -(iLess0(_118589, szszuzczcdt0(_118589)))], (213 ^ _111906) ^ [_118781] : [aScalar0(_118781), true___, -(true___)], (223 ^ _111906) ^ [] : [-(aScalar0(sz0z00))], (225 ^ _111906) ^ [_119103, _119105] : [-(aScalar0(sdtpldt0(_119105, _119103))), aScalar0(_119105), aScalar0(_119103)], (235 ^ _111906) ^ [_119402, _119404] : [-(aScalar0(sdtasdt0(_119404, _119402))), aScalar0(_119404), aScalar0(_119402)], (245 ^ _111906) ^ [_119687] : [aScalar0(_119687), -(aScalar0(smndt0(_119687)))], (251 ^ _111906) ^ [_119877] : [aScalar0(_119877), 254 ^ _111906 : [(255 ^ _111906) ^ [] : [-(sdtpldt0(_119877, sz0z00) = _119877)], (257 ^ _111906) ^ [] : [-(sdtpldt0(sz0z00, _119877) = _119877)], (259 ^ _111906) ^ [] : [-(sdtasdt0(_119877, sz0z00) = sz0z00)], (261 ^ _111906) ^ [] : [-(sdtasdt0(sz0z00, _119877) = sz0z00)], (263 ^ _111906) ^ [] : [-(sdtpldt0(_119877, smndt0(_119877)) = sz0z00)], (265 ^ _111906) ^ [] : [-(sdtpldt0(smndt0(_119877), _119877) = sz0z00)], (267 ^ _111906) ^ [] : [-(smndt0(smndt0(_119877)) = _119877)], (269 ^ _111906) ^ [] : [-(smndt0(sz0z00) = sz0z00)]]], (271 ^ _111906) ^ [_120644, _120646, _120648] : [282 ^ _111906 : [(283 ^ _111906) ^ [] : [-(sdtpldt0(sdtpldt0(_120648, _120646), _120644) = sdtpldt0(_120648, sdtpldt0(_120646, _120644)))], (285 ^ _111906) ^ [] : [-(sdtpldt0(_120648, _120646) = sdtpldt0(_120646, _120648))], (287 ^ _111906) ^ [] : [-(sdtasdt0(sdtasdt0(_120648, _120646), _120644) = sdtasdt0(_120648, sdtasdt0(_120646, _120644)))], (289 ^ _111906) ^ [] : [-(sdtasdt0(_120648, _120646) = sdtasdt0(_120646, _120648))]], aScalar0(_120648), aScalar0(_120646), aScalar0(_120644)], (291 ^ _111906) ^ [_121355, _121357, _121359] : [302 ^ _111906 : [(303 ^ _111906) ^ [] : [-(sdtasdt0(_121359, sdtpldt0(_121357, _121355)) = sdtpldt0(sdtasdt0(_121359, _121357), sdtasdt0(_121359, _121355)))], (305 ^ _111906) ^ [] : [-(sdtasdt0(sdtpldt0(_121359, _121357), _121355) = sdtpldt0(sdtasdt0(_121359, _121355), sdtasdt0(_121357, _121355)))]], aScalar0(_121359), aScalar0(_121357), aScalar0(_121355)], (307 ^ _111906) ^ [_121916, _121918, _121920, _121922] : [-(sdtasdt0(sdtpldt0(_121922, _121920), sdtpldt0(_121918, _121916)) = sdtpldt0(sdtpldt0(sdtasdt0(_121922, _121918), sdtasdt0(_121922, _121916)), sdtpldt0(sdtasdt0(_121920, _121918), sdtasdt0(_121920, _121916)))), aScalar0(_121922), aScalar0(_121920), aScalar0(_121918), aScalar0(_121916)], (325 ^ _111906) ^ [_122481, _122483] : [332 ^ _111906 : [(333 ^ _111906) ^ [] : [-(sdtasdt0(_122483, smndt0(_122481)) = smndt0(sdtasdt0(_122483, _122481)))], (335 ^ _111906) ^ [] : [-(sdtasdt0(smndt0(_122483), _122481) = smndt0(sdtasdt0(_122483, _122481)))]], aScalar0(_122483), aScalar0(_122481)], (337 ^ _111906) ^ [_122891, _122893] : [-(sdtasdt0(smndt0(_122893), smndt0(_122891)) = sdtasdt0(_122893, _122891)), aScalar0(_122893), aScalar0(_122891)], (347 ^ _111906) ^ [_123206, _123208] : [aScalar0(_123208), aScalar0(_123206), sdtlseqdt0(_123208, _123206), true___, -(true___)], (365 ^ _111906) ^ [_123652] : [aScalar0(_123652), -(sdtlseqdt0(_123652, _123652))], (371 ^ _111906) ^ [_123854, _123856] : [aScalar0(_123856), aScalar0(_123854), -(_123856 = _123854), sdtlseqdt0(_123856, _123854), sdtlseqdt0(_123854, _123856)], (389 ^ _111906) ^ [_124343, _124345, _124347] : [aScalar0(_124347), aScalar0(_124345), aScalar0(_124343), -(sdtlseqdt0(_124347, _124343)), sdtlseqdt0(_124347, _124345), sdtlseqdt0(_124345, _124343)], (411 ^ _111906) ^ [_124957, _124959, _124961, _124963] : [-(sdtlseqdt0(sdtpldt0(_124963, _124959), sdtpldt0(_124961, _124957))), sdtlseqdt0(_124963, _124961), sdtlseqdt0(_124959, _124957), aScalar0(_124963), aScalar0(_124961), aScalar0(_124959), aScalar0(_124957)], (437 ^ _111906) ^ [_125700, _125702, _125704, _125706] : [aScalar0(_125706), aScalar0(_125704), aScalar0(_125702), aScalar0(_125700), -(sdtlseqdt0(sdtasdt0(_125706, _125702), sdtasdt0(_125704, _125700))), sdtlseqdt0(_125706, _125704), sdtlseqdt0(sz0z00, _125702), sdtlseqdt0(_125702, _125700)], (467 ^ _111906) ^ [_126514, _126516] : [aScalar0(_126516), aScalar0(_126514), -(sdtlseqdt0(_126516, _126514)), -(sdtlseqdt0(_126514, _126516))], (481 ^ _111906) ^ [_126901, _126903] : [aScalar0(_126903), aScalar0(_126901), 496 ^ _111906 : [(497 ^ _111906) ^ [] : [-(sdtlseqdt0(sz0z00, sdtpldt0(_126903, _126901)))], (499 ^ _111906) ^ [] : [-(sdtlseqdt0(sz0z00, sdtasdt0(_126903, _126901)))]], sdtlseqdt0(sz0z00, _126903), sdtlseqdt0(sz0z00, _126901)], (501 ^ _111906) ^ [_127449] : [aScalar0(_127449), -(sdtlseqdt0(sz0z00, sdtasdt0(_127449, _127449)))], (507 ^ _111906) ^ [_127657, _127659] : [aScalar0(_127659), aScalar0(_127657), -(_127659 = _127657), sdtlseqdt0(sz0z00, _127659), sdtlseqdt0(sz0z00, _127657), sdtasdt0(_127659, _127659) = sdtasdt0(_127657, _127657)], (529 ^ _111906) ^ [_128219] : [aVector0(_128219), true___, -(true___)], (539 ^ _111906) ^ [_128474] : [aVector0(_128474), -(aNaturalNumber0(aDimensionOf0(_128474)))], (545 ^ _111906) ^ [_128678, _128680] : [-(aScalar0(sdtlbdtrb0(_128680, _128678))), aVector0(_128680), aNaturalNumber0(_128678)], (555 ^ _111906) ^ [_128963] : [aVector0(_128963), -(aDimensionOf0(_128963) = sz00), 562 ^ _111906 : [(563 ^ _111906) ^ [_129246] : [_129246 = sziznziztdt0(_128963), 566 ^ _111906 : [(567 ^ _111906) ^ [] : [-(aVector0(_129246))], (569 ^ _111906) ^ [] : [-(szszuzczcdt0(aDimensionOf0(_129246)) = aDimensionOf0(_128963))], (571 ^ _111906) ^ [_129548] : [aNaturalNumber0(_129548), -(sdtlbdtrb0(_129246, _129548) = sdtlbdtrb0(_128963, _129548))]]], (577 ^ _111906) ^ [_129739] : [-(_129739 = sziznziztdt0(_128963)), aVector0(_129739), szszuzczcdt0(aDimensionOf0(_129739)) = aDimensionOf0(_128963), 587 ^ _111906 : [(588 ^ _111906) ^ [] : [-(aNaturalNumber0(586 ^ [_128963, _129739]))], (590 ^ _111906) ^ [] : [sdtlbdtrb0(_129739, 586 ^ [_128963, _129739]) = sdtlbdtrb0(_128963, 586 ^ [_128963, _129739])]]]]], (594 ^ _111906) ^ [_130321, _130323] : [aVector0(_130323), aVector0(_130321), -(aDimensionOf0(sziznziztdt0(_130323)) = aDimensionOf0(sziznziztdt0(_130321))), aDimensionOf0(_130323) = aDimensionOf0(_130321), -(aDimensionOf0(_130321) = sz00)], (612 ^ _111906) ^ [_130827, _130829] : [aVector0(_130829), aVector0(_130827), aDimensionOf0(_130829) = aDimensionOf0(_130827), -(aScalar0(sdtasasdt0(_130829, _130827)))], (626 ^ _111906) ^ [_131225, _131227] : [aVector0(_131227), aVector0(_131225), -(sdtasasdt0(_131227, _131225) = sz0z00), aDimensionOf0(_131227) = aDimensionOf0(_131225), aDimensionOf0(_131225) = sz00], (644 ^ _111906) ^ [_131718, _131720] : [aVector0(_131720), aVector0(_131718), -(sdtasasdt0(_131720, _131718) = sdtpldt0(sdtasasdt0(sziznziztdt0(_131720), sziznziztdt0(_131718)), sdtasdt0(sdtlbdtrb0(_131720, aDimensionOf0(_131720)), sdtlbdtrb0(_131718, aDimensionOf0(_131718))))), aDimensionOf0(_131720) = aDimensionOf0(_131718), -(aDimensionOf0(_131718) = sz00)], (662 ^ _111906) ^ [_132246] : [aVector0(_132246), -(sdtlseqdt0(sz0z00, sdtasasdt0(_132246, _132246)))], (668 ^ _111906) ^ [] : [-(aVector0(xs))], (670 ^ _111906) ^ [] : [-(aVector0(xt))], (690 ^ _111906) ^ [] : [-(aDimensionOf0(xs) = aDimensionOf0(xt))], (692 ^ _111906) ^ [] : [aDimensionOf0(xs) = sz00], (694 ^ _111906) ^ [] : [-(aVector0(xp))], (696 ^ _111906) ^ [] : [-(xp = sziznziztdt0(xs))], (698 ^ _111906) ^ [] : [-(aVector0(xq))], (700 ^ _111906) ^ [] : [-(xq = sziznziztdt0(xt))], (702 ^ _111906) ^ [] : [-(aScalar0(xA))], (704 ^ _111906) ^ [] : [-(xA = sdtlbdtrb0(xs, aDimensionOf0(xs)))], (706 ^ _111906) ^ [] : [-(aScalar0(xB))], (708 ^ _111906) ^ [] : [-(xB = sdtlbdtrb0(xt, aDimensionOf0(xt)))], (710 ^ _111906) ^ [] : [-(aScalar0(xC))], (712 ^ _111906) ^ [] : [-(xC = sdtasasdt0(xp, xp))], (714 ^ _111906) ^ [] : [-(aScalar0(xD))], (716 ^ _111906) ^ [] : [-(xD = sdtasasdt0(xq, xq))], (718 ^ _111906) ^ [] : [-(aScalar0(xE))], (720 ^ _111906) ^ [] : [-(xE = sdtasasdt0(xp, xq))], (722 ^ _111906) ^ [] : [-(aScalar0(xF))], (724 ^ _111906) ^ [] : [-(xF = sdtasdt0(xA, xA))], (726 ^ _111906) ^ [] : [-(aScalar0(xG))], (728 ^ _111906) ^ [] : [-(xG = sdtasdt0(xB, xB))], (730 ^ _111906) ^ [] : [-(aScalar0(xH))], (732 ^ _111906) ^ [] : [-(xH = sdtasdt0(xA, xB))], (734 ^ _111906) ^ [] : [-(aScalar0(xR))], (736 ^ _111906) ^ [] : [-(xR = sdtasdt0(xC, xG))], (738 ^ _111906) ^ [] : [-(aScalar0(xP))], (740 ^ _111906) ^ [] : [-(xP = sdtasdt0(xE, xH))], (742 ^ _111906) ^ [] : [-(aScalar0(xS))], (744 ^ _111906) ^ [] : [-(xS = sdtasdt0(xF, xD))], (746 ^ _111906) ^ [] : [-(aScalar0(xN))], (748 ^ _111906) ^ [] : [-(xN = sdtasdt0(xR, xS))], (750 ^ _111906) ^ [] : [-(sdtlseqdt0(sdtasdt0(xE, xE), sdtasdt0(xC, xD)))], (752 ^ _111906) ^ [] : [-(sdtlseqdt0(sdtasdt0(xP, xP), xN))], (754 ^ _111906) ^ [] : [-(sdtasdt0(xR, smndt0(xS)) = smndt0(xN))], (756 ^ _111906) ^ [] : [-(sdtasdt0(smndt0(xS), xR) = smndt0(xN))], (758 ^ _111906) ^ [] : [-(sdtasdt0(smndt0(xS), smndt0(xS)) = sdtasdt0(xS, xS))], (760 ^ _111906) ^ [] : [-(sdtasdt0(sdtpldt0(xR, smndt0(xS)), sdtpldt0(xR, smndt0(xS))) = sdtpldt0(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(smndt0(xN), sdtasdt0(xS, xS))))], (672 ^ _111906) ^ [_132562, _132564] : [aVector0(_132564), aVector0(_132562), aDimensionOf0(_132564) = aDimensionOf0(_132562), iLess0(aDimensionOf0(_132564), aDimensionOf0(xs)), -(sdtlseqdt0(sdtasdt0(sdtasasdt0(_132564, _132562), sdtasasdt0(_132564, _132562)), sdtasdt0(sdtasasdt0(_132564, _132564), sdtasasdt0(_132562, _132562))))]], input).
% 4.87/5.43 ncf('1',plain,[aNaturalNumber0(sz00), 160 : szszuzczcdt0(sz00) = sz00],start(154 ^ 0,bind([[_117053], [sz00]]))).
% 4.87/5.43 ncf('1.1',plain,[-(aNaturalNumber0(sz00))],extension(152 ^ 1)).
% 4.87/5.43 ncf('1.2',plain,[-(szszuzczcdt0(sz00) = sz00), 171 : -(aNaturalNumber0(169 ^ [szszuzczcdt0(sz00)])), 171 : aNaturalNumber0(szszuzczcdt0(sz00))],extension(162 ^ 3,bind([[_117321], [szszuzczcdt0(sz00)]]))).
% 4.87/5.43 ncf('1.2.1',plain,[aNaturalNumber0(169 ^ [szszuzczcdt0(sz00)]), -(aScalar0(sdtlbdtrb0(xs, 169 ^ [szszuzczcdt0(sz00)]))), aVector0(xs)],extension(545 ^ 6,bind([[_128678, _128680], [169 ^ [szszuzczcdt0(sz00)], xs]]))).
% 4.87/5.43 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([[_120644, _120646, _120648], [sdtlbdtrb0(xs, 169 ^ [szszuzczcdt0(sz00)]), sdtasdt0(xS, xS), smndt0(xN)]]))).
% 4.87/5.43 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([[_115841, _115843, _115845, _115847], [sdtpldt0(sdtasdt0(xS, xS), smndt0(xN)), sdtpldt0(smndt0(xN), sdtasdt0(xS, xS)), sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)), sdtpldt0(sdtasdt0(xR, xR), smndt0(xN))]]))).
% 4.87/5.43 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([[_112361, _112363, _112365], [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)))]]))).
% 4.87/5.43 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(762 ^ 12)).
% 4.87/5.43 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(760 ^ 12)).
% 4.87/5.43 ncf('1.2.1.1.1.2',plain,[-(sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)) = sdtpldt0(sdtasdt0(xR, xR), smndt0(xN)))],extension(2 ^ 11,bind([[_112050], [sdtpldt0(sdtasdt0(xR, xR), smndt0(xN))]]))).
% 4.87/5.43 ncf('1.2.1.1.2',plain,[-(aScalar0(smndt0(xN))), aScalar0(xN)],extension(245 ^ 8,bind([[_119687], [xN]]))).
% 4.87/5.43 ncf('1.2.1.1.2.1',plain,[-(aScalar0(xN))],extension(746 ^ 9)).
% 4.87/5.43 ncf('1.2.1.1.3',plain,[-(aScalar0(sdtasdt0(xS, xS))), aScalar0(xS), aScalar0(xS)],extension(235 ^ 8,bind([[_119402, _119404], [xS, xS]]))).
% 4.87/5.43 ncf('1.2.1.1.3.1',plain,[-(aScalar0(xS))],extension(742 ^ 9)).
% 4.87/5.43 ncf('1.2.1.1.3.2',plain,[-(aScalar0(xS))],lemmata('[1, 1, 2, 1].x')).
% 4.87/5.43 ncf('1.2.1.2',plain,[-(aVector0(xs))],extension(668 ^ 7)).
% 4.87/5.43 ncf('1.2.2',plain,[-(aNaturalNumber0(szszuzczcdt0(sz00)))],extension(158 ^ 4)).
% 4.87/5.43 %-----------------------------------------------------
% 4.87/5.43 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------