%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : RNG072+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n001.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:44 EDT 2023
% Result : Theorem 0.33s 1.37s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : RNG072+1 : TPTP v8.1.2. Released v4.0.0.
% 0.06/0.13 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n001.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 18 20:56:35 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.33/1.37
% 0.33/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.33/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 ncf(matrix, plain, [(766 ^ _111249) ^ [] : [sdtlseqdt0(sdtasdt0(sdtpldt0(xR, xS), sdtpldt0(xR, xS)), sdtasdt0(sdtpldt0(xP, xP), sdtpldt0(xP, xP)))], (78 ^ _111249) ^ [_113784, _113786] : [_113786 = _113784, -(smndt0(_113786) = smndt0(_113784))], (84 ^ _111249) ^ [_114002, _114004] : [_114004 = _114002, -(szszuzczcdt0(_114004) = szszuzczcdt0(_114002))], (90 ^ _111249) ^ [_114220, _114222] : [_114222 = _114220, -(sziznziztdt0(_114222) = sziznziztdt0(_114220))], (96 ^ _111249) ^ [_114466, _114468, _114470, _114472] : [-(sdtlbdtrb0(_114472, _114468) = sdtlbdtrb0(_114470, _114466)), _114472 = _114470, _114468 = _114466], (106 ^ _111249) ^ [_114797, _114799] : [_114799 = _114797, -(aDimensionOf0(_114799) = aDimensionOf0(_114797))], (112 ^ _111249) ^ [_115043, _115045, _115047, _115049] : [-(sdtasasdt0(_115049, _115045) = sdtasasdt0(_115047, _115043)), _115049 = _115047, _115045 = _115043], (122 ^ _111249) ^ [_115402, _115404, _115406, _115408] : [-(sdtasdt0(_115408, _115404) = sdtasdt0(_115406, _115402)), _115408 = _115406, _115404 = _115402], (132 ^ _111249) ^ [_115741, _115743, _115745, _115747] : [-(sdtpldt0(_115747, _115743) = sdtpldt0(_115745, _115741)), _115747 = _115745, _115743 = _115741], (2 ^ _111249) ^ [_111393] : [-(_111393 = _111393)], (4 ^ _111249) ^ [_111500, _111502] : [_111502 = _111500, -(_111500 = _111502)], (10 ^ _111249) ^ [_111704, _111706, _111708] : [-(_111708 = _111704), _111708 = _111706, _111706 = _111704], (20 ^ _111249) ^ [_112017, _112019] : [-(aNaturalNumber0(_112017)), _112019 = _112017, aNaturalNumber0(_112019)], (30 ^ _111249) ^ [_112340, _112342, _112344, _112346] : [-(iLess0(_112344, _112340)), iLess0(_112346, _112342), _112346 = _112344, _112342 = _112340], (44 ^ _111249) ^ [_112756, _112758] : [-(aVector0(_112756)), _112758 = _112756, aVector0(_112758)], (54 ^ _111249) ^ [_113051, _113053] : [-(aScalar0(_113051)), _113053 = _113051, aScalar0(_113053)], (64 ^ _111249) ^ [_113354, _113356, _113358, _113360] : [-(sdtlseqdt0(_113358, _113354)), sdtlseqdt0(_113360, _113356), _113360 = _113358, _113356 = _113354], (142 ^ _111249) ^ [_116088] : [aNaturalNumber0(_116088), true___, -(true___)], (152 ^ _111249) ^ [] : [-(aNaturalNumber0(sz00))], (154 ^ _111249) ^ [_116396] : [aNaturalNumber0(_116396), 157 ^ _111249 : [(158 ^ _111249) ^ [] : [-(aNaturalNumber0(szszuzczcdt0(_116396)))], (160 ^ _111249) ^ [] : [szszuzczcdt0(_116396) = sz00]]], (162 ^ _111249) ^ [_116664] : [170 ^ _111249 : [(171 ^ _111249) ^ [] : [-(aNaturalNumber0(169 ^ [_116664]))], (173 ^ _111249) ^ [] : [-(_116664 = szszuzczcdt0(169 ^ [_116664]))]], aNaturalNumber0(_116664), -(_116664 = sz00)], (175 ^ _111249) ^ [_117092, _117094] : [aNaturalNumber0(_117094), aNaturalNumber0(_117092), szszuzczcdt0(_117094) = szszuzczcdt0(_117092), -(_117094 = _117092)], (189 ^ _111249) ^ [_117486, _117488] : [aNaturalNumber0(_117488), aNaturalNumber0(_117486), iLess0(_117488, _117486), true___, -(true___)], (207 ^ _111249) ^ [_117932] : [aNaturalNumber0(_117932), -(iLess0(_117932, szszuzczcdt0(_117932)))], (213 ^ _111249) ^ [_118124] : [aScalar0(_118124), true___, -(true___)], (223 ^ _111249) ^ [] : [-(aScalar0(sz0z00))], (225 ^ _111249) ^ [_118446, _118448] : [-(aScalar0(sdtpldt0(_118448, _118446))), aScalar0(_118448), aScalar0(_118446)], (235 ^ _111249) ^ [_118745, _118747] : [-(aScalar0(sdtasdt0(_118747, _118745))), aScalar0(_118747), aScalar0(_118745)], (245 ^ _111249) ^ [_119030] : [aScalar0(_119030), -(aScalar0(smndt0(_119030)))], (251 ^ _111249) ^ [_119220] : [aScalar0(_119220), 254 ^ _111249 : [(255 ^ _111249) ^ [] : [-(sdtpldt0(_119220, sz0z00) = _119220)], (257 ^ _111249) ^ [] : [-(sdtpldt0(sz0z00, _119220) = _119220)], (259 ^ _111249) ^ [] : [-(sdtasdt0(_119220, sz0z00) = sz0z00)], (261 ^ _111249) ^ [] : [-(sdtasdt0(sz0z00, _119220) = sz0z00)], (263 ^ _111249) ^ [] : [-(sdtpldt0(_119220, smndt0(_119220)) = sz0z00)], (265 ^ _111249) ^ [] : [-(sdtpldt0(smndt0(_119220), _119220) = sz0z00)], (267 ^ _111249) ^ [] : [-(smndt0(smndt0(_119220)) = _119220)], (269 ^ _111249) ^ [] : [-(smndt0(sz0z00) = sz0z00)]]], (271 ^ _111249) ^ [_119987, _119989, _119991] : [282 ^ _111249 : [(283 ^ _111249) ^ [] : [-(sdtpldt0(sdtpldt0(_119991, _119989), _119987) = sdtpldt0(_119991, sdtpldt0(_119989, _119987)))], (285 ^ _111249) ^ [] : [-(sdtpldt0(_119991, _119989) = sdtpldt0(_119989, _119991))], (287 ^ _111249) ^ [] : [-(sdtasdt0(sdtasdt0(_119991, _119989), _119987) = sdtasdt0(_119991, sdtasdt0(_119989, _119987)))], (289 ^ _111249) ^ [] : [-(sdtasdt0(_119991, _119989) = sdtasdt0(_119989, _119991))]], aScalar0(_119991), aScalar0(_119989), aScalar0(_119987)], (291 ^ _111249) ^ [_120698, _120700, _120702] : [302 ^ _111249 : [(303 ^ _111249) ^ [] : [-(sdtasdt0(_120702, sdtpldt0(_120700, _120698)) = sdtpldt0(sdtasdt0(_120702, _120700), sdtasdt0(_120702, _120698)))], (305 ^ _111249) ^ [] : [-(sdtasdt0(sdtpldt0(_120702, _120700), _120698) = sdtpldt0(sdtasdt0(_120702, _120698), sdtasdt0(_120700, _120698)))]], aScalar0(_120702), aScalar0(_120700), aScalar0(_120698)], (307 ^ _111249) ^ [_121259, _121261, _121263, _121265] : [-(sdtasdt0(sdtpldt0(_121265, _121263), sdtpldt0(_121261, _121259)) = sdtpldt0(sdtpldt0(sdtasdt0(_121265, _121261), sdtasdt0(_121265, _121259)), sdtpldt0(sdtasdt0(_121263, _121261), sdtasdt0(_121263, _121259)))), aScalar0(_121265), aScalar0(_121263), aScalar0(_121261), aScalar0(_121259)], (325 ^ _111249) ^ [_121824, _121826] : [332 ^ _111249 : [(333 ^ _111249) ^ [] : [-(sdtasdt0(_121826, smndt0(_121824)) = smndt0(sdtasdt0(_121826, _121824)))], (335 ^ _111249) ^ [] : [-(sdtasdt0(smndt0(_121826), _121824) = smndt0(sdtasdt0(_121826, _121824)))]], aScalar0(_121826), aScalar0(_121824)], (337 ^ _111249) ^ [_122234, _122236] : [-(sdtasdt0(smndt0(_122236), smndt0(_122234)) = sdtasdt0(_122236, _122234)), aScalar0(_122236), aScalar0(_122234)], (347 ^ _111249) ^ [_122549, _122551] : [aScalar0(_122551), aScalar0(_122549), sdtlseqdt0(_122551, _122549), true___, -(true___)], (365 ^ _111249) ^ [_122995] : [aScalar0(_122995), -(sdtlseqdt0(_122995, _122995))], (371 ^ _111249) ^ [_123197, _123199] : [aScalar0(_123199), aScalar0(_123197), -(_123199 = _123197), sdtlseqdt0(_123199, _123197), sdtlseqdt0(_123197, _123199)], (389 ^ _111249) ^ [_123686, _123688, _123690] : [aScalar0(_123690), aScalar0(_123688), aScalar0(_123686), -(sdtlseqdt0(_123690, _123686)), sdtlseqdt0(_123690, _123688), sdtlseqdt0(_123688, _123686)], (411 ^ _111249) ^ [_124300, _124302, _124304, _124306] : [-(sdtlseqdt0(sdtpldt0(_124306, _124302), sdtpldt0(_124304, _124300))), sdtlseqdt0(_124306, _124304), sdtlseqdt0(_124302, _124300), aScalar0(_124306), aScalar0(_124304), aScalar0(_124302), aScalar0(_124300)], (437 ^ _111249) ^ [_125043, _125045, _125047, _125049] : [aScalar0(_125049), aScalar0(_125047), aScalar0(_125045), aScalar0(_125043), -(sdtlseqdt0(sdtasdt0(_125049, _125045), sdtasdt0(_125047, _125043))), sdtlseqdt0(_125049, _125047), sdtlseqdt0(sz0z00, _125045), sdtlseqdt0(_125045, _125043)], (467 ^ _111249) ^ [_125857, _125859] : [aScalar0(_125859), aScalar0(_125857), -(sdtlseqdt0(_125859, _125857)), -(sdtlseqdt0(_125857, _125859))], (481 ^ _111249) ^ [_126244, _126246] : [aScalar0(_126246), aScalar0(_126244), 496 ^ _111249 : [(497 ^ _111249) ^ [] : [-(sdtlseqdt0(sz0z00, sdtpldt0(_126246, _126244)))], (499 ^ _111249) ^ [] : [-(sdtlseqdt0(sz0z00, sdtasdt0(_126246, _126244)))]], sdtlseqdt0(sz0z00, _126246), sdtlseqdt0(sz0z00, _126244)], (501 ^ _111249) ^ [_126792] : [aScalar0(_126792), -(sdtlseqdt0(sz0z00, sdtasdt0(_126792, _126792)))], (507 ^ _111249) ^ [_127000, _127002] : [aScalar0(_127002), aScalar0(_127000), -(_127002 = _127000), sdtlseqdt0(sz0z00, _127002), sdtlseqdt0(sz0z00, _127000), sdtasdt0(_127002, _127002) = sdtasdt0(_127000, _127000)], (529 ^ _111249) ^ [_127562] : [aVector0(_127562), true___, -(true___)], (539 ^ _111249) ^ [_127817] : [aVector0(_127817), -(aNaturalNumber0(aDimensionOf0(_127817)))], (545 ^ _111249) ^ [_128021, _128023] : [-(aScalar0(sdtlbdtrb0(_128023, _128021))), aVector0(_128023), aNaturalNumber0(_128021)], (555 ^ _111249) ^ [_128306] : [aVector0(_128306), -(aDimensionOf0(_128306) = sz00), 562 ^ _111249 : [(563 ^ _111249) ^ [_128589] : [_128589 = sziznziztdt0(_128306), 566 ^ _111249 : [(567 ^ _111249) ^ [] : [-(aVector0(_128589))], (569 ^ _111249) ^ [] : [-(szszuzczcdt0(aDimensionOf0(_128589)) = aDimensionOf0(_128306))], (571 ^ _111249) ^ [_128891] : [aNaturalNumber0(_128891), -(sdtlbdtrb0(_128589, _128891) = sdtlbdtrb0(_128306, _128891))]]], (577 ^ _111249) ^ [_129082] : [-(_129082 = sziznziztdt0(_128306)), aVector0(_129082), szszuzczcdt0(aDimensionOf0(_129082)) = aDimensionOf0(_128306), 587 ^ _111249 : [(588 ^ _111249) ^ [] : [-(aNaturalNumber0(586 ^ [_128306, _129082]))], (590 ^ _111249) ^ [] : [sdtlbdtrb0(_129082, 586 ^ [_128306, _129082]) = sdtlbdtrb0(_128306, 586 ^ [_128306, _129082])]]]]], (594 ^ _111249) ^ [_129664, _129666] : [aVector0(_129666), aVector0(_129664), -(aDimensionOf0(sziznziztdt0(_129666)) = aDimensionOf0(sziznziztdt0(_129664))), aDimensionOf0(_129666) = aDimensionOf0(_129664), -(aDimensionOf0(_129664) = sz00)], (612 ^ _111249) ^ [_130170, _130172] : [aVector0(_130172), aVector0(_130170), aDimensionOf0(_130172) = aDimensionOf0(_130170), -(aScalar0(sdtasasdt0(_130172, _130170)))], (626 ^ _111249) ^ [_130568, _130570] : [aVector0(_130570), aVector0(_130568), -(sdtasasdt0(_130570, _130568) = sz0z00), aDimensionOf0(_130570) = aDimensionOf0(_130568), aDimensionOf0(_130568) = sz00], (644 ^ _111249) ^ [_131061, _131063] : [aVector0(_131063), aVector0(_131061), -(sdtasasdt0(_131063, _131061) = sdtpldt0(sdtasasdt0(sziznziztdt0(_131063), sziznziztdt0(_131061)), sdtasdt0(sdtlbdtrb0(_131063, aDimensionOf0(_131063)), sdtlbdtrb0(_131061, aDimensionOf0(_131061))))), aDimensionOf0(_131063) = aDimensionOf0(_131061), -(aDimensionOf0(_131061) = sz00)], (662 ^ _111249) ^ [_131589] : [aVector0(_131589), -(sdtlseqdt0(sz0z00, sdtasasdt0(_131589, _131589)))], (668 ^ _111249) ^ [] : [-(aVector0(xs))], (670 ^ _111249) ^ [] : [-(aVector0(xt))], (690 ^ _111249) ^ [] : [-(aDimensionOf0(xs) = aDimensionOf0(xt))], (692 ^ _111249) ^ [] : [aDimensionOf0(xs) = sz00], (694 ^ _111249) ^ [] : [-(aVector0(xp))], (696 ^ _111249) ^ [] : [-(xp = sziznziztdt0(xs))], (698 ^ _111249) ^ [] : [-(aVector0(xq))], (700 ^ _111249) ^ [] : [-(xq = sziznziztdt0(xt))], (702 ^ _111249) ^ [] : [-(aScalar0(xA))], (704 ^ _111249) ^ [] : [-(xA = sdtlbdtrb0(xs, aDimensionOf0(xs)))], (706 ^ _111249) ^ [] : [-(aScalar0(xB))], (708 ^ _111249) ^ [] : [-(xB = sdtlbdtrb0(xt, aDimensionOf0(xt)))], (710 ^ _111249) ^ [] : [-(aScalar0(xC))], (712 ^ _111249) ^ [] : [-(xC = sdtasasdt0(xp, xp))], (714 ^ _111249) ^ [] : [-(aScalar0(xD))], (716 ^ _111249) ^ [] : [-(xD = sdtasasdt0(xq, xq))], (718 ^ _111249) ^ [] : [-(aScalar0(xE))], (720 ^ _111249) ^ [] : [-(xE = sdtasasdt0(xp, xq))], (722 ^ _111249) ^ [] : [-(aScalar0(xF))], (724 ^ _111249) ^ [] : [-(xF = sdtasdt0(xA, xA))], (726 ^ _111249) ^ [] : [-(aScalar0(xG))], (728 ^ _111249) ^ [] : [-(xG = sdtasdt0(xB, xB))], (730 ^ _111249) ^ [] : [-(aScalar0(xH))], (732 ^ _111249) ^ [] : [-(xH = sdtasdt0(xA, xB))], (734 ^ _111249) ^ [] : [-(aScalar0(xR))], (736 ^ _111249) ^ [] : [-(xR = sdtasdt0(xC, xG))], (738 ^ _111249) ^ [] : [-(aScalar0(xP))], (740 ^ _111249) ^ [] : [-(xP = sdtasdt0(xE, xH))], (742 ^ _111249) ^ [] : [-(aScalar0(xS))], (744 ^ _111249) ^ [] : [-(xS = sdtasdt0(xF, xD))], (746 ^ _111249) ^ [] : [-(aScalar0(xN))], (748 ^ _111249) ^ [] : [-(xN = sdtasdt0(xR, xS))], (750 ^ _111249) ^ [] : [-(sdtlseqdt0(sdtasdt0(xE, xE), sdtasdt0(xC, xD)))], (752 ^ _111249) ^ [] : [-(sdtlseqdt0(sdtasdt0(xP, xP), xN))], (754 ^ _111249) ^ [] : [-(sdtlseqdt0(sdtpldt0(sdtasdt0(xP, xP), sdtasdt0(xP, xP)), sdtpldt0(sdtasdt0(xR, xR), sdtasdt0(xS, xS))))], (756 ^ _111249) ^ [] : [-(sdtlseqdt0(sdtasdt0(sdtpldt0(xP, xP), sdtpldt0(xP, xP)), sdtasdt0(sdtpldt0(xR, xS), sdtpldt0(xR, xS))))], (758 ^ _111249) ^ [] : [sdtlseqdt0(sdtpldt0(xP, xP), sdtpldt0(xR, xS))], (760 ^ _111249) ^ [] : [-(sdtlseqdt0(sdtpldt0(xR, xS), sdtpldt0(xP, xP)))], (762 ^ _111249) ^ [] : [-(sdtlseqdt0(sz0z00, sdtpldt0(xR, xS)))], (764 ^ _111249) ^ [] : [-(sdtlseqdt0(sz0z00, sdtpldt0(xP, xP)))], (672 ^ _111249) ^ [_131905, _131907] : [aVector0(_131907), aVector0(_131905), aDimensionOf0(_131907) = aDimensionOf0(_131905), iLess0(aDimensionOf0(_131907), aDimensionOf0(xs)), -(sdtlseqdt0(sdtasdt0(sdtasasdt0(_131907, _131905), sdtasasdt0(_131907, _131905)), sdtasdt0(sdtasasdt0(_131907, _131907), sdtasasdt0(_131905, _131905))))]], input).
% 0.33/1.37 ncf('1',plain,[sdtlseqdt0(sdtasdt0(sdtpldt0(xR, xS), sdtpldt0(xR, xS)), sdtasdt0(sdtpldt0(xP, xP), sdtpldt0(xP, xP)))],start(766 ^ 0)).
% 0.33/1.37 ncf('1.1',plain,[-(sdtlseqdt0(sdtasdt0(sdtpldt0(xR, xS), sdtpldt0(xR, xS)), sdtasdt0(sdtpldt0(xP, xP), sdtpldt0(xP, xP)))), aScalar0(sdtpldt0(xR, xS)), aScalar0(sdtpldt0(xP, xP)), aScalar0(sdtpldt0(xR, xS)), aScalar0(sdtpldt0(xP, xP)), sdtlseqdt0(sdtpldt0(xR, xS), sdtpldt0(xP, xP)), sdtlseqdt0(sz0z00, sdtpldt0(xR, xS)), sdtlseqdt0(sdtpldt0(xR, xS), sdtpldt0(xP, xP))],extension(437 ^ 1,bind([[_125043, _125045, _125047, _125049], [sdtpldt0(xP, xP), sdtpldt0(xR, xS), sdtpldt0(xP, xP), sdtpldt0(xR, xS)]]))).
% 0.33/1.37 ncf('1.1.1',plain,[-(aScalar0(sdtpldt0(xR, xS))), aScalar0(xR), aScalar0(xS)],extension(225 ^ 2,bind([[_118446, _118448], [xS, xR]]))).
% 0.33/1.37 ncf('1.1.1.1',plain,[-(aScalar0(xR))],extension(734 ^ 3)).
% 0.33/1.37 ncf('1.1.1.2',plain,[-(aScalar0(xS))],extension(742 ^ 3)).
% 0.33/1.37 ncf('1.1.2',plain,[-(aScalar0(sdtpldt0(xP, xP))), aScalar0(xP), aScalar0(xP)],extension(225 ^ 2,bind([[_118446, _118448], [xP, xP]]))).
% 0.33/1.37 ncf('1.1.2.1',plain,[-(aScalar0(xP))],extension(738 ^ 3)).
% 0.33/1.37 ncf('1.1.2.2',plain,[-(aScalar0(xP))],lemmata('[1, 1].x')).
% 0.33/1.37 ncf('1.1.3',plain,[-(aScalar0(sdtpldt0(xR, xS)))],lemmata('[1].x')).
% 0.33/1.37 ncf('1.1.4',plain,[-(aScalar0(sdtpldt0(xP, xP)))],lemmata('[1].x')).
% 0.33/1.37 ncf('1.1.5',plain,[-(sdtlseqdt0(sdtpldt0(xR, xS), sdtpldt0(xP, xP))), aScalar0(sdtpldt0(xR, xS)), aScalar0(sdtpldt0(xP, xP)), -(sdtlseqdt0(sdtpldt0(xP, xP), sdtpldt0(xR, xS)))],extension(467 ^ 2,bind([[_125857, _125859], [sdtpldt0(xP, xP), sdtpldt0(xR, xS)]]))).
% 0.33/1.37 ncf('1.1.5.1',plain,[-(aScalar0(sdtpldt0(xR, xS)))],lemmata('[1].x')).
% 0.33/1.37 ncf('1.1.5.2',plain,[-(aScalar0(sdtpldt0(xP, xP)))],lemmata('[1].x')).
% 0.33/1.37 ncf('1.1.5.3',plain,[sdtlseqdt0(sdtpldt0(xP, xP), sdtpldt0(xR, xS))],extension(758 ^ 3)).
% 0.33/1.37 ncf('1.1.6',plain,[-(sdtlseqdt0(sz0z00, sdtpldt0(xR, xS)))],extension(762 ^ 2)).
% 0.33/1.37 ncf('1.1.7',plain,[-(sdtlseqdt0(sdtpldt0(xR, xS), sdtpldt0(xP, xP)))],lemmata('[1].x')).
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------