%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : RNG092+1 : 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 0.46s 1.41s
% Output : Proof 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : RNG092+1 : TPTP v8.1.2. Released v4.0.0.
% 0.04/0.15 % Command : nanocop.sh %s %d
% 0.13/0.36 % Computer : n005.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8042.1875MB
% 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Thu May 18 20:18:38 EDT 2023
% 0.13/0.36 % CPUTime :
% 0.46/1.41
% 0.46/1.41 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.46/1.41 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.46/1.41 %-----------------------------------------------------
% 0.46/1.41 ncf(matrix, plain, [(539 ^ _79428) ^ [] : [aIdeal0(sdtpldt1(xI, xJ))], (497 ^ _79428) ^ [_96435, _96437, _96439] : [510 ^ _79428 : [(511 ^ _79428) ^ [] : [-(aElementOf0(508 ^ [_96435, _96437, _96439], xI))], (513 ^ _79428) ^ [] : [-(aElementOf0(509 ^ [_96435, _96437, _96439], xJ))], (515 ^ _79428) ^ [] : [-(_96439 = sdtpldt0(508 ^ [_96435, _96437, _96439], 509 ^ [_96435, _96437, _96439]))], (519 ^ _79428) ^ [] : [-(aElementOf0(516 ^ [_96435, _96437, _96439], xI))], (521 ^ _79428) ^ [] : [-(aElementOf0(517 ^ [_96435, _96437, _96439], xJ))], (523 ^ _79428) ^ [] : [-(_96437 = sdtpldt0(516 ^ [_96435, _96437, _96439], 517 ^ [_96435, _96437, _96439]))], (525 ^ _79428) ^ [] : [-(aElementOf0(sdtpldt0(508 ^ [_96435, _96437, _96439], 516 ^ [_96435, _96437, _96439]), xI))], (527 ^ _79428) ^ [] : [-(aElementOf0(sdtpldt0(509 ^ [_96435, _96437, _96439], 517 ^ [_96435, _96437, _96439]), xJ))], (529 ^ _79428) ^ [] : [-(aElementOf0(sdtasdt0(_96435, 508 ^ [_96435, _96437, _96439]), xI))], (531 ^ _79428) ^ [] : [-(aElementOf0(sdtasdt0(_96435, 509 ^ [_96435, _96437, _96439]), xJ))], (533 ^ _79428) ^ [] : [-(sdtpldt0(_96439, _96437) = sdtpldt0(sdtpldt0(508 ^ [_96435, _96437, _96439], 516 ^ [_96435, _96437, _96439]), sdtpldt0(509 ^ [_96435, _96437, _96439], 517 ^ [_96435, _96437, _96439])))], (535 ^ _79428) ^ [] : [-(aElementOf0(sdtpldt0(_96439, _96437), sdtpldt1(xI, xJ)))], (537 ^ _79428) ^ [] : [-(aElementOf0(sdtasdt0(_96435, _96439), sdtpldt1(xI, xJ)))]], aElementOf0(_96439, sdtpldt1(xI, xJ)), aElementOf0(_96437, sdtpldt1(xI, xJ)), aElement0(_96435)], (64 ^ _79428) ^ [_81517, _81519] : [_81519 = _81517, -(smndt0(_81519) = smndt0(_81517))], (70 ^ _79428) ^ [_81763, _81765, _81767, _81769] : [-(sdtasasdt0(_81769, _81765) = sdtasasdt0(_81767, _81763)), _81769 = _81767, _81765 = _81763], (80 ^ _79428) ^ [_82122, _82124, _82126, _82128] : [-(sdtpldt0(_82128, _82124) = sdtpldt0(_82126, _82122)), _82128 = _82126, _82124 = _82122], (90 ^ _79428) ^ [_82481, _82483, _82485, _82487] : [-(sdtasdt0(_82487, _82483) = sdtasdt0(_82485, _82481)), _82487 = _82485, _82483 = _82481], (100 ^ _79428) ^ [_82820, _82822, _82824, _82826] : [-(sdtpldt1(_82826, _82822) = sdtpldt1(_82824, _82820)), _82826 = _82824, _82822 = _82820], (2 ^ _79428) ^ [_79572] : [-(_79572 = _79572)], (4 ^ _79428) ^ [_79679, _79681] : [_79681 = _79679, -(_79679 = _79681)], (10 ^ _79428) ^ [_79883, _79885, _79887] : [-(_79887 = _79883), _79887 = _79885, _79885 = _79883], (20 ^ _79428) ^ [_80196, _80198] : [-(aSet0(_80196)), _80198 = _80196, aSet0(_80198)], (30 ^ _79428) ^ [_80491, _80493] : [-(aElement0(_80491)), _80493 = _80491, aElement0(_80493)], (54 ^ _79428) ^ [_81210, _81212] : [-(aIdeal0(_81210)), _81212 = _81210, aIdeal0(_81212)], (40 ^ _79428) ^ [_80814, _80816, _80818, _80820] : [-(aElementOf0(_80818, _80814)), aElementOf0(_80820, _80816), _80820 = _80818, _80816 = _80814], (110 ^ _79428) ^ [_83155] : [aElement0(_83155), true___, -(true___)], (120 ^ _79428) ^ [] : [-(aElement0(sz00))], (122 ^ _79428) ^ [] : [-(aElement0(sz10))], (124 ^ _79428) ^ [_83516] : [aElement0(_83516), -(aElement0(smndt0(_83516)))], (130 ^ _79428) ^ [_83720, _83722] : [-(aElement0(sdtpldt0(_83722, _83720))), aElement0(_83722), aElement0(_83720)], (140 ^ _79428) ^ [_84019, _84021] : [-(aElement0(sdtasdt0(_84021, _84019))), aElement0(_84021), aElement0(_84019)], (150 ^ _79428) ^ [_84318, _84320] : [-(sdtpldt0(_84320, _84318) = sdtpldt0(_84318, _84320)), aElement0(_84320), aElement0(_84318)], (160 ^ _79428) ^ [_84639, _84641, _84643] : [-(sdtpldt0(sdtpldt0(_84643, _84641), _84639) = sdtpldt0(_84643, sdtpldt0(_84641, _84639))), aElement0(_84643), aElement0(_84641), aElement0(_84639)], (174 ^ _79428) ^ [_85045] : [aElement0(_85045), 177 ^ _79428 : [(178 ^ _79428) ^ [] : [-(sdtpldt0(_85045, sz00) = _85045)], (180 ^ _79428) ^ [] : [-(_85045 = sdtpldt0(sz00, _85045))]]], (182 ^ _79428) ^ [_85318] : [aElement0(_85318), 185 ^ _79428 : [(186 ^ _79428) ^ [] : [-(sdtpldt0(_85318, smndt0(_85318)) = sz00)], (188 ^ _79428) ^ [] : [-(sz00 = sdtpldt0(smndt0(_85318), _85318))]]], (190 ^ _79428) ^ [_85613, _85615] : [-(sdtasdt0(_85615, _85613) = sdtasdt0(_85613, _85615)), aElement0(_85615), aElement0(_85613)], (200 ^ _79428) ^ [_85934, _85936, _85938] : [-(sdtasdt0(sdtasdt0(_85938, _85936), _85934) = sdtasdt0(_85938, sdtasdt0(_85936, _85934))), aElement0(_85938), aElement0(_85936), aElement0(_85934)], (214 ^ _79428) ^ [_86340] : [aElement0(_86340), 217 ^ _79428 : [(218 ^ _79428) ^ [] : [-(sdtasdt0(_86340, sz10) = _86340)], (220 ^ _79428) ^ [] : [-(_86340 = sdtasdt0(sz10, _86340))]]], (222 ^ _79428) ^ [_86641, _86643, _86645] : [233 ^ _79428 : [(234 ^ _79428) ^ [] : [-(sdtasdt0(_86645, sdtpldt0(_86643, _86641)) = sdtpldt0(sdtasdt0(_86645, _86643), sdtasdt0(_86645, _86641)))], (236 ^ _79428) ^ [] : [-(sdtasdt0(sdtpldt0(_86643, _86641), _86645) = sdtpldt0(sdtasdt0(_86643, _86645), sdtasdt0(_86641, _86645)))]], aElement0(_86645), aElement0(_86643), aElement0(_86641)], (238 ^ _79428) ^ [_87160] : [aElement0(_87160), 241 ^ _79428 : [(242 ^ _79428) ^ [] : [-(sdtasdt0(smndt0(sz10), _87160) = smndt0(_87160))], (244 ^ _79428) ^ [] : [-(smndt0(_87160) = sdtasdt0(_87160, smndt0(sz10)))]]], (246 ^ _79428) ^ [_87441] : [aElement0(_87441), 249 ^ _79428 : [(250 ^ _79428) ^ [] : [-(sdtasdt0(_87441, sz00) = sz00)], (252 ^ _79428) ^ [] : [-(sz00 = sdtasdt0(sz00, _87441))]]], (254 ^ _79428) ^ [_87728, _87730] : [aElement0(_87730), aElement0(_87728), sdtasdt0(_87730, _87728) = sz00, -(_87730 = sz00), -(_87728 = sz00)], (272 ^ _79428) ^ [] : [sz10 = sz00], (274 ^ _79428) ^ [_88248] : [aSet0(_88248), true___, -(true___)], (284 ^ _79428) ^ [_88503] : [aSet0(_88503), 287 ^ _79428 : [(288 ^ _79428) ^ [_88633] : [aElementOf0(_88633, _88503), -(aElement0(_88633))]]], (294 ^ _79428) ^ [_88848, _88850] : [aSet0(_88850), aSet0(_88848), -(_88850 = _88848), 306 ^ _79428 : [(307 ^ _79428) ^ [] : [-(aElementOf0(305 ^ [_88848, _88850], _88850))], (309 ^ _79428) ^ [] : [aElementOf0(305 ^ [_88848, _88850], _88848)]], 311 ^ _79428 : [(312 ^ _79428) ^ [] : [-(aElementOf0(310 ^ [_88848, _88850], _88848))], (314 ^ _79428) ^ [] : [aElementOf0(310 ^ [_88848, _88850], _88850)]]], (318 ^ _79428) ^ [_89613, _89615] : [aSet0(_89615), aSet0(_89613), 325 ^ _79428 : [(358 ^ _79428) ^ [_91243] : [-(_91243 = sdtpldt1(_89615, _89613)), aSet0(_91243), 380 ^ _79428 : [(381 ^ _79428) ^ [] : [-(aElementOf0(378 ^ [_89613, _89615, _91243], _89615))], (383 ^ _79428) ^ [] : [-(aElementOf0(379 ^ [_89613, _89615, _91243], _89613))], (385 ^ _79428) ^ [] : [-(sdtpldt0(378 ^ [_89613, _89615, _91243], 379 ^ [_89613, _89615, _91243]) = 363 ^ [_89613, _89615, _91243])], (387 ^ _79428) ^ [] : [aElementOf0(363 ^ [_89613, _89615, _91243], _91243)]], 366 ^ _79428 : [(367 ^ _79428) ^ [] : [-(aElementOf0(363 ^ [_89613, _89615, _91243], _91243))], (369 ^ _79428) ^ [_91672, _91674] : [aElementOf0(_91674, _89615), aElementOf0(_91672, _89613), sdtpldt0(_91674, _91672) = 363 ^ [_89613, _89615, _91243]]]], (326 ^ _79428) ^ [_89908] : [_89908 = sdtpldt1(_89615, _89613), 329 ^ _79428 : [(330 ^ _79428) ^ [] : [-(aSet0(_89908))], (332 ^ _79428) ^ [_90185] : [aElementOf0(_90185, _89908), 337 ^ _79428 : [(338 ^ _79428) ^ [] : [-(aElementOf0(335 ^ [_89613, _89615, _89908, _90185], _89615))], (340 ^ _79428) ^ [] : [-(aElementOf0(336 ^ [_89613, _89615, _89908, _90185], _89613))], (342 ^ _79428) ^ [] : [-(sdtpldt0(335 ^ [_89613, _89615, _89908, _90185], 336 ^ [_89613, _89615, _89908, _90185]) = _90185)]]], (344 ^ _79428) ^ [_90745] : [-(aElementOf0(_90745, _89908)), 345 ^ _79428 : [(346 ^ _79428) ^ [_90875, _90877] : [aElementOf0(_90877, _89615), aElementOf0(_90875, _89613), sdtpldt0(_90877, _90875) = _90745]]]]]]], (493 ^ _79428) ^ [] : [-(aIdeal0(xI))], (495 ^ _79428) ^ [] : [-(aIdeal0(xJ))], (470 ^ _79428) ^ [_95337] : [-(aIdeal0(_95337)), aSet0(_95337), 476 ^ _79428 : [(477 ^ _79428) ^ [] : [-(aElementOf0(475 ^ [_95337], _95337))], (479 ^ _79428) ^ [] : [481 ^ _79428 : [(482 ^ _79428) ^ [] : [-(aElementOf0(480 ^ [_95337], _95337))], (484 ^ _79428) ^ [] : [aElementOf0(sdtpldt0(475 ^ [_95337], 480 ^ [_95337]), _95337)]], 486 ^ _79428 : [(487 ^ _79428) ^ [] : [-(aElement0(485 ^ [_95337]))], (489 ^ _79428) ^ [] : [aElementOf0(sdtasdt0(485 ^ [_95337], 475 ^ [_95337]), _95337)]]]]], (448 ^ _79428) ^ [_94542] : [aIdeal0(_94542), 451 ^ _79428 : [(452 ^ _79428) ^ [] : [-(aSet0(_94542))], (454 ^ _79428) ^ [_94774] : [aElementOf0(_94774, _94542), 457 ^ _79428 : [(458 ^ _79428) ^ [_94955] : [aElementOf0(_94955, _94542), -(aElementOf0(sdtpldt0(_94774, _94955), _94542))], (464 ^ _79428) ^ [_95147] : [aElement0(_95147), -(aElementOf0(sdtasdt0(_95147, _94774), _94542))]]]]], (391 ^ _79428) ^ [_92593, _92595] : [aSet0(_92595), aSet0(_92593), 398 ^ _79428 : [(423 ^ _79428) ^ [_93672] : [-(_93672 = sdtasasdt0(_92595, _92593)), aSet0(_93672), 439 ^ _79428 : [(440 ^ _79428) ^ [] : [-(aElementOf0(428 ^ [_92593, _92595, _93672], _92595))], (442 ^ _79428) ^ [] : [-(aElementOf0(428 ^ [_92593, _92595, _93672], _92593))], (444 ^ _79428) ^ [] : [aElementOf0(428 ^ [_92593, _92595, _93672], _93672)]], 431 ^ _79428 : [(432 ^ _79428) ^ [] : [-(aElementOf0(428 ^ [_92593, _92595, _93672], _93672))], (434 ^ _79428) ^ [] : [aElementOf0(428 ^ [_92593, _92595, _93672], _92595), aElementOf0(428 ^ [_92593, _92595, _93672], _92593)]]], (399 ^ _79428) ^ [_92869] : [_92869 = sdtasasdt0(_92595, _92593), 402 ^ _79428 : [(403 ^ _79428) ^ [] : [-(aSet0(_92869))], (405 ^ _79428) ^ [_93127] : [aElementOf0(_93127, _92869), 408 ^ _79428 : [(409 ^ _79428) ^ [] : [-(aElementOf0(_93127, _92595))], (411 ^ _79428) ^ [] : [-(aElementOf0(_93127, _92593))]]], (413 ^ _79428) ^ [_93386] : [-(aElementOf0(_93386, _92869)), aElementOf0(_93386, _92595), aElementOf0(_93386, _92593)]]]]]], input).
% 0.46/1.41 ncf('1',plain,[aIdeal0(sdtpldt1(xI, xJ))],start(539 ^ 0)).
% 0.46/1.41 ncf('1.1',plain,[-(aIdeal0(sdtpldt1(xI, xJ))), aSet0(sdtpldt1(xI, xJ)), 482 : -(aElementOf0(480 ^ [sdtpldt1(xI, xJ)], sdtpldt1(xI, xJ))), 487 : -(aElement0(485 ^ [sdtpldt1(xI, xJ)]))],extension(470 ^ 1,bind([[_95337], [sdtpldt1(xI, xJ)]]))).
% 0.46/1.41 ncf('1.1.1',plain,[-(aSet0(sdtpldt1(xI, xJ))), 326 : sdtpldt1(xI, xJ) = sdtpldt1(xI, xJ), 326 : aSet0(xI), 326 : aSet0(xJ)],extension(318 ^ 2,bind([[_89613, _89615, _89908], [xJ, xI, sdtpldt1(xI, xJ)]]))).
% 0.46/1.41 ncf('1.1.1.1',plain,[-(sdtpldt1(xI, xJ) = sdtpldt1(xI, xJ))],extension(2 ^ 5,bind([[_79572], [sdtpldt1(xI, xJ)]]))).
% 0.46/1.41 ncf('1.1.1.2',plain,[-(aSet0(xI)), aIdeal0(xI)],extension(448 ^ 3,bind([[_94542], [xI]]))).
% 0.46/1.41 ncf('1.1.1.2.1',plain,[-(aIdeal0(xI))],extension(493 ^ 4)).
% 0.46/1.41 ncf('1.1.1.3',plain,[-(aSet0(xJ)), aIdeal0(xJ)],extension(448 ^ 3,bind([[_94542], [xJ]]))).
% 0.46/1.41 ncf('1.1.1.3.1',plain,[-(aIdeal0(xJ))],extension(495 ^ 4)).
% 0.46/1.41 ncf('1.1.2',plain,[aElementOf0(480 ^ [sdtpldt1(xI, xJ)], sdtpldt1(xI, xJ)), 535 : -(aElementOf0(sdtpldt0(475 ^ [sdtpldt1(xI, xJ)], 480 ^ [sdtpldt1(xI, xJ)]), sdtpldt1(xI, xJ))), 535 : aElementOf0(475 ^ [sdtpldt1(xI, xJ)], sdtpldt1(xI, xJ)), 535 : aElement0(sz00)],extension(497 ^ 6,bind([[_96435, _96437, _96439], [sz00, 480 ^ [sdtpldt1(xI, xJ)], 475 ^ [sdtpldt1(xI, xJ)]]]))).
% 0.46/1.41 ncf('1.1.2.1',plain,[aElementOf0(sdtpldt0(475 ^ [sdtpldt1(xI, xJ)], 480 ^ [sdtpldt1(xI, xJ)]), sdtpldt1(xI, xJ))],extension(484 ^ 9)).
% 0.46/1.41 ncf('1.1.2.2',plain,[-(aElementOf0(475 ^ [sdtpldt1(xI, xJ)], sdtpldt1(xI, xJ)))],extension(477 ^ 7)).
% 0.46/1.41 ncf('1.1.2.3',plain,[-(aElement0(sz00))],extension(120 ^ 7)).
% 0.46/1.41 ncf('1.1.3',plain,[aElement0(485 ^ [sdtpldt1(xI, xJ)]), 537 : -(aElementOf0(sdtasdt0(485 ^ [sdtpldt1(xI, xJ)], 475 ^ [sdtpldt1(xI, xJ)]), sdtpldt1(xI, xJ))), 537 : aElementOf0(475 ^ [sdtpldt1(xI, xJ)], sdtpldt1(xI, xJ)), 537 : aElementOf0(475 ^ [sdtpldt1(xI, xJ)], sdtpldt1(xI, xJ))],extension(497 ^ 6,bind([[_96435, _96437, _96439], [485 ^ [sdtpldt1(xI, xJ)], 475 ^ [sdtpldt1(xI, xJ)], 475 ^ [sdtpldt1(xI, xJ)]]]))).
% 0.46/1.41 ncf('1.1.3.1',plain,[aElementOf0(sdtasdt0(485 ^ [sdtpldt1(xI, xJ)], 475 ^ [sdtpldt1(xI, xJ)]), sdtpldt1(xI, xJ))],extension(489 ^ 9)).
% 0.46/1.41 ncf('1.1.3.2',plain,[-(aElementOf0(475 ^ [sdtpldt1(xI, xJ)], sdtpldt1(xI, xJ)))],extension(477 ^ 7)).
% 0.46/1.41 ncf('1.1.3.3',plain,[-(aElementOf0(475 ^ [sdtpldt1(xI, xJ)], sdtpldt1(xI, xJ)))],extension(477 ^ 7)).
% 0.46/1.41 %-----------------------------------------------------
% 0.46/1.41 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------