%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM520+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n022.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.35s 1.38s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM520+1 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n022.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:36:17 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.35/1.38
% 0.35/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.35/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.35/1.38 %-----------------------------------------------------
% 0.35/1.38 ncf(matrix, plain, [(866 ^ _109574) ^ [] : [doDivides0(xp, xn)], (868 ^ _109574) ^ [] : [doDivides0(xp, xm)], (82 ^ _109574) ^ [_112286, _112288, _112290, _112292] : [-(sdtmndt0(_112292, _112288) = sdtmndt0(_112290, _112286)), _112292 = _112290, _112288 = _112286], (92 ^ _109574) ^ [_112645, _112647, _112649, _112651] : [-(sdtpldt0(_112651, _112647) = sdtpldt0(_112649, _112645)), _112651 = _112649, _112647 = _112645], (102 ^ _109574) ^ [_113004, _113006, _113008, _113010] : [-(sdtsldt0(_113010, _113006) = sdtsldt0(_113008, _113004)), _113010 = _113008, _113006 = _113004], (112 ^ _109574) ^ [_113343, _113345, _113347, _113349] : [-(sdtasdt0(_113349, _113345) = sdtasdt0(_113347, _113343)), _113349 = _113347, _113345 = _113343], (2 ^ _109574) ^ [_109718] : [-(_109718 = _109718)], (4 ^ _109574) ^ [_109825, _109827] : [_109827 = _109825, -(_109825 = _109827)], (10 ^ _109574) ^ [_110029, _110031, _110033] : [-(_110033 = _110029), _110033 = _110031, _110031 = _110029], (20 ^ _109574) ^ [_110342, _110344] : [-(aNaturalNumber0(_110342)), _110344 = _110342, aNaturalNumber0(_110344)], (30 ^ _109574) ^ [_110665, _110667, _110669, _110671] : [-(iLess0(_110669, _110665)), iLess0(_110671, _110667), _110671 = _110669, _110667 = _110665], (44 ^ _109574) ^ [_111081, _111083] : [-(isPrime0(_111081)), _111083 = _111081, isPrime0(_111083)], (54 ^ _109574) ^ [_111404, _111406, _111408, _111410] : [-(sdtlseqdt0(_111408, _111404)), sdtlseqdt0(_111410, _111406), _111410 = _111408, _111406 = _111404], (68 ^ _109574) ^ [_111828, _111830, _111832, _111834] : [-(doDivides0(_111832, _111828)), doDivides0(_111834, _111830), _111834 = _111832, _111830 = _111828], (122 ^ _109574) ^ [_113674] : [aNaturalNumber0(_113674), true___, -(true___)], (132 ^ _109574) ^ [] : [-(aNaturalNumber0(sz00))], (134 ^ _109574) ^ [] : [-(aNaturalNumber0(sz10))], (136 ^ _109574) ^ [] : [sz10 = sz00], (138 ^ _109574) ^ [_114103, _114105] : [-(aNaturalNumber0(sdtpldt0(_114105, _114103))), aNaturalNumber0(_114105), aNaturalNumber0(_114103)], (148 ^ _109574) ^ [_114402, _114404] : [-(aNaturalNumber0(sdtasdt0(_114404, _114402))), aNaturalNumber0(_114404), aNaturalNumber0(_114402)], (158 ^ _109574) ^ [_114701, _114703] : [-(sdtpldt0(_114703, _114701) = sdtpldt0(_114701, _114703)), aNaturalNumber0(_114703), aNaturalNumber0(_114701)], (168 ^ _109574) ^ [_115022, _115024, _115026] : [-(sdtpldt0(sdtpldt0(_115026, _115024), _115022) = sdtpldt0(_115026, sdtpldt0(_115024, _115022))), aNaturalNumber0(_115026), aNaturalNumber0(_115024), aNaturalNumber0(_115022)], (182 ^ _109574) ^ [_115428] : [aNaturalNumber0(_115428), 185 ^ _109574 : [(186 ^ _109574) ^ [] : [-(sdtpldt0(_115428, sz00) = _115428)], (188 ^ _109574) ^ [] : [-(_115428 = sdtpldt0(sz00, _115428))]]], (190 ^ _109574) ^ [_115715, _115717] : [-(sdtasdt0(_115717, _115715) = sdtasdt0(_115715, _115717)), aNaturalNumber0(_115717), aNaturalNumber0(_115715)], (200 ^ _109574) ^ [_116036, _116038, _116040] : [-(sdtasdt0(sdtasdt0(_116040, _116038), _116036) = sdtasdt0(_116040, sdtasdt0(_116038, _116036))), aNaturalNumber0(_116040), aNaturalNumber0(_116038), aNaturalNumber0(_116036)], (214 ^ _109574) ^ [_116442] : [aNaturalNumber0(_116442), 217 ^ _109574 : [(218 ^ _109574) ^ [] : [-(sdtasdt0(_116442, sz10) = _116442)], (220 ^ _109574) ^ [] : [-(_116442 = sdtasdt0(sz10, _116442))]]], (222 ^ _109574) ^ [_116715] : [aNaturalNumber0(_116715), 225 ^ _109574 : [(226 ^ _109574) ^ [] : [-(sdtasdt0(_116715, sz00) = sz00)], (228 ^ _109574) ^ [] : [-(sz00 = sdtasdt0(sz00, _116715))]]], (230 ^ _109574) ^ [_117016, _117018, _117020] : [241 ^ _109574 : [(242 ^ _109574) ^ [] : [-(sdtasdt0(_117020, sdtpldt0(_117018, _117016)) = sdtpldt0(sdtasdt0(_117020, _117018), sdtasdt0(_117020, _117016)))], (244 ^ _109574) ^ [] : [-(sdtasdt0(sdtpldt0(_117018, _117016), _117020) = sdtpldt0(sdtasdt0(_117018, _117020), sdtasdt0(_117016, _117020)))]], aNaturalNumber0(_117020), aNaturalNumber0(_117018), aNaturalNumber0(_117016)], (246 ^ _109574) ^ [_117563, _117565, _117567] : [259 ^ _109574 : [(260 ^ _109574) ^ [] : [sdtpldt0(_117567, _117565) = sdtpldt0(_117567, _117563)], (262 ^ _109574) ^ [] : [sdtpldt0(_117565, _117567) = sdtpldt0(_117563, _117567)]], -(_117565 = _117563), aNaturalNumber0(_117567), aNaturalNumber0(_117565), aNaturalNumber0(_117563)], (266 ^ _109574) ^ [_118140] : [aNaturalNumber0(_118140), -(_118140 = sz00), 273 ^ _109574 : [(274 ^ _109574) ^ [_118402, _118404] : [aNaturalNumber0(_118404), aNaturalNumber0(_118402), 283 ^ _109574 : [(284 ^ _109574) ^ [] : [sdtasdt0(_118140, _118404) = sdtasdt0(_118140, _118402)], (286 ^ _109574) ^ [] : [sdtasdt0(_118404, _118140) = sdtasdt0(_118402, _118140)]], -(_118404 = _118402)]]], (290 ^ _109574) ^ [_118913, _118915] : [aNaturalNumber0(_118915), aNaturalNumber0(_118913), sdtpldt0(_118915, _118913) = sz00, 301 ^ _109574 : [(302 ^ _109574) ^ [] : [-(_118915 = sz00)], (304 ^ _109574) ^ [] : [-(_118913 = sz00)]]], (306 ^ _109574) ^ [_119380, _119382] : [aNaturalNumber0(_119382), aNaturalNumber0(_119380), sdtasdt0(_119382, _119380) = sz00, -(_119382 = sz00), -(_119380 = sz00)], (324 ^ _109574) ^ [_119862, _119864] : [aNaturalNumber0(_119864), aNaturalNumber0(_119862), 331 ^ _109574 : [(332 ^ _109574) ^ [] : [sdtlseqdt0(_119864, _119862), 336 ^ _109574 : [(337 ^ _109574) ^ [] : [-(aNaturalNumber0(335 ^ [_119862, _119864]))], (339 ^ _109574) ^ [] : [-(sdtpldt0(_119864, 335 ^ [_119862, _119864]) = _119862)]]], (341 ^ _109574) ^ [] : [-(sdtlseqdt0(_119864, _119862)), 342 ^ _109574 : [(343 ^ _109574) ^ [_120422] : [aNaturalNumber0(_120422), sdtpldt0(_119864, _120422) = _119862]]]]], (351 ^ _109574) ^ [_120705, _120707] : [aNaturalNumber0(_120707), aNaturalNumber0(_120705), sdtlseqdt0(_120707, _120705), 362 ^ _109574 : [(363 ^ _109574) ^ [_121052] : [_121052 = sdtmndt0(_120705, _120707), 366 ^ _109574 : [(367 ^ _109574) ^ [] : [-(aNaturalNumber0(_121052))], (369 ^ _109574) ^ [] : [-(sdtpldt0(_120707, _121052) = _120705)]]], (371 ^ _109574) ^ [_121311] : [-(_121311 = sdtmndt0(_120705, _120707)), aNaturalNumber0(_121311), sdtpldt0(_120707, _121311) = _120705]]], (381 ^ _109574) ^ [_121633] : [aNaturalNumber0(_121633), -(sdtlseqdt0(_121633, _121633))], (387 ^ _109574) ^ [_121835, _121837] : [aNaturalNumber0(_121837), aNaturalNumber0(_121835), -(_121837 = _121835), sdtlseqdt0(_121837, _121835), sdtlseqdt0(_121835, _121837)], (405 ^ _109574) ^ [_122324, _122326, _122328] : [aNaturalNumber0(_122328), aNaturalNumber0(_122326), aNaturalNumber0(_122324), -(sdtlseqdt0(_122328, _122324)), sdtlseqdt0(_122328, _122326), sdtlseqdt0(_122326, _122324)], (427 ^ _109574) ^ [_122910, _122912] : [aNaturalNumber0(_122912), aNaturalNumber0(_122910), -(sdtlseqdt0(_122912, _122910)), 438 ^ _109574 : [(439 ^ _109574) ^ [] : [_122910 = _122912], (441 ^ _109574) ^ [] : [-(sdtlseqdt0(_122910, _122912))]]], (443 ^ _109574) ^ [_123373, _123375] : [aNaturalNumber0(_123375), aNaturalNumber0(_123373), -(_123375 = _123373), sdtlseqdt0(_123375, _123373), 458 ^ _109574 : [(459 ^ _109574) ^ [_123817] : [aNaturalNumber0(_123817), 462 ^ _109574 : [(463 ^ _109574) ^ [] : [sdtpldt0(_123817, _123375) = sdtpldt0(_123817, _123373)], (465 ^ _109574) ^ [] : [-(sdtlseqdt0(sdtpldt0(_123817, _123375), sdtpldt0(_123817, _123373)))], (467 ^ _109574) ^ [] : [sdtpldt0(_123375, _123817) = sdtpldt0(_123373, _123817)], (469 ^ _109574) ^ [] : [-(sdtlseqdt0(sdtpldt0(_123375, _123817), sdtpldt0(_123373, _123817)))]]]]], (471 ^ _109574) ^ [_124341, _124343, _124345] : [aNaturalNumber0(_124345), aNaturalNumber0(_124343), aNaturalNumber0(_124341), 494 ^ _109574 : [(495 ^ _109574) ^ [] : [sdtasdt0(_124345, _124343) = sdtasdt0(_124345, _124341)], (497 ^ _109574) ^ [] : [-(sdtlseqdt0(sdtasdt0(_124345, _124343), sdtasdt0(_124345, _124341)))], (499 ^ _109574) ^ [] : [sdtasdt0(_124343, _124345) = sdtasdt0(_124341, _124345)], (501 ^ _109574) ^ [] : [-(sdtlseqdt0(sdtasdt0(_124343, _124345), sdtasdt0(_124341, _124345)))]], -(_124345 = sz00), -(_124343 = _124341), sdtlseqdt0(_124343, _124341)], (503 ^ _109574) ^ [_125291] : [aNaturalNumber0(_125291), -(_125291 = sz00), -(_125291 = sz10), 514 ^ _109574 : [(515 ^ _109574) ^ [] : [sz10 = _125291], (517 ^ _109574) ^ [] : [-(sdtlseqdt0(sz10, _125291))]]], (519 ^ _109574) ^ [_125739, _125741] : [aNaturalNumber0(_125741), aNaturalNumber0(_125739), -(_125741 = sz00), -(sdtlseqdt0(_125739, sdtasdt0(_125739, _125741)))], (533 ^ _109574) ^ [_126134, _126136] : [aNaturalNumber0(_126136), aNaturalNumber0(_126134), iLess0(_126136, _126134), true___, -(true___)], (551 ^ _109574) ^ [_126594, _126596] : [aNaturalNumber0(_126596), aNaturalNumber0(_126594), -(iLess0(_126596, _126594)), -(_126596 = _126594), sdtlseqdt0(_126596, _126594)], (569 ^ _109574) ^ [_127072, _127074] : [aNaturalNumber0(_127074), aNaturalNumber0(_127072), 576 ^ _109574 : [(577 ^ _109574) ^ [] : [doDivides0(_127074, _127072), 581 ^ _109574 : [(582 ^ _109574) ^ [] : [-(aNaturalNumber0(580 ^ [_127072, _127074]))], (584 ^ _109574) ^ [] : [-(_127072 = sdtasdt0(_127074, 580 ^ [_127072, _127074]))]]], (586 ^ _109574) ^ [] : [-(doDivides0(_127074, _127072)), 587 ^ _109574 : [(588 ^ _109574) ^ [_127632] : [aNaturalNumber0(_127632), _127072 = sdtasdt0(_127074, _127632)]]]]], (596 ^ _109574) ^ [_127915, _127917] : [aNaturalNumber0(_127917), aNaturalNumber0(_127915), -(_127917 = sz00), doDivides0(_127917, _127915), 611 ^ _109574 : [(612 ^ _109574) ^ [_128354] : [_128354 = sdtsldt0(_127915, _127917), 615 ^ _109574 : [(616 ^ _109574) ^ [] : [-(aNaturalNumber0(_128354))], (618 ^ _109574) ^ [] : [-(_127915 = sdtasdt0(_127917, _128354))]]], (620 ^ _109574) ^ [_128613] : [-(_128613 = sdtsldt0(_127915, _127917)), aNaturalNumber0(_128613), _127915 = sdtasdt0(_127917, _128613)]]], (630 ^ _109574) ^ [_128965, _128967, _128969] : [aNaturalNumber0(_128969), aNaturalNumber0(_128967), aNaturalNumber0(_128965), -(doDivides0(_128969, _128965)), doDivides0(_128969, _128967), doDivides0(_128967, _128965)], (652 ^ _109574) ^ [_129565, _129567, _129569] : [aNaturalNumber0(_129569), aNaturalNumber0(_129567), aNaturalNumber0(_129565), -(doDivides0(_129569, sdtpldt0(_129567, _129565))), doDivides0(_129569, _129567), doDivides0(_129569, _129565)], (674 ^ _109574) ^ [_130171, _130173, _130175] : [aNaturalNumber0(_130175), aNaturalNumber0(_130173), aNaturalNumber0(_130171), -(doDivides0(_130175, _130171)), doDivides0(_130175, _130173), doDivides0(_130175, sdtpldt0(_130173, _130171))], (696 ^ _109574) ^ [_130763, _130765] : [aNaturalNumber0(_130765), aNaturalNumber0(_130763), -(sdtlseqdt0(_130765, _130763)), doDivides0(_130765, _130763), -(_130763 = sz00)], (714 ^ _109574) ^ [_131241, _131243] : [aNaturalNumber0(_131243), aNaturalNumber0(_131241), -(_131243 = sz00), doDivides0(_131243, _131241), 729 ^ _109574 : [(730 ^ _109574) ^ [_131651] : [aNaturalNumber0(_131651), -(sdtasdt0(_131651, sdtsldt0(_131241, _131243)) = sdtsldt0(sdtasdt0(_131651, _131241), _131243))]]], (736 ^ _109574) ^ [_131892] : [aNaturalNumber0(_131892), 739 ^ _109574 : [(762 ^ _109574) ^ [] : [-(isPrime0(_131892)), -(_131892 = sz00), -(_131892 = sz10), 772 ^ _109574 : [(773 ^ _109574) ^ [] : [-(aNaturalNumber0(771 ^ [_131892]))], (775 ^ _109574) ^ [] : [-(doDivides0(771 ^ [_131892], _131892))], (777 ^ _109574) ^ [] : [771 ^ [_131892] = sz10], (779 ^ _109574) ^ [] : [771 ^ [_131892] = _131892]]], (740 ^ _109574) ^ [] : [isPrime0(_131892), 743 ^ _109574 : [(744 ^ _109574) ^ [] : [_131892 = sz00], (746 ^ _109574) ^ [] : [_131892 = sz10], (748 ^ _109574) ^ [_132284] : [aNaturalNumber0(_132284), doDivides0(_132284, _131892), -(_132284 = sz10), -(_132284 = _131892)]]]]], (783 ^ _109574) ^ [_133236] : [795 ^ _109574 : [(796 ^ _109574) ^ [] : [-(aNaturalNumber0(794 ^ [_133236]))], (798 ^ _109574) ^ [] : [-(doDivides0(794 ^ [_133236], _133236))], (800 ^ _109574) ^ [] : [-(isPrime0(794 ^ [_133236]))]], aNaturalNumber0(_133236), -(_133236 = sz00), -(_133236 = sz10)], (802 ^ _109574) ^ [] : [-(aNaturalNumber0(xn))], (804 ^ _109574) ^ [] : [-(aNaturalNumber0(xm))], (806 ^ _109574) ^ [] : [-(aNaturalNumber0(xp))], (838 ^ _109574) ^ [] : [-(isPrime0(xp))], (840 ^ _109574) ^ [] : [-(doDivides0(xp, sdtasdt0(xn, xm)))], (842 ^ _109574) ^ [] : [sdtlseqdt0(xp, xn)], (844 ^ _109574) ^ [] : [sdtlseqdt0(xp, xm)], (846 ^ _109574) ^ [] : [xn = xp], (848 ^ _109574) ^ [] : [-(sdtlseqdt0(xn, xp))], (850 ^ _109574) ^ [] : [xm = xp], (852 ^ _109574) ^ [] : [-(sdtlseqdt0(xm, xp))], (854 ^ _109574) ^ [] : [-(xk = sdtsldt0(sdtasdt0(xn, xm), xp))], (856 ^ _109574) ^ [] : [xk = sz00], (858 ^ _109574) ^ [] : [xk = sz10], (860 ^ _109574) ^ [] : [-(xk = sz00), -(xk = sz10)], (808 ^ _109574) ^ [_134003, _134005, _134007] : [aNaturalNumber0(_134007), aNaturalNumber0(_134005), aNaturalNumber0(_134003), isPrime0(_134003), doDivides0(_134003, sdtasdt0(_134007, _134005)), iLess0(sdtpldt0(sdtpldt0(_134007, _134005), _134003), sdtpldt0(sdtpldt0(xn, xm), xp)), -(doDivides0(_134003, _134007)), -(doDivides0(_134003, _134005))]], input).
% 0.35/1.38 ncf('1',plain,[xk = sz00],start(856 ^ 0)).
% 0.35/1.38 ncf('1.1',plain,[-(xk = sz00), -(xk = sz10)],extension(860 ^ 1)).
% 0.35/1.38 ncf('1.1.1',plain,[xk = sz10],extension(858 ^ 2)).
% 0.35/1.38 %-----------------------------------------------------
% 0.35/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------