%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : RNG091+2 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n005.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:48 EDT 2023
% Result : Theorem 102.57s 99.58s
% Output : Proof 102.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : RNG091+2 : TPTP v8.1.2. Released v4.0.0.
% 0.00/0.09 % Command : nanocop.sh %s %d
% 0.08/0.28 % Computer : n005.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:18:53 EDT 2023
% 0.08/0.28 % CPUTime :
% 102.57/99.58
% 102.57/99.58 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 102.57/99.58 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 102.57/99.58 %-----------------------------------------------------
% 102.57/99.58 ncf(matrix, plain, [(579 ^ _84802) ^ [] : [580 ^ _84802 : [(591 ^ _84802) ^ [] : [aElementOf0(sdtpldt0(xx, xy), sdtpldt1(xI, xJ))], (581 ^ _84802) ^ [_104525, _104527] : [aElementOf0(_104527, xI), aElementOf0(_104525, xJ), sdtpldt0(_104527, _104525) = sdtpldt0(xx, xy)]], 592 ^ _84802 : [(603 ^ _84802) ^ [] : [aElementOf0(sdtasdt0(xz, xx), sdtpldt1(xI, xJ))], (593 ^ _84802) ^ [_104863, _104865] : [aElementOf0(_104865, xI), aElementOf0(_104863, xJ), sdtpldt0(_104865, _104863) = sdtasdt0(xz, xx)]]], (64 ^ _84802) ^ [_86891, _86893] : [_86893 = _86891, -(smndt0(_86893) = smndt0(_86891))], (70 ^ _84802) ^ [_87137, _87139, _87141, _87143] : [-(sdtasasdt0(_87143, _87139) = sdtasasdt0(_87141, _87137)), _87143 = _87141, _87139 = _87137], (80 ^ _84802) ^ [_87496, _87498, _87500, _87502] : [-(sdtpldt0(_87502, _87498) = sdtpldt0(_87500, _87496)), _87502 = _87500, _87498 = _87496], (90 ^ _84802) ^ [_87855, _87857, _87859, _87861] : [-(sdtasdt0(_87861, _87857) = sdtasdt0(_87859, _87855)), _87861 = _87859, _87857 = _87855], (100 ^ _84802) ^ [_88194, _88196, _88198, _88200] : [-(sdtpldt1(_88200, _88196) = sdtpldt1(_88198, _88194)), _88200 = _88198, _88196 = _88194], (2 ^ _84802) ^ [_84946] : [-(_84946 = _84946)], (4 ^ _84802) ^ [_85053, _85055] : [_85055 = _85053, -(_85053 = _85055)], (10 ^ _84802) ^ [_85257, _85259, _85261] : [-(_85261 = _85257), _85261 = _85259, _85259 = _85257], (20 ^ _84802) ^ [_85570, _85572] : [-(aSet0(_85570)), _85572 = _85570, aSet0(_85572)], (30 ^ _84802) ^ [_85865, _85867] : [-(aIdeal0(_85865)), _85867 = _85865, aIdeal0(_85867)], (40 ^ _84802) ^ [_86160, _86162] : [-(aElement0(_86160)), _86162 = _86160, aElement0(_86162)], (50 ^ _84802) ^ [_86463, _86465, _86467, _86469] : [-(aElementOf0(_86467, _86463)), aElementOf0(_86469, _86465), _86469 = _86467, _86465 = _86463], (110 ^ _84802) ^ [_88529] : [aElement0(_88529), true___, -(true___)], (120 ^ _84802) ^ [] : [-(aElement0(sz00))], (122 ^ _84802) ^ [] : [-(aElement0(sz10))], (124 ^ _84802) ^ [_88890] : [aElement0(_88890), -(aElement0(smndt0(_88890)))], (130 ^ _84802) ^ [_89094, _89096] : [-(aElement0(sdtpldt0(_89096, _89094))), aElement0(_89096), aElement0(_89094)], (140 ^ _84802) ^ [_89393, _89395] : [-(aElement0(sdtasdt0(_89395, _89393))), aElement0(_89395), aElement0(_89393)], (150 ^ _84802) ^ [_89692, _89694] : [-(sdtpldt0(_89694, _89692) = sdtpldt0(_89692, _89694)), aElement0(_89694), aElement0(_89692)], (160 ^ _84802) ^ [_90013, _90015, _90017] : [-(sdtpldt0(sdtpldt0(_90017, _90015), _90013) = sdtpldt0(_90017, sdtpldt0(_90015, _90013))), aElement0(_90017), aElement0(_90015), aElement0(_90013)], (174 ^ _84802) ^ [_90419] : [aElement0(_90419), 177 ^ _84802 : [(178 ^ _84802) ^ [] : [-(sdtpldt0(_90419, sz00) = _90419)], (180 ^ _84802) ^ [] : [-(_90419 = sdtpldt0(sz00, _90419))]]], (182 ^ _84802) ^ [_90692] : [aElement0(_90692), 185 ^ _84802 : [(186 ^ _84802) ^ [] : [-(sdtpldt0(_90692, smndt0(_90692)) = sz00)], (188 ^ _84802) ^ [] : [-(sz00 = sdtpldt0(smndt0(_90692), _90692))]]], (190 ^ _84802) ^ [_90987, _90989] : [-(sdtasdt0(_90989, _90987) = sdtasdt0(_90987, _90989)), aElement0(_90989), aElement0(_90987)], (200 ^ _84802) ^ [_91308, _91310, _91312] : [-(sdtasdt0(sdtasdt0(_91312, _91310), _91308) = sdtasdt0(_91312, sdtasdt0(_91310, _91308))), aElement0(_91312), aElement0(_91310), aElement0(_91308)], (214 ^ _84802) ^ [_91714] : [aElement0(_91714), 217 ^ _84802 : [(218 ^ _84802) ^ [] : [-(sdtasdt0(_91714, sz10) = _91714)], (220 ^ _84802) ^ [] : [-(_91714 = sdtasdt0(sz10, _91714))]]], (222 ^ _84802) ^ [_92015, _92017, _92019] : [233 ^ _84802 : [(234 ^ _84802) ^ [] : [-(sdtasdt0(_92019, sdtpldt0(_92017, _92015)) = sdtpldt0(sdtasdt0(_92019, _92017), sdtasdt0(_92019, _92015)))], (236 ^ _84802) ^ [] : [-(sdtasdt0(sdtpldt0(_92017, _92015), _92019) = sdtpldt0(sdtasdt0(_92017, _92019), sdtasdt0(_92015, _92019)))]], aElement0(_92019), aElement0(_92017), aElement0(_92015)], (238 ^ _84802) ^ [_92534] : [aElement0(_92534), 241 ^ _84802 : [(242 ^ _84802) ^ [] : [-(sdtasdt0(smndt0(sz10), _92534) = smndt0(_92534))], (244 ^ _84802) ^ [] : [-(smndt0(_92534) = sdtasdt0(_92534, smndt0(sz10)))]]], (246 ^ _84802) ^ [_92815] : [aElement0(_92815), 249 ^ _84802 : [(250 ^ _84802) ^ [] : [-(sdtasdt0(_92815, sz00) = sz00)], (252 ^ _84802) ^ [] : [-(sz00 = sdtasdt0(sz00, _92815))]]], (254 ^ _84802) ^ [_93102, _93104] : [aElement0(_93104), aElement0(_93102), sdtasdt0(_93104, _93102) = sz00, -(_93104 = sz00), -(_93102 = sz00)], (272 ^ _84802) ^ [] : [sz10 = sz00], (274 ^ _84802) ^ [_93622] : [aSet0(_93622), true___, -(true___)], (284 ^ _84802) ^ [_93877] : [aSet0(_93877), 287 ^ _84802 : [(288 ^ _84802) ^ [_94007] : [aElementOf0(_94007, _93877), -(aElement0(_94007))]]], (294 ^ _84802) ^ [_94222, _94224] : [aSet0(_94224), aSet0(_94222), -(_94224 = _94222), 306 ^ _84802 : [(307 ^ _84802) ^ [] : [-(aElementOf0(305 ^ [_94222, _94224], _94224))], (309 ^ _84802) ^ [] : [aElementOf0(305 ^ [_94222, _94224], _94222)]], 311 ^ _84802 : [(312 ^ _84802) ^ [] : [-(aElementOf0(310 ^ [_94222, _94224], _94222))], (314 ^ _84802) ^ [] : [aElementOf0(310 ^ [_94222, _94224], _94224)]]], (318 ^ _84802) ^ [_94987, _94989] : [aSet0(_94989), aSet0(_94987), 325 ^ _84802 : [(358 ^ _84802) ^ [_96617] : [-(_96617 = sdtpldt1(_94989, _94987)), aSet0(_96617), 380 ^ _84802 : [(381 ^ _84802) ^ [] : [-(aElementOf0(378 ^ [_94987, _94989, _96617], _94989))], (383 ^ _84802) ^ [] : [-(aElementOf0(379 ^ [_94987, _94989, _96617], _94987))], (385 ^ _84802) ^ [] : [-(sdtpldt0(378 ^ [_94987, _94989, _96617], 379 ^ [_94987, _94989, _96617]) = 363 ^ [_94987, _94989, _96617])], (387 ^ _84802) ^ [] : [aElementOf0(363 ^ [_94987, _94989, _96617], _96617)]], 366 ^ _84802 : [(367 ^ _84802) ^ [] : [-(aElementOf0(363 ^ [_94987, _94989, _96617], _96617))], (369 ^ _84802) ^ [_97046, _97048] : [aElementOf0(_97048, _94989), aElementOf0(_97046, _94987), sdtpldt0(_97048, _97046) = 363 ^ [_94987, _94989, _96617]]]], (326 ^ _84802) ^ [_95282] : [_95282 = sdtpldt1(_94989, _94987), 329 ^ _84802 : [(330 ^ _84802) ^ [] : [-(aSet0(_95282))], (332 ^ _84802) ^ [_95559] : [aElementOf0(_95559, _95282), 337 ^ _84802 : [(338 ^ _84802) ^ [] : [-(aElementOf0(335 ^ [_94987, _94989, _95282, _95559], _94989))], (340 ^ _84802) ^ [] : [-(aElementOf0(336 ^ [_94987, _94989, _95282, _95559], _94987))], (342 ^ _84802) ^ [] : [-(sdtpldt0(335 ^ [_94987, _94989, _95282, _95559], 336 ^ [_94987, _94989, _95282, _95559]) = _95559)]]], (344 ^ _84802) ^ [_96119] : [-(aElementOf0(_96119, _95282)), 345 ^ _84802 : [(346 ^ _84802) ^ [_96249, _96251] : [aElementOf0(_96251, _94989), aElementOf0(_96249, _94987), sdtpldt0(_96251, _96249) = _96119]]]]]]], (391 ^ _84802) ^ [_97967, _97969] : [aSet0(_97969), aSet0(_97967), 398 ^ _84802 : [(423 ^ _84802) ^ [_99046] : [-(_99046 = sdtasasdt0(_97969, _97967)), aSet0(_99046), 439 ^ _84802 : [(440 ^ _84802) ^ [] : [-(aElementOf0(428 ^ [_97967, _97969, _99046], _97969))], (442 ^ _84802) ^ [] : [-(aElementOf0(428 ^ [_97967, _97969, _99046], _97967))], (444 ^ _84802) ^ [] : [aElementOf0(428 ^ [_97967, _97969, _99046], _99046)]], 431 ^ _84802 : [(432 ^ _84802) ^ [] : [-(aElementOf0(428 ^ [_97967, _97969, _99046], _99046))], (434 ^ _84802) ^ [] : [aElementOf0(428 ^ [_97967, _97969, _99046], _97969), aElementOf0(428 ^ [_97967, _97969, _99046], _97967)]]], (399 ^ _84802) ^ [_98243] : [_98243 = sdtasasdt0(_97969, _97967), 402 ^ _84802 : [(403 ^ _84802) ^ [] : [-(aSet0(_98243))], (405 ^ _84802) ^ [_98501] : [aElementOf0(_98501, _98243), 408 ^ _84802 : [(409 ^ _84802) ^ [] : [-(aElementOf0(_98501, _97969))], (411 ^ _84802) ^ [] : [-(aElementOf0(_98501, _97967))]]], (413 ^ _84802) ^ [_98760] : [-(aElementOf0(_98760, _98243)), aElementOf0(_98760, _97969), aElementOf0(_98760, _97967)]]]]], (470 ^ _84802) ^ [_100711] : [-(aIdeal0(_100711)), aSet0(_100711), 476 ^ _84802 : [(477 ^ _84802) ^ [] : [-(aElementOf0(475 ^ [_100711], _100711))], (479 ^ _84802) ^ [] : [481 ^ _84802 : [(482 ^ _84802) ^ [] : [-(aElementOf0(480 ^ [_100711], _100711))], (484 ^ _84802) ^ [] : [aElementOf0(sdtpldt0(475 ^ [_100711], 480 ^ [_100711]), _100711)]], 486 ^ _84802 : [(487 ^ _84802) ^ [] : [-(aElement0(485 ^ [_100711]))], (489 ^ _84802) ^ [] : [aElementOf0(sdtasdt0(485 ^ [_100711], 475 ^ [_100711]), _100711)]]]]], (448 ^ _84802) ^ [_99916] : [aIdeal0(_99916), 451 ^ _84802 : [(452 ^ _84802) ^ [] : [-(aSet0(_99916))], (454 ^ _84802) ^ [_100148] : [aElementOf0(_100148, _99916), 457 ^ _84802 : [(458 ^ _84802) ^ [_100329] : [aElementOf0(_100329, _99916), -(aElementOf0(sdtpldt0(_100148, _100329), _99916))], (464 ^ _84802) ^ [_100521] : [aElement0(_100521), -(aElementOf0(sdtasdt0(_100521, _100148), _99916))]]]]], (535 ^ _84802) ^ [] : [-(aElementOf0(532 ^ [], xI))], (537 ^ _84802) ^ [] : [-(aElementOf0(533 ^ [], xJ))], (539 ^ _84802) ^ [] : [-(sdtpldt0(532 ^ [], 533 ^ []) = xx)], (541 ^ _84802) ^ [] : [-(aElementOf0(xx, sdtpldt1(xI, xJ)))], (545 ^ _84802) ^ [] : [-(aElementOf0(542 ^ [], xI))], (547 ^ _84802) ^ [] : [-(aElementOf0(543 ^ [], xJ))], (549 ^ _84802) ^ [] : [-(sdtpldt0(542 ^ [], 543 ^ []) = xy)], (551 ^ _84802) ^ [] : [-(aElementOf0(xy, sdtpldt1(xI, xJ)))], (553 ^ _84802) ^ [] : [-(aElement0(xz))], (555 ^ _84802) ^ [] : [-(aElementOf0(xk, xI))], (557 ^ _84802) ^ [] : [-(aElementOf0(xl, xJ))], (559 ^ _84802) ^ [] : [-(xx = sdtpldt0(xk, xl))], (561 ^ _84802) ^ [] : [-(aElementOf0(xm, xI))], (563 ^ _84802) ^ [] : [-(aElementOf0(xn, xJ))], (565 ^ _84802) ^ [] : [-(xy = sdtpldt0(xm, xn))], (567 ^ _84802) ^ [] : [-(aElementOf0(sdtpldt0(xk, xm), xI))], (569 ^ _84802) ^ [] : [-(aElementOf0(sdtpldt0(xl, xn), xJ))], (571 ^ _84802) ^ [] : [-(aElementOf0(sdtasdt0(xz, xk), xI))], (573 ^ _84802) ^ [] : [-(aElementOf0(sdtasdt0(xz, xl), xJ))], (575 ^ _84802) ^ [] : [-(sdtpldt0(xx, xy) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn)))], (577 ^ _84802) ^ [] : [-(sdtasdt0(xz, xx) = sdtpldt0(sdtasdt0(xz, xk), sdtasdt0(xz, xl)))], (493 ^ _84802) ^ [] : [-(aSet0(xI))], (495 ^ _84802) ^ [_101610] : [aElementOf0(_101610, xI), 498 ^ _84802 : [(499 ^ _84802) ^ [_101785] : [aElementOf0(_101785, xI), -(aElementOf0(sdtpldt0(_101610, _101785), xI))], (505 ^ _84802) ^ [_101969] : [aElement0(_101969), -(aElementOf0(sdtasdt0(_101969, _101610), xI))]]], (511 ^ _84802) ^ [] : [-(aIdeal0(xI))], (513 ^ _84802) ^ [] : [-(aSet0(xJ))], (531 ^ _84802) ^ [] : [-(aIdeal0(xJ))], (515 ^ _84802) ^ [_102284] : [aElementOf0(_102284, xJ), 518 ^ _84802 : [(519 ^ _84802) ^ [_102459] : [aElementOf0(_102459, xJ), -(aElementOf0(sdtpldt0(_102284, _102459), xJ))], (525 ^ _84802) ^ [_102643] : [aElement0(_102643), -(aElementOf0(sdtasdt0(_102643, _102284), xJ))]]]], input).
% 102.57/99.58 ncf('1',plain,[581 : aElementOf0(sdtpldt0(xk, xm), xI), 581 : aElementOf0(sdtpldt0(xl, xn), xJ), 581 : sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn)) = sdtpldt0(xx, xy), 593 : aElementOf0(sdtasdt0(xz, xk), xI), 593 : aElementOf0(sdtasdt0(xz, xl), xJ), 593 : sdtpldt0(sdtasdt0(xz, xk), sdtasdt0(xz, xl)) = sdtasdt0(xz, xx)],start(579 ^ 0,bind([[_104525, _104527, _104863, _104865], [sdtpldt0(xl, xn), sdtpldt0(xk, xm), sdtasdt0(xz, xl), sdtasdt0(xz, xk)]]))).
% 102.57/99.58 ncf('1.1',plain,[-(aElementOf0(sdtpldt0(xk, xm), xI)), 458 : aElementOf0(xm, xI), 458 : aElementOf0(xk, xI), 454 : aIdeal0(xI)],extension(448 ^ 3,bind([[_99916, _100148, _100329], [xI, xk, xm]]))).
% 102.57/99.58 ncf('1.1.1',plain,[-(aElementOf0(xm, xI))],extension(561 ^ 8)).
% 102.57/99.58 ncf('1.1.2',plain,[-(aElementOf0(xk, xI))],extension(555 ^ 6)).
% 102.57/99.58 ncf('1.1.3',plain,[-(aIdeal0(xI))],extension(511 ^ 4)).
% 102.57/99.58 ncf('1.2',plain,[-(aElementOf0(sdtpldt0(xl, xn), xJ)), 458 : aElementOf0(xn, xJ), 458 : aElementOf0(xl, xJ), 454 : aIdeal0(xJ)],extension(448 ^ 3,bind([[_99916, _100148, _100329], [xJ, xl, xn]]))).
% 102.57/99.58 ncf('1.2.1',plain,[-(aElementOf0(xn, xJ))],extension(563 ^ 8)).
% 102.57/99.58 ncf('1.2.2',plain,[-(aElementOf0(xl, xJ))],extension(557 ^ 6)).
% 102.57/99.58 ncf('1.2.3',plain,[-(aIdeal0(xJ))],extension(531 ^ 4)).
% 102.57/99.58 ncf('1.3',plain,[-(sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn)) = sdtpldt0(xx, xy)), sdtpldt0(xx, xy) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn))],extension(4 ^ 3,bind([[_85053, _85055], [sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn)), sdtpldt0(xx, xy)]]))).
% 102.57/99.58 ncf('1.3.1',plain,[-(sdtpldt0(xx, xy) = sdtpldt0(sdtpldt0(xk, xm), sdtpldt0(xl, xn)))],extension(575 ^ 4)).
% 102.57/99.58 ncf('1.4',plain,[-(aElementOf0(sdtasdt0(xz, xk), xI)), 464 : aElement0(xz), 464 : aElementOf0(xk, xI), 454 : aIdeal0(xI)],extension(448 ^ 3,bind([[_99916, _100148, _100521], [xI, xk, xz]]))).
% 102.57/99.58 ncf('1.4.1',plain,[-(aElement0(xz))],extension(553 ^ 8)).
% 102.57/99.58 ncf('1.4.2',plain,[-(aElementOf0(xk, xI))],extension(555 ^ 6)).
% 102.57/99.58 ncf('1.4.3',plain,[-(aIdeal0(xI))],extension(511 ^ 4)).
% 102.57/99.58 ncf('1.5',plain,[-(aElementOf0(sdtasdt0(xz, xl), xJ)), 464 : aElement0(xz), 464 : aElementOf0(xl, xJ), 454 : aIdeal0(xJ)],extension(448 ^ 3,bind([[_99916, _100148, _100521], [xJ, xl, xz]]))).
% 102.57/99.58 ncf('1.5.1',plain,[-(aElement0(xz))],extension(553 ^ 8)).
% 102.57/99.58 ncf('1.5.2',plain,[-(aElementOf0(xl, xJ))],extension(557 ^ 6)).
% 102.57/99.58 ncf('1.5.3',plain,[-(aIdeal0(xJ))],extension(531 ^ 4)).
% 102.57/99.58 ncf('1.6',plain,[-(sdtpldt0(sdtasdt0(xz, xk), sdtasdt0(xz, xl)) = sdtasdt0(xz, xx)), sdtasdt0(xz, xx) = sdtpldt0(sdtasdt0(xz, xk), sdtasdt0(xz, xl))],extension(4 ^ 3,bind([[_85053, _85055], [sdtpldt0(sdtasdt0(xz, xk), sdtasdt0(xz, xl)), sdtasdt0(xz, xx)]]))).
% 102.57/99.58 ncf('1.6.1',plain,[-(sdtasdt0(xz, xx) = sdtpldt0(sdtasdt0(xz, xk), sdtasdt0(xz, xl)))],extension(577 ^ 4)).
% 102.57/99.58 %-----------------------------------------------------
% 102.57/99.58 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------