%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM520+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n024.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:51 EDT 2023
% Result : Theorem 0.37s 1.38s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM520+3 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n024.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 16:42:36 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.37/1.38
% 0.37/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.37/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/1.38 %-----------------------------------------------------
% 0.37/1.38 ncf(matrix, plain, [(959 ^ _126250) ^ [_155756] : [aNaturalNumber0(_155756), xn = sdtasdt0(xp, _155756)], (965 ^ _126250) ^ [] : [doDivides0(xp, xn)], (973 ^ _126250) ^ [] : [doDivides0(xp, xm)], (967 ^ _126250) ^ [_156001] : [aNaturalNumber0(_156001), xm = sdtasdt0(xp, _156001)], (82 ^ _126250) ^ [_128962, _128964, _128966, _128968] : [-(sdtmndt0(_128968, _128964) = sdtmndt0(_128966, _128962)), _128968 = _128966, _128964 = _128962], (92 ^ _126250) ^ [_129321, _129323, _129325, _129327] : [-(sdtpldt0(_129327, _129323) = sdtpldt0(_129325, _129321)), _129327 = _129325, _129323 = _129321], (102 ^ _126250) ^ [_129680, _129682, _129684, _129686] : [-(sdtsldt0(_129686, _129682) = sdtsldt0(_129684, _129680)), _129686 = _129684, _129682 = _129680], (112 ^ _126250) ^ [_130019, _130021, _130023, _130025] : [-(sdtasdt0(_130025, _130021) = sdtasdt0(_130023, _130019)), _130025 = _130023, _130021 = _130019], (2 ^ _126250) ^ [_126394] : [-(_126394 = _126394)], (4 ^ _126250) ^ [_126501, _126503] : [_126503 = _126501, -(_126501 = _126503)], (10 ^ _126250) ^ [_126705, _126707, _126709] : [-(_126709 = _126705), _126709 = _126707, _126707 = _126705], (20 ^ _126250) ^ [_127046, _127048, _127050, _127052] : [-(iLess0(_127050, _127046)), iLess0(_127052, _127048), _127052 = _127050, _127048 = _127046], (34 ^ _126250) ^ [_127462, _127464] : [-(isPrime0(_127462)), _127464 = _127462, isPrime0(_127464)], (44 ^ _126250) ^ [_127785, _127787, _127789, _127791] : [-(sdtlseqdt0(_127789, _127785)), sdtlseqdt0(_127791, _127787), _127791 = _127789, _127787 = _127785], (58 ^ _126250) ^ [_128201, _128203] : [-(aNaturalNumber0(_128201)), _128203 = _128201, aNaturalNumber0(_128203)], (68 ^ _126250) ^ [_128504, _128506, _128508, _128510] : [-(doDivides0(_128508, _128504)), doDivides0(_128510, _128506), _128510 = _128508, _128506 = _128504], (122 ^ _126250) ^ [_130350] : [aNaturalNumber0(_130350), true___, -(true___)], (132 ^ _126250) ^ [] : [-(aNaturalNumber0(sz00))], (134 ^ _126250) ^ [] : [-(aNaturalNumber0(sz10))], (136 ^ _126250) ^ [] : [sz10 = sz00], (138 ^ _126250) ^ [_130779, _130781] : [-(aNaturalNumber0(sdtpldt0(_130781, _130779))), aNaturalNumber0(_130781), aNaturalNumber0(_130779)], (148 ^ _126250) ^ [_131078, _131080] : [-(aNaturalNumber0(sdtasdt0(_131080, _131078))), aNaturalNumber0(_131080), aNaturalNumber0(_131078)], (158 ^ _126250) ^ [_131377, _131379] : [-(sdtpldt0(_131379, _131377) = sdtpldt0(_131377, _131379)), aNaturalNumber0(_131379), aNaturalNumber0(_131377)], (168 ^ _126250) ^ [_131698, _131700, _131702] : [-(sdtpldt0(sdtpldt0(_131702, _131700), _131698) = sdtpldt0(_131702, sdtpldt0(_131700, _131698))), aNaturalNumber0(_131702), aNaturalNumber0(_131700), aNaturalNumber0(_131698)], (182 ^ _126250) ^ [_132104] : [aNaturalNumber0(_132104), 185 ^ _126250 : [(186 ^ _126250) ^ [] : [-(sdtpldt0(_132104, sz00) = _132104)], (188 ^ _126250) ^ [] : [-(_132104 = sdtpldt0(sz00, _132104))]]], (190 ^ _126250) ^ [_132391, _132393] : [-(sdtasdt0(_132393, _132391) = sdtasdt0(_132391, _132393)), aNaturalNumber0(_132393), aNaturalNumber0(_132391)], (200 ^ _126250) ^ [_132712, _132714, _132716] : [-(sdtasdt0(sdtasdt0(_132716, _132714), _132712) = sdtasdt0(_132716, sdtasdt0(_132714, _132712))), aNaturalNumber0(_132716), aNaturalNumber0(_132714), aNaturalNumber0(_132712)], (214 ^ _126250) ^ [_133118] : [aNaturalNumber0(_133118), 217 ^ _126250 : [(218 ^ _126250) ^ [] : [-(sdtasdt0(_133118, sz10) = _133118)], (220 ^ _126250) ^ [] : [-(_133118 = sdtasdt0(sz10, _133118))]]], (222 ^ _126250) ^ [_133391] : [aNaturalNumber0(_133391), 225 ^ _126250 : [(226 ^ _126250) ^ [] : [-(sdtasdt0(_133391, sz00) = sz00)], (228 ^ _126250) ^ [] : [-(sz00 = sdtasdt0(sz00, _133391))]]], (230 ^ _126250) ^ [_133692, _133694, _133696] : [241 ^ _126250 : [(242 ^ _126250) ^ [] : [-(sdtasdt0(_133696, sdtpldt0(_133694, _133692)) = sdtpldt0(sdtasdt0(_133696, _133694), sdtasdt0(_133696, _133692)))], (244 ^ _126250) ^ [] : [-(sdtasdt0(sdtpldt0(_133694, _133692), _133696) = sdtpldt0(sdtasdt0(_133694, _133696), sdtasdt0(_133692, _133696)))]], aNaturalNumber0(_133696), aNaturalNumber0(_133694), aNaturalNumber0(_133692)], (246 ^ _126250) ^ [_134239, _134241, _134243] : [259 ^ _126250 : [(260 ^ _126250) ^ [] : [sdtpldt0(_134243, _134241) = sdtpldt0(_134243, _134239)], (262 ^ _126250) ^ [] : [sdtpldt0(_134241, _134243) = sdtpldt0(_134239, _134243)]], -(_134241 = _134239), aNaturalNumber0(_134243), aNaturalNumber0(_134241), aNaturalNumber0(_134239)], (266 ^ _126250) ^ [_134816] : [aNaturalNumber0(_134816), -(_134816 = sz00), 273 ^ _126250 : [(274 ^ _126250) ^ [_135078, _135080] : [aNaturalNumber0(_135080), aNaturalNumber0(_135078), 283 ^ _126250 : [(284 ^ _126250) ^ [] : [sdtasdt0(_134816, _135080) = sdtasdt0(_134816, _135078)], (286 ^ _126250) ^ [] : [sdtasdt0(_135080, _134816) = sdtasdt0(_135078, _134816)]], -(_135080 = _135078)]]], (290 ^ _126250) ^ [_135589, _135591] : [aNaturalNumber0(_135591), aNaturalNumber0(_135589), sdtpldt0(_135591, _135589) = sz00, 301 ^ _126250 : [(302 ^ _126250) ^ [] : [-(_135591 = sz00)], (304 ^ _126250) ^ [] : [-(_135589 = sz00)]]], (306 ^ _126250) ^ [_136056, _136058] : [aNaturalNumber0(_136058), aNaturalNumber0(_136056), sdtasdt0(_136058, _136056) = sz00, -(_136058 = sz00), -(_136056 = sz00)], (324 ^ _126250) ^ [_136538, _136540] : [aNaturalNumber0(_136540), aNaturalNumber0(_136538), 331 ^ _126250 : [(332 ^ _126250) ^ [] : [sdtlseqdt0(_136540, _136538), 336 ^ _126250 : [(337 ^ _126250) ^ [] : [-(aNaturalNumber0(335 ^ [_136538, _136540]))], (339 ^ _126250) ^ [] : [-(sdtpldt0(_136540, 335 ^ [_136538, _136540]) = _136538)]]], (341 ^ _126250) ^ [] : [-(sdtlseqdt0(_136540, _136538)), 342 ^ _126250 : [(343 ^ _126250) ^ [_137098] : [aNaturalNumber0(_137098), sdtpldt0(_136540, _137098) = _136538]]]]], (351 ^ _126250) ^ [_137381, _137383] : [aNaturalNumber0(_137383), aNaturalNumber0(_137381), sdtlseqdt0(_137383, _137381), 362 ^ _126250 : [(363 ^ _126250) ^ [_137728] : [_137728 = sdtmndt0(_137381, _137383), 366 ^ _126250 : [(367 ^ _126250) ^ [] : [-(aNaturalNumber0(_137728))], (369 ^ _126250) ^ [] : [-(sdtpldt0(_137383, _137728) = _137381)]]], (371 ^ _126250) ^ [_137987] : [-(_137987 = sdtmndt0(_137381, _137383)), aNaturalNumber0(_137987), sdtpldt0(_137383, _137987) = _137381]]], (381 ^ _126250) ^ [_138309] : [aNaturalNumber0(_138309), -(sdtlseqdt0(_138309, _138309))], (387 ^ _126250) ^ [_138511, _138513] : [aNaturalNumber0(_138513), aNaturalNumber0(_138511), -(_138513 = _138511), sdtlseqdt0(_138513, _138511), sdtlseqdt0(_138511, _138513)], (405 ^ _126250) ^ [_139000, _139002, _139004] : [aNaturalNumber0(_139004), aNaturalNumber0(_139002), aNaturalNumber0(_139000), -(sdtlseqdt0(_139004, _139000)), sdtlseqdt0(_139004, _139002), sdtlseqdt0(_139002, _139000)], (427 ^ _126250) ^ [_139586, _139588] : [aNaturalNumber0(_139588), aNaturalNumber0(_139586), -(sdtlseqdt0(_139588, _139586)), 438 ^ _126250 : [(439 ^ _126250) ^ [] : [_139586 = _139588], (441 ^ _126250) ^ [] : [-(sdtlseqdt0(_139586, _139588))]]], (443 ^ _126250) ^ [_140049, _140051] : [aNaturalNumber0(_140051), aNaturalNumber0(_140049), -(_140051 = _140049), sdtlseqdt0(_140051, _140049), 458 ^ _126250 : [(459 ^ _126250) ^ [_140493] : [aNaturalNumber0(_140493), 462 ^ _126250 : [(463 ^ _126250) ^ [] : [sdtpldt0(_140493, _140051) = sdtpldt0(_140493, _140049)], (465 ^ _126250) ^ [] : [-(sdtlseqdt0(sdtpldt0(_140493, _140051), sdtpldt0(_140493, _140049)))], (467 ^ _126250) ^ [] : [sdtpldt0(_140051, _140493) = sdtpldt0(_140049, _140493)], (469 ^ _126250) ^ [] : [-(sdtlseqdt0(sdtpldt0(_140051, _140493), sdtpldt0(_140049, _140493)))]]]]], (471 ^ _126250) ^ [_141017, _141019, _141021] : [aNaturalNumber0(_141021), aNaturalNumber0(_141019), aNaturalNumber0(_141017), 494 ^ _126250 : [(495 ^ _126250) ^ [] : [sdtasdt0(_141021, _141019) = sdtasdt0(_141021, _141017)], (497 ^ _126250) ^ [] : [-(sdtlseqdt0(sdtasdt0(_141021, _141019), sdtasdt0(_141021, _141017)))], (499 ^ _126250) ^ [] : [sdtasdt0(_141019, _141021) = sdtasdt0(_141017, _141021)], (501 ^ _126250) ^ [] : [-(sdtlseqdt0(sdtasdt0(_141019, _141021), sdtasdt0(_141017, _141021)))]], -(_141021 = sz00), -(_141019 = _141017), sdtlseqdt0(_141019, _141017)], (503 ^ _126250) ^ [_141967] : [aNaturalNumber0(_141967), -(_141967 = sz00), -(_141967 = sz10), 514 ^ _126250 : [(515 ^ _126250) ^ [] : [sz10 = _141967], (517 ^ _126250) ^ [] : [-(sdtlseqdt0(sz10, _141967))]]], (519 ^ _126250) ^ [_142415, _142417] : [aNaturalNumber0(_142417), aNaturalNumber0(_142415), -(_142417 = sz00), -(sdtlseqdt0(_142415, sdtasdt0(_142415, _142417)))], (533 ^ _126250) ^ [_142810, _142812] : [aNaturalNumber0(_142812), aNaturalNumber0(_142810), iLess0(_142812, _142810), true___, -(true___)], (551 ^ _126250) ^ [_143270, _143272] : [aNaturalNumber0(_143272), aNaturalNumber0(_143270), -(iLess0(_143272, _143270)), -(_143272 = _143270), sdtlseqdt0(_143272, _143270)], (569 ^ _126250) ^ [_143748, _143750] : [aNaturalNumber0(_143750), aNaturalNumber0(_143748), 576 ^ _126250 : [(577 ^ _126250) ^ [] : [doDivides0(_143750, _143748), 581 ^ _126250 : [(582 ^ _126250) ^ [] : [-(aNaturalNumber0(580 ^ [_143748, _143750]))], (584 ^ _126250) ^ [] : [-(_143748 = sdtasdt0(_143750, 580 ^ [_143748, _143750]))]]], (586 ^ _126250) ^ [] : [-(doDivides0(_143750, _143748)), 587 ^ _126250 : [(588 ^ _126250) ^ [_144308] : [aNaturalNumber0(_144308), _143748 = sdtasdt0(_143750, _144308)]]]]], (596 ^ _126250) ^ [_144591, _144593] : [aNaturalNumber0(_144593), aNaturalNumber0(_144591), -(_144593 = sz00), doDivides0(_144593, _144591), 611 ^ _126250 : [(612 ^ _126250) ^ [_145030] : [_145030 = sdtsldt0(_144591, _144593), 615 ^ _126250 : [(616 ^ _126250) ^ [] : [-(aNaturalNumber0(_145030))], (618 ^ _126250) ^ [] : [-(_144591 = sdtasdt0(_144593, _145030))]]], (620 ^ _126250) ^ [_145289] : [-(_145289 = sdtsldt0(_144591, _144593)), aNaturalNumber0(_145289), _144591 = sdtasdt0(_144593, _145289)]]], (630 ^ _126250) ^ [_145641, _145643, _145645] : [aNaturalNumber0(_145645), aNaturalNumber0(_145643), aNaturalNumber0(_145641), -(doDivides0(_145645, _145641)), doDivides0(_145645, _145643), doDivides0(_145643, _145641)], (652 ^ _126250) ^ [_146241, _146243, _146245] : [aNaturalNumber0(_146245), aNaturalNumber0(_146243), aNaturalNumber0(_146241), -(doDivides0(_146245, sdtpldt0(_146243, _146241))), doDivides0(_146245, _146243), doDivides0(_146245, _146241)], (674 ^ _126250) ^ [_146847, _146849, _146851] : [aNaturalNumber0(_146851), aNaturalNumber0(_146849), aNaturalNumber0(_146847), -(doDivides0(_146851, _146847)), doDivides0(_146851, _146849), doDivides0(_146851, sdtpldt0(_146849, _146847))], (696 ^ _126250) ^ [_147439, _147441] : [aNaturalNumber0(_147441), aNaturalNumber0(_147439), -(sdtlseqdt0(_147441, _147439)), doDivides0(_147441, _147439), -(_147439 = sz00)], (714 ^ _126250) ^ [_147917, _147919] : [aNaturalNumber0(_147919), aNaturalNumber0(_147917), -(_147919 = sz00), doDivides0(_147919, _147917), 729 ^ _126250 : [(730 ^ _126250) ^ [_148327] : [aNaturalNumber0(_148327), -(sdtasdt0(_148327, sdtsldt0(_147917, _147919)) = sdtsldt0(sdtasdt0(_148327, _147917), _147919))]]], (736 ^ _126250) ^ [_148568] : [aNaturalNumber0(_148568), 739 ^ _126250 : [(762 ^ _126250) ^ [] : [-(isPrime0(_148568)), -(_148568 = sz00), -(_148568 = sz10), 772 ^ _126250 : [(773 ^ _126250) ^ [] : [-(aNaturalNumber0(771 ^ [_148568]))], (775 ^ _126250) ^ [] : [-(doDivides0(771 ^ [_148568], _148568))], (777 ^ _126250) ^ [] : [771 ^ [_148568] = sz10], (779 ^ _126250) ^ [] : [771 ^ [_148568] = _148568]]], (740 ^ _126250) ^ [] : [isPrime0(_148568), 743 ^ _126250 : [(744 ^ _126250) ^ [] : [_148568 = sz00], (746 ^ _126250) ^ [] : [_148568 = sz10], (748 ^ _126250) ^ [_148960] : [aNaturalNumber0(_148960), doDivides0(_148960, _148568), -(_148960 = sz10), -(_148960 = _148568)]]]]], (783 ^ _126250) ^ [_149912] : [795 ^ _126250 : [(796 ^ _126250) ^ [] : [-(aNaturalNumber0(794 ^ [_149912]))], (798 ^ _126250) ^ [] : [-(doDivides0(794 ^ [_149912], _149912))], (800 ^ _126250) ^ [] : [-(isPrime0(794 ^ [_149912]))]], aNaturalNumber0(_149912), -(_149912 = sz00), -(_149912 = sz10)], (802 ^ _126250) ^ [] : [-(aNaturalNumber0(xn))], (804 ^ _126250) ^ [] : [-(aNaturalNumber0(xm))], (806 ^ _126250) ^ [] : [-(aNaturalNumber0(xp))], (808 ^ _126250) ^ [_150679, _150681, _150683] : [aNaturalNumber0(_150683), aNaturalNumber0(_150681), aNaturalNumber0(_150679), iLess0(sdtpldt0(sdtpldt0(_150683, _150681), _150679), sdtpldt0(sdtpldt0(xn, xm), xp)), 862 ^ _126250 : [(863 ^ _126250) ^ [] : [-(aNaturalNumber0(861 ^ [_150679, _150681, _150683]))], (865 ^ _126250) ^ [] : [-(_150683 = sdtasdt0(_150679, 861 ^ [_150679, _150681, _150683]))], (867 ^ _126250) ^ [] : [-(doDivides0(_150679, _150683))]], 869 ^ _126250 : [(870 ^ _126250) ^ [] : [-(aNaturalNumber0(868 ^ [_150679, _150681, _150683]))], (872 ^ _126250) ^ [] : [-(_150681 = sdtasdt0(_150679, 868 ^ [_150679, _150681, _150683]))], (874 ^ _126250) ^ [] : [-(doDivides0(_150679, _150681))]], 847 ^ _126250 : [(854 ^ _126250) ^ [] : [doDivides0(_150679, sdtasdt0(_150683, _150681))], (848 ^ _126250) ^ [_152100] : [aNaturalNumber0(_152100), sdtasdt0(_150683, _150681) = sdtasdt0(_150679, _152100)]], 823 ^ _126250 : [(846 ^ _126250) ^ [] : [isPrime0(_150679)], (824 ^ _126250) ^ [] : [-(_150679 = sz00), -(_150679 = sz10), 832 ^ _126250 : [(833 ^ _126250) ^ [] : [-(aNaturalNumber0(831 ^ [_150679, _150681, _150683]))], (836 ^ _126250) ^ [] : [-(aNaturalNumber0(834 ^ [_150679, _150681, _150683]))], (838 ^ _126250) ^ [] : [-(_150679 = sdtasdt0(831 ^ [_150679, _150681, _150683], 834 ^ [_150679, _150681, _150683]))], (840 ^ _126250) ^ [] : [-(doDivides0(831 ^ [_150679, _150681, _150683], _150679))], (842 ^ _126250) ^ [] : [831 ^ [_150679, _150681, _150683] = sz10], (844 ^ _126250) ^ [] : [831 ^ [_150679, _150681, _150683] = _150679]]]]], (876 ^ _126250) ^ [] : [xp = sz00], (878 ^ _126250) ^ [] : [xp = sz10], (900 ^ _126250) ^ [] : [-(isPrime0(xp))], (903 ^ _126250) ^ [] : [-(aNaturalNumber0(901 ^ []))], (905 ^ _126250) ^ [] : [-(sdtasdt0(xn, xm) = sdtasdt0(xp, 901 ^ []))], (907 ^ _126250) ^ [] : [-(doDivides0(xp, sdtasdt0(xn, xm)))], (880 ^ _126250) ^ [_153190] : [-(_153190 = sz10), -(_153190 = xp), aNaturalNumber0(_153190), 885 ^ _126250 : [(892 ^ _126250) ^ [] : [doDivides0(_153190, xp)], (886 ^ _126250) ^ [_153393] : [aNaturalNumber0(_153393), xp = sdtasdt0(_153190, _153393)]]], (915 ^ _126250) ^ [] : [sdtlseqdt0(xp, xn)], (909 ^ _126250) ^ [_154051] : [aNaturalNumber0(_154051), sdtpldt0(xp, _154051) = xn], (923 ^ _126250) ^ [] : [sdtlseqdt0(xp, xm)], (917 ^ _126250) ^ [_154298] : [aNaturalNumber0(_154298), sdtpldt0(xp, _154298) = xm], (925 ^ _126250) ^ [] : [xn = xp], (928 ^ _126250) ^ [] : [-(aNaturalNumber0(926 ^ []))], (930 ^ _126250) ^ [] : [-(sdtpldt0(xn, 926 ^ []) = xp)], (932 ^ _126250) ^ [] : [-(sdtlseqdt0(xn, xp))], (934 ^ _126250) ^ [] : [xm = xp], (937 ^ _126250) ^ [] : [-(aNaturalNumber0(935 ^ []))], (939 ^ _126250) ^ [] : [-(sdtpldt0(xm, 935 ^ []) = xp)], (941 ^ _126250) ^ [] : [-(sdtlseqdt0(xm, xp))], (943 ^ _126250) ^ [] : [-(aNaturalNumber0(xk))], (945 ^ _126250) ^ [] : [-(sdtasdt0(xn, xm) = sdtasdt0(xp, xk))], (947 ^ _126250) ^ [] : [-(xk = sdtsldt0(sdtasdt0(xn, xm), xp))], (949 ^ _126250) ^ [] : [xk = sz00], (951 ^ _126250) ^ [] : [xk = sz10], (953 ^ _126250) ^ [] : [-(xk = sz00), -(xk = sz10)]], input).
% 0.37/1.38 ncf('1',plain,[xk = sz00],start(949 ^ 0)).
% 0.37/1.38 ncf('1.1',plain,[-(xk = sz00), -(xk = sz10)],extension(953 ^ 1)).
% 0.37/1.38 ncf('1.1.1',plain,[xk = sz10],extension(951 ^ 2)).
% 0.37/1.38 %-----------------------------------------------------
% 0.37/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------