%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM538+2 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n010.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:56 EDT 2023
% Result : Theorem 189.85s 183.35s
% Output : Proof 189.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : NUM538+2 : TPTP v8.1.2. Released v4.0.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n010.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 17:15:57 EDT 2023
% 0.13/0.33 % CPUTime :
% 189.85/183.35
% 189.85/183.35 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 189.85/183.35 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 189.85/183.35 %-----------------------------------------------------
% 189.85/183.35 ncf(matrix, plain, [(829 ^ _123698) ^ [] : [szszuzczcdt0(sbrdtbr0(sdtmndt0(xS, xx))) = sbrdtbr0(xS)], (815 ^ _123698) ^ [_124159] : [-(aElementOf0(_124159, sdtmndt0(xS, xx))), aElement0(_124159), aElementOf0(_124159, xS), -(_124159 = xx)], (805 ^ _123698) ^ [_123859] : [aElementOf0(_123859, sdtmndt0(xS, xx)), 808 ^ _123698 : [(813 ^ _123698) ^ [] : [_123859 = xx], (811 ^ _123698) ^ [] : [-(aElementOf0(_123859, xS))], (809 ^ _123698) ^ [] : [-(aElement0(_123859))]]], (803 ^ _123698) ^ [] : [-(aSet0(sdtmndt0(xS, xx)))], !, (601 ^ _99066) ^ [_117845, _117847] : [aElementOf0(_117847, szNzAzT0), aElementOf0(_117845, szNzAzT0), sdtlseqdt0(_117847, _117845), true___, -(true___)], (276 ^ _99066) ^ [_107630] : [aSet0(_107630), isFinite0(_107630), 283 ^ _99066 : [(284 ^ _99066) ^ [_107843] : [aSubsetOf0(_107843, _107630), -(isFinite0(_107843))]]], (142 ^ _99066) ^ [_103686, _103688] : [_103688 = _103686, -(sbrdtbr0(_103688) = sbrdtbr0(_103686))], (526 ^ _99066) ^ [_115530] : [aElement0(_115530), 529 ^ _99066 : [(530 ^ _99066) ^ [_115667] : [-(isFinite0(sdtpldt0(_115667, _115530))), aSet0(_115667), isFinite0(_115667)]]], (211 ^ _99066) ^ [] : [-(isFinite0(slcrc0))], (568 ^ _99066) ^ [_116835, _116837] : [aElementOf0(_116837, szNzAzT0), aElementOf0(_116835, szNzAzT0), szszuzczcdt0(_116837) = szszuzczcdt0(_116835), -(_116837 = _116835)], (148 ^ _99066) ^ [_103904] : [aSet0(_103904), true___, -(true___)], (227 ^ _99066) ^ [_106087] : [isFinite0(_106087), aSet0(_106087), isCountable0(_106087)], (556 ^ _99066) ^ [] : [-(isCountable0(szNzAzT0))], (797 ^ _99066) ^ [] : [-(aSet0(xS))], (779 ^ _99066) ^ [_122820] : [aSet0(_122820), isFinite0(_122820), 786 ^ _99066 : [(787 ^ _99066) ^ [_123050] : [aElement0(_123050), -(aElementOf0(_123050, _122820)), -(sbrdtbr0(sdtpldt0(_122820, _123050)) = szszuzczcdt0(sbrdtbr0(_122820)))]]], (34 ^ _99066) ^ [_100258, _100260] : [-(isCountable0(_100258)), _100260 = _100258, isCountable0(_100260)], (44 ^ _99066) ^ [_100581, _100583, _100585, _100587] : [-(sdtlseqdt0(_100585, _100581)), sdtlseqdt0(_100587, _100583), _100587 = _100585, _100583 = _100581], (405 ^ _99066) ^ [_111621, _111623] : [aSet0(_111623), aElement0(_111621), 412 ^ _99066 : [(443 ^ _99066) ^ [_112889] : [-(_112889 = sdtmndt0(_111623, _111621)), aSet0(_112889), 463 ^ _99066 : [(464 ^ _99066) ^ [] : [-(aElement0(448 ^ [_111621, _111623, _112889]))], (470 ^ _99066) ^ [] : [aElementOf0(448 ^ [_111621, _111623, _112889], _112889)], (468 ^ _99066) ^ [] : [448 ^ [_111621, _111623, _112889] = _111621], (466 ^ _99066) ^ [] : [-(aElementOf0(448 ^ [_111621, _111623, _112889], _111623))]], 451 ^ _99066 : [(452 ^ _99066) ^ [] : [-(aElementOf0(448 ^ [_111621, _111623, _112889], _112889))], (454 ^ _99066) ^ [] : [aElement0(448 ^ [_111621, _111623, _112889]), aElementOf0(448 ^ [_111621, _111623, _112889], _111623), -(448 ^ [_111621, _111623, _112889] = _111621)]]], (413 ^ _99066) ^ [_111904] : [_111904 = sdtmndt0(_111623, _111621), 416 ^ _99066 : [(429 ^ _99066) ^ [_112505] : [-(aElementOf0(_112505, _111904)), aElement0(_112505), aElementOf0(_112505, _111623), -(_112505 = _111621)], (419 ^ _99066) ^ [_112169] : [aElementOf0(_112169, _111904), 422 ^ _99066 : [(427 ^ _99066) ^ [] : [_112169 = _111621], (425 ^ _99066) ^ [] : [-(aElementOf0(_112169, _111623))], (423 ^ _99066) ^ [] : [-(aElement0(_112169))]]], (417 ^ _99066) ^ [] : [-(aSet0(_111904))]]]]], (631 ^ _99066) ^ [_118694, _118696] : [aElementOf0(_118696, szNzAzT0), aElementOf0(_118694, szNzAzT0), 638 ^ _99066 : [(639 ^ _99066) ^ [] : [sdtlseqdt0(_118696, _118694), -(sdtlseqdt0(szszuzczcdt0(_118696), szszuzczcdt0(_118694)))], (645 ^ _99066) ^ [] : [sdtlseqdt0(szszuzczcdt0(_118696), szszuzczcdt0(_118694)), -(sdtlseqdt0(_118696, _118694))]]], (582 ^ _99066) ^ [_117219] : [aElementOf0(_117219, szNzAzT0), -(_117219 = sz00), 590 ^ _99066 : [(591 ^ _99066) ^ [] : [-(aElementOf0(589 ^ [_117219], szNzAzT0))], (593 ^ _99066) ^ [] : [-(_117219 = szszuzczcdt0(589 ^ [_117219]))]]], (619 ^ _99066) ^ [_118295] : [aElementOf0(_118295, szNzAzT0), -(sdtlseqdt0(sz00, _118295))], (10 ^ _99066) ^ [_99501, _99503, _99505] : [-(_99505 = _99501), _99505 = _99503, _99503 = _99501], (116 ^ _99066) ^ [_102798, _102800, _102802, _102804] : [-(sdtpldt0(_102804, _102800) = sdtpldt0(_102802, _102798)), _102804 = _102802, _102800 = _102798], (474 ^ _99066) ^ [_113919] : [aSet0(_113919), 477 ^ _99066 : [(478 ^ _99066) ^ [_114056] : [aElementOf0(_114056, _113919), -(sdtpldt0(sdtmndt0(_113919, _114056), _114056) = _113919)]]], (58 ^ _99066) ^ [_101025, _101027, _101029, _101031] : [-(iLess0(_101029, _101025)), iLess0(_101031, _101027), _101031 = _101029, _101027 = _101025], (168 ^ _99066) ^ [_104414] : [aSet0(_104414), 171 ^ _99066 : [(172 ^ _99066) ^ [_104544] : [aElementOf0(_104544, _104414), -(aElement0(_104544))]]], (799 ^ _99066) ^ [] : [-(isFinite0(xS))], (558 ^ _99066) ^ [] : [-(aElementOf0(sz00, szNzAzT0))], (512 ^ _99066) ^ [_115101] : [aElement0(_115101), 515 ^ _99066 : [(516 ^ _99066) ^ [_115238] : [-(isCountable0(sdtmndt0(_115238, _115101))), aSet0(_115238), isCountable0(_115238)]]], (554 ^ _99066) ^ [] : [-(aSet0(szNzAzT0))], (237 ^ _99066) ^ [_106357] : [_106357 = slcrc0, aSet0(_106357), isCountable0(_106357)], (158 ^ _99066) ^ [_104159] : [aElement0(_104159), true___, -(true___)], (72 ^ _99066) ^ [_101441, _101443] : [-(isFinite0(_101441)), _101443 = _101441, isFinite0(_101443)], (540 ^ _99066) ^ [_115959] : [aElement0(_115959), 543 ^ _99066 : [(544 ^ _99066) ^ [_116096] : [-(isFinite0(sdtmndt0(_116096, _115959))), aSet0(_116096), isFinite0(_116096)]]], (4 ^ _99066) ^ [_99297, _99299] : [_99299 = _99297, -(_99297 = _99299)], (735 ^ _99066) ^ [_121571] : [aElementOf0(_121571, szNzAzT0), -(iLess0(_121571, szszuzczcdt0(_121571)))], (336 ^ _99066) ^ [_109323, _109325] : [aSet0(_109325), aElement0(_109323), 343 ^ _99066 : [(374 ^ _99066) ^ [_110584] : [-(_110584 = sdtpldt0(_109325, _109323)), aSet0(_110584), 382 ^ _99066 : [(383 ^ _99066) ^ [] : [-(aElementOf0(379 ^ [_109323, _109325, _110584], _110584))], (385 ^ _99066) ^ [] : [aElement0(379 ^ [_109323, _109325, _110584]), 388 ^ _99066 : [(389 ^ _99066) ^ [] : [aElementOf0(379 ^ [_109323, _109325, _110584], _109325)], (391 ^ _99066) ^ [] : [379 ^ [_109323, _109325, _110584] = _109323]]]], 392 ^ _99066 : [(395 ^ _99066) ^ [] : [-(aElementOf0(379 ^ [_109323, _109325, _110584], _109325)), -(379 ^ [_109323, _109325, _110584] = _109323)], (393 ^ _99066) ^ [] : [-(aElement0(379 ^ [_109323, _109325, _110584]))], (401 ^ _99066) ^ [] : [aElementOf0(379 ^ [_109323, _109325, _110584], _110584)]]], (344 ^ _99066) ^ [_109604] : [_109604 = sdtpldt0(_109325, _109323), 347 ^ _99066 : [(362 ^ _99066) ^ [_110222] : [-(aElementOf0(_110222, _109604)), aElement0(_110222), 367 ^ _99066 : [(368 ^ _99066) ^ [] : [aElementOf0(_110222, _109325)], (370 ^ _99066) ^ [] : [_110222 = _109323]]], (350 ^ _99066) ^ [_109867] : [aElementOf0(_109867, _109604), 353 ^ _99066 : [(354 ^ _99066) ^ [] : [-(aElement0(_109867))], (356 ^ _99066) ^ [] : [-(aElementOf0(_109867, _109325)), -(_109867 = _109323)]]], (348 ^ _99066) ^ [] : [-(aSet0(_109604))]]]]], (82 ^ _99066) ^ [_101736, _101738] : [-(aSet0(_101736)), _101738 = _101736, aSet0(_101738)], (247 ^ _99066) ^ [_106629] : [aSet0(_106629), 250 ^ _99066 : [(251 ^ _99066) ^ [_106805] : [aSubsetOf0(_106805, _106629), 254 ^ _99066 : [(255 ^ _99066) ^ [] : [-(aSet0(_106805))], (257 ^ _99066) ^ [_107014] : [aElementOf0(_107014, _106805), -(aElementOf0(_107014, _106629))]]], (263 ^ _99066) ^ [_107193] : [-(aSubsetOf0(_107193, _106629)), aSet0(_107193), 269 ^ _99066 : [(270 ^ _99066) ^ [] : [-(aElementOf0(268 ^ [_106629, _107193], _107193))], (272 ^ _99066) ^ [] : [aElementOf0(268 ^ [_106629, _107193], _106629)]]]]], (651 ^ _99066) ^ [_119243] : [aElementOf0(_119243, szNzAzT0), -(sdtlseqdt0(_119243, szszuzczcdt0(_119243)))], (717 ^ _99066) ^ [_121121, _121123] : [aElementOf0(_121123, szNzAzT0), aElementOf0(_121121, szNzAzT0), iLess0(_121123, _121121), true___, -(true___)], (126 ^ _99066) ^ [_103129, _103131] : [_103131 = _103129, -(szszuzczcdt0(_103131) = szszuzczcdt0(_103129))], (213 ^ _99066) ^ [_105746] : [aSet0(_105746), isCountable0(_105746), true___, -(true___)], (681 ^ _99066) ^ [_120134, _120136, _120138] : [aElementOf0(_120138, szNzAzT0), aElementOf0(_120136, szNzAzT0), aElementOf0(_120134, szNzAzT0), -(sdtlseqdt0(_120138, _120134)), sdtlseqdt0(_120138, _120136), sdtlseqdt0(_120136, _120134)], (498 ^ _99066) ^ [_114672] : [aElement0(_114672), 501 ^ _99066 : [(502 ^ _99066) ^ [_114809] : [-(isCountable0(sdtpldt0(_114809, _114672))), aSet0(_114809), isCountable0(_114809)]]], (178 ^ _99066) ^ [_104745] : [aSet0(_104745), isFinite0(_104745), true___, -(true___)], (484 ^ _99066) ^ [_114285, _114287] : [aElement0(_114287), aSet0(_114285), -(aElementOf0(_114287, _114285)), -(sdtmndt0(sdtpldt0(_114285, _114287), _114287) = _114285)], (801 ^ _99066) ^ [] : [-(aElementOf0(xx, xS))], (2 ^ _99066) ^ [_99190] : [-(_99190 = _99190)], (290 ^ _99066) ^ [_108046] : [aSet0(_108046), -(aSubsetOf0(_108046, _108046))], (560 ^ _99066) ^ [_116549] : [aElementOf0(_116549, szNzAzT0), 563 ^ _99066 : [(564 ^ _99066) ^ [] : [-(aElementOf0(szszuzczcdt0(_116549), szNzAzT0))], (566 ^ _99066) ^ [] : [szszuzczcdt0(_116549) = sz00]]], (625 ^ _99066) ^ [_118485] : [aElementOf0(_118485, szNzAzT0), sdtlseqdt0(szszuzczcdt0(_118485), sz00)], (200 ^ _99066) ^ [_105364] : [-(_105364 = slcrc0), aSet0(_105364), -(aElementOf0(205 ^ [_105364], _105364))], (741 ^ _99066) ^ [_121765] : [aSet0(_121765), -(aElement0(sbrdtbr0(_121765)))], (20 ^ _99066) ^ [_99842, _99844, _99846, _99848] : [-(aSubsetOf0(_99846, _99842)), aSubsetOf0(_99848, _99844), _99848 = _99846, _99844 = _99842], (595 ^ _99066) ^ [_117636] : [aElementOf0(_117636, szNzAzT0), _117636 = szszuzczcdt0(_117636)], (703 ^ _99066) ^ [_120726, _120728] : [aElementOf0(_120728, szNzAzT0), aElementOf0(_120726, szNzAzT0), -(sdtlseqdt0(_120728, _120726)), -(sdtlseqdt0(szszuzczcdt0(_120726), _120728))], (747 ^ _99066) ^ [_121955] : [aSet0(_121955), 750 ^ _99066 : [(751 ^ _99066) ^ [] : [aElementOf0(sbrdtbr0(_121955), szNzAzT0), -(isFinite0(_121955))], (757 ^ _99066) ^ [] : [isFinite0(_121955), -(aElementOf0(sbrdtbr0(_121955), szNzAzT0))]]], (132 ^ _99066) ^ [_103375, _103377, _103379, _103381] : [-(sdtmndt0(_103381, _103377) = sdtmndt0(_103379, _103375)), _103381 = _103379, _103377 = _103375], (192 ^ _99066) ^ [_105115] : [_105115 = slcrc0, 195 ^ _99066 : [(196 ^ _99066) ^ [] : [-(aSet0(_105115))], (198 ^ _99066) ^ [_105296] : [aElementOf0(_105296, _105115)]]], (296 ^ _99066) ^ [_108248, _108250] : [aSet0(_108250), aSet0(_108248), -(_108250 = _108248), aSubsetOf0(_108250, _108248), aSubsetOf0(_108248, _108250)], (663 ^ _99066) ^ [_119641, _119643] : [aElementOf0(_119643, szNzAzT0), aElementOf0(_119641, szNzAzT0), -(_119643 = _119641), sdtlseqdt0(_119643, _119641), sdtlseqdt0(_119641, _119643)], (92 ^ _99066) ^ [_102031, _102033] : [-(aElement0(_102031)), _102033 = _102031, aElement0(_102033)], (657 ^ _99066) ^ [_119437] : [aElementOf0(_119437, szNzAzT0), -(sdtlseqdt0(_119437, _119437))], (102 ^ _99066) ^ [_102334, _102336, _102338, _102340] : [-(aElementOf0(_102338, _102334)), aElementOf0(_102340, _102336), _102340 = _102338, _102336 = _102334], (314 ^ _99066) ^ [_108737, _108739, _108741] : [aSet0(_108741), aSet0(_108739), aSet0(_108737), -(aSubsetOf0(_108741, _108737)), aSubsetOf0(_108741, _108739), aSubsetOf0(_108739, _108737)], (763 ^ _99066) ^ [_122386] : [aSet0(_122386), 766 ^ _99066 : [(767 ^ _99066) ^ [] : [sbrdtbr0(_122386) = sz00, -(_122386 = slcrc0)], (773 ^ _99066) ^ [] : [_122386 = slcrc0, -(sbrdtbr0(_122386) = sz00)]]]], input).
% 189.85/183.35 ncf('1',plain,[szszuzczcdt0(sbrdtbr0(sdtmndt0(xS, xx))) = sbrdtbr0(xS)],start(829 ^ 0)).
% 189.85/183.35 ncf('1.1',plain,[-(szszuzczcdt0(sbrdtbr0(sdtmndt0(xS, xx))) = sbrdtbr0(xS)), sbrdtbr0(xS) = szszuzczcdt0(sbrdtbr0(sdtmndt0(xS, xx)))],extension(4 ^ 1,bind([[_99297, _99299], [szszuzczcdt0(sbrdtbr0(sdtmndt0(xS, xx))), sbrdtbr0(xS)]]))).
% 189.85/183.35 ncf('1.1.1',plain,[-(sbrdtbr0(xS) = szszuzczcdt0(sbrdtbr0(sdtmndt0(xS, xx)))), sbrdtbr0(xS) = sbrdtbr0(sdtpldt0(sdtmndt0(xS, xx), xx)), sbrdtbr0(sdtpldt0(sdtmndt0(xS, xx), xx)) = szszuzczcdt0(sbrdtbr0(sdtmndt0(xS, xx)))],extension(10 ^ 2,bind([[_99501, _99503, _99505], [szszuzczcdt0(sbrdtbr0(sdtmndt0(xS, xx))), sbrdtbr0(sdtpldt0(sdtmndt0(xS, xx), xx)), sbrdtbr0(xS)]]))).
% 189.85/183.35 ncf('1.1.1.1',plain,[-(sbrdtbr0(xS) = sbrdtbr0(sdtpldt0(sdtmndt0(xS, xx), xx))), xS = sdtpldt0(sdtmndt0(xS, xx), xx)],extension(142 ^ 3,bind([[_103686, _103688], [sdtpldt0(sdtmndt0(xS, xx), xx), xS]]))).
% 189.85/183.35 ncf('1.1.1.1.1',plain,[-(xS = sdtpldt0(sdtmndt0(xS, xx), xx)), sdtpldt0(sdtmndt0(xS, xx), xx) = xS],extension(4 ^ 4,bind([[_99297, _99299], [xS, sdtpldt0(sdtmndt0(xS, xx), xx)]]))).
% 189.85/183.35 ncf('1.1.1.1.1.1',plain,[-(sdtpldt0(sdtmndt0(xS, xx), xx) = xS), 478 : aElementOf0(xx, xS), 478 : aSet0(xS)],extension(474 ^ 5,bind([[_113919, _114056], [xS, xx]]))).
% 189.85/183.35 ncf('1.1.1.1.1.1.1',plain,[-(aElementOf0(xx, xS))],extension(801 ^ 8)).
% 189.85/183.35 ncf('1.1.1.1.1.1.2',plain,[-(aSet0(xS))],extension(797 ^ 6)).
% 189.85/183.35 ncf('1.1.1.2',plain,[-(sbrdtbr0(sdtpldt0(sdtmndt0(xS, xx), xx)) = szszuzczcdt0(sbrdtbr0(sdtmndt0(xS, xx)))), 787 : aElement0(xx), 787 : -(aElementOf0(xx, sdtmndt0(xS, xx))), 787 : aSet0(sdtmndt0(xS, xx)), 787 : isFinite0(sdtmndt0(xS, xx))],extension(779 ^ 3,bind([[_122820, _123050], [sdtmndt0(xS, xx), xx]]))).
% 189.85/183.35 ncf('1.1.1.2.1',plain,[-(aElement0(xx)), 172 : aElementOf0(xx, xS), 172 : aSet0(xS)],extension(168 ^ 6,bind([[_104414, _104544], [xS, xx]]))).
% 189.85/183.35 ncf('1.1.1.2.1.1',plain,[-(aElementOf0(xx, xS))],extension(801 ^ 9)).
% 189.85/183.35 ncf('1.1.1.2.1.2',plain,[-(aSet0(xS))],extension(797 ^ 7)).
% 189.85/183.35 ncf('1.1.1.2.2',plain,[aElementOf0(xx, sdtmndt0(xS, xx)), 813 : xx = xx],extension(805 ^ 6,bind([[_123859], [xx]]))).
% 189.85/183.35 ncf('1.1.1.2.2.1',plain,[-(xx = xx)],extension(2 ^ 9,bind([[_99190], [xx]]))).
% 189.85/183.35 ncf('1.1.1.2.3',plain,[-(aSet0(sdtmndt0(xS, xx)))],extension(803 ^ 4)).
% 189.85/183.35 ncf('1.1.1.2.4',plain,[-(isFinite0(sdtmndt0(xS, xx))), 544 : aSet0(xS), 544 : isFinite0(xS), 544 : aElement0(xx)],extension(540 ^ 4,bind([[_115959, _116096], [xx, xS]]))).
% 189.85/183.35 ncf('1.1.1.2.4.1',plain,[-(aSet0(xS))],extension(797 ^ 7)).
% 189.85/183.35 ncf('1.1.1.2.4.2',plain,[-(isFinite0(xS))],extension(799 ^ 7)).
% 189.85/183.35 ncf('1.1.1.2.4.3',plain,[-(aElement0(xx)), 172 : aElementOf0(xx, xS), 172 : aSet0(xS)],extension(168 ^ 5,bind([[_104414, _104544], [xS, xx]]))).
% 189.85/183.35 ncf('1.1.1.2.4.3.1',plain,[-(aElementOf0(xx, xS))],extension(801 ^ 8)).
% 189.85/183.35 ncf('1.1.1.2.4.3.2',plain,[-(aSet0(xS))],extension(797 ^ 6)).
% 189.85/183.35 %-----------------------------------------------------
% 189.85/183.35 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------