%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM500+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n003.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:47 EDT 2023
% Result : Theorem 2.16s 2.43s
% Output : Proof 2.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : NUM500+1 : TPTP v8.1.2. Released v4.0.0.
% 0.13/0.14 % Command : nanocop.sh %s %d
% 0.13/0.35 % Computer : n003.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 18 17:41:30 EDT 2023
% 0.20/0.35 % CPUTime :
% 2.16/2.43
% 2.16/2.43 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 2.16/2.43 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.16/2.43 %-----------------------------------------------------
% 2.16/2.43 ncf(matrix, plain, [(864 ^ _114150) ^ [_140324] : [aNaturalNumber0(_140324), doDivides0(_140324, xk), isPrime0(_140324)], (82 ^ _114150) ^ [_116862, _116864, _116866, _116868] : [-(sdtmndt0(_116868, _116864) = sdtmndt0(_116866, _116862)), _116868 = _116866, _116864 = _116862], (92 ^ _114150) ^ [_117221, _117223, _117225, _117227] : [-(sdtpldt0(_117227, _117223) = sdtpldt0(_117225, _117221)), _117227 = _117225, _117223 = _117221], (102 ^ _114150) ^ [_117580, _117582, _117584, _117586] : [-(sdtsldt0(_117586, _117582) = sdtsldt0(_117584, _117580)), _117586 = _117584, _117582 = _117580], (112 ^ _114150) ^ [_117919, _117921, _117923, _117925] : [-(sdtasdt0(_117925, _117921) = sdtasdt0(_117923, _117919)), _117925 = _117923, _117921 = _117919], (2 ^ _114150) ^ [_114294] : [-(_114294 = _114294)], (4 ^ _114150) ^ [_114401, _114403] : [_114403 = _114401, -(_114401 = _114403)], (10 ^ _114150) ^ [_114605, _114607, _114609] : [-(_114609 = _114605), _114609 = _114607, _114607 = _114605], (20 ^ _114150) ^ [_114946, _114948, _114950, _114952] : [-(iLess0(_114950, _114946)), iLess0(_114952, _114948), _114952 = _114950, _114948 = _114946], (34 ^ _114150) ^ [_115390, _115392, _115394, _115396] : [-(sdtlseqdt0(_115394, _115390)), sdtlseqdt0(_115396, _115392), _115396 = _115394, _115392 = _115390], (48 ^ _114150) ^ [_115806, _115808] : [-(aNaturalNumber0(_115806)), _115808 = _115806, aNaturalNumber0(_115808)], (72 ^ _114150) ^ [_116525, _116527] : [-(isPrime0(_116525)), _116527 = _116525, isPrime0(_116527)], (58 ^ _114150) ^ [_116129, _116131, _116133, _116135] : [-(doDivides0(_116133, _116129)), doDivides0(_116135, _116131), _116135 = _116133, _116131 = _116129], (122 ^ _114150) ^ [_118250] : [aNaturalNumber0(_118250), true___, -(true___)], (132 ^ _114150) ^ [] : [-(aNaturalNumber0(sz00))], (134 ^ _114150) ^ [] : [-(aNaturalNumber0(sz10))], (136 ^ _114150) ^ [] : [sz10 = sz00], (138 ^ _114150) ^ [_118679, _118681] : [-(aNaturalNumber0(sdtpldt0(_118681, _118679))), aNaturalNumber0(_118681), aNaturalNumber0(_118679)], (148 ^ _114150) ^ [_118978, _118980] : [-(aNaturalNumber0(sdtasdt0(_118980, _118978))), aNaturalNumber0(_118980), aNaturalNumber0(_118978)], (158 ^ _114150) ^ [_119277, _119279] : [-(sdtpldt0(_119279, _119277) = sdtpldt0(_119277, _119279)), aNaturalNumber0(_119279), aNaturalNumber0(_119277)], (168 ^ _114150) ^ [_119598, _119600, _119602] : [-(sdtpldt0(sdtpldt0(_119602, _119600), _119598) = sdtpldt0(_119602, sdtpldt0(_119600, _119598))), aNaturalNumber0(_119602), aNaturalNumber0(_119600), aNaturalNumber0(_119598)], (182 ^ _114150) ^ [_120004] : [aNaturalNumber0(_120004), 185 ^ _114150 : [(186 ^ _114150) ^ [] : [-(sdtpldt0(_120004, sz00) = _120004)], (188 ^ _114150) ^ [] : [-(_120004 = sdtpldt0(sz00, _120004))]]], (190 ^ _114150) ^ [_120291, _120293] : [-(sdtasdt0(_120293, _120291) = sdtasdt0(_120291, _120293)), aNaturalNumber0(_120293), aNaturalNumber0(_120291)], (200 ^ _114150) ^ [_120612, _120614, _120616] : [-(sdtasdt0(sdtasdt0(_120616, _120614), _120612) = sdtasdt0(_120616, sdtasdt0(_120614, _120612))), aNaturalNumber0(_120616), aNaturalNumber0(_120614), aNaturalNumber0(_120612)], (214 ^ _114150) ^ [_121018] : [aNaturalNumber0(_121018), 217 ^ _114150 : [(218 ^ _114150) ^ [] : [-(sdtasdt0(_121018, sz10) = _121018)], (220 ^ _114150) ^ [] : [-(_121018 = sdtasdt0(sz10, _121018))]]], (222 ^ _114150) ^ [_121291] : [aNaturalNumber0(_121291), 225 ^ _114150 : [(226 ^ _114150) ^ [] : [-(sdtasdt0(_121291, sz00) = sz00)], (228 ^ _114150) ^ [] : [-(sz00 = sdtasdt0(sz00, _121291))]]], (230 ^ _114150) ^ [_121592, _121594, _121596] : [241 ^ _114150 : [(242 ^ _114150) ^ [] : [-(sdtasdt0(_121596, sdtpldt0(_121594, _121592)) = sdtpldt0(sdtasdt0(_121596, _121594), sdtasdt0(_121596, _121592)))], (244 ^ _114150) ^ [] : [-(sdtasdt0(sdtpldt0(_121594, _121592), _121596) = sdtpldt0(sdtasdt0(_121594, _121596), sdtasdt0(_121592, _121596)))]], aNaturalNumber0(_121596), aNaturalNumber0(_121594), aNaturalNumber0(_121592)], (246 ^ _114150) ^ [_122139, _122141, _122143] : [259 ^ _114150 : [(260 ^ _114150) ^ [] : [sdtpldt0(_122143, _122141) = sdtpldt0(_122143, _122139)], (262 ^ _114150) ^ [] : [sdtpldt0(_122141, _122143) = sdtpldt0(_122139, _122143)]], -(_122141 = _122139), aNaturalNumber0(_122143), aNaturalNumber0(_122141), aNaturalNumber0(_122139)], (266 ^ _114150) ^ [_122716] : [aNaturalNumber0(_122716), -(_122716 = sz00), 273 ^ _114150 : [(274 ^ _114150) ^ [_122978, _122980] : [aNaturalNumber0(_122980), aNaturalNumber0(_122978), 283 ^ _114150 : [(284 ^ _114150) ^ [] : [sdtasdt0(_122716, _122980) = sdtasdt0(_122716, _122978)], (286 ^ _114150) ^ [] : [sdtasdt0(_122980, _122716) = sdtasdt0(_122978, _122716)]], -(_122980 = _122978)]]], (290 ^ _114150) ^ [_123489, _123491] : [aNaturalNumber0(_123491), aNaturalNumber0(_123489), sdtpldt0(_123491, _123489) = sz00, 301 ^ _114150 : [(302 ^ _114150) ^ [] : [-(_123491 = sz00)], (304 ^ _114150) ^ [] : [-(_123489 = sz00)]]], (306 ^ _114150) ^ [_123956, _123958] : [aNaturalNumber0(_123958), aNaturalNumber0(_123956), sdtasdt0(_123958, _123956) = sz00, -(_123958 = sz00), -(_123956 = sz00)], (324 ^ _114150) ^ [_124438, _124440] : [aNaturalNumber0(_124440), aNaturalNumber0(_124438), 331 ^ _114150 : [(332 ^ _114150) ^ [] : [sdtlseqdt0(_124440, _124438), 336 ^ _114150 : [(337 ^ _114150) ^ [] : [-(aNaturalNumber0(335 ^ [_124438, _124440]))], (339 ^ _114150) ^ [] : [-(sdtpldt0(_124440, 335 ^ [_124438, _124440]) = _124438)]]], (341 ^ _114150) ^ [] : [-(sdtlseqdt0(_124440, _124438)), 342 ^ _114150 : [(343 ^ _114150) ^ [_124998] : [aNaturalNumber0(_124998), sdtpldt0(_124440, _124998) = _124438]]]]], (351 ^ _114150) ^ [_125281, _125283] : [aNaturalNumber0(_125283), aNaturalNumber0(_125281), sdtlseqdt0(_125283, _125281), 362 ^ _114150 : [(363 ^ _114150) ^ [_125628] : [_125628 = sdtmndt0(_125281, _125283), 366 ^ _114150 : [(367 ^ _114150) ^ [] : [-(aNaturalNumber0(_125628))], (369 ^ _114150) ^ [] : [-(sdtpldt0(_125283, _125628) = _125281)]]], (371 ^ _114150) ^ [_125887] : [-(_125887 = sdtmndt0(_125281, _125283)), aNaturalNumber0(_125887), sdtpldt0(_125283, _125887) = _125281]]], (381 ^ _114150) ^ [_126209] : [aNaturalNumber0(_126209), -(sdtlseqdt0(_126209, _126209))], (387 ^ _114150) ^ [_126411, _126413] : [aNaturalNumber0(_126413), aNaturalNumber0(_126411), -(_126413 = _126411), sdtlseqdt0(_126413, _126411), sdtlseqdt0(_126411, _126413)], (405 ^ _114150) ^ [_126900, _126902, _126904] : [aNaturalNumber0(_126904), aNaturalNumber0(_126902), aNaturalNumber0(_126900), -(sdtlseqdt0(_126904, _126900)), sdtlseqdt0(_126904, _126902), sdtlseqdt0(_126902, _126900)], (427 ^ _114150) ^ [_127486, _127488] : [aNaturalNumber0(_127488), aNaturalNumber0(_127486), -(sdtlseqdt0(_127488, _127486)), 438 ^ _114150 : [(439 ^ _114150) ^ [] : [_127486 = _127488], (441 ^ _114150) ^ [] : [-(sdtlseqdt0(_127486, _127488))]]], (443 ^ _114150) ^ [_127949, _127951] : [aNaturalNumber0(_127951), aNaturalNumber0(_127949), -(_127951 = _127949), sdtlseqdt0(_127951, _127949), 458 ^ _114150 : [(459 ^ _114150) ^ [_128393] : [aNaturalNumber0(_128393), 462 ^ _114150 : [(463 ^ _114150) ^ [] : [sdtpldt0(_128393, _127951) = sdtpldt0(_128393, _127949)], (465 ^ _114150) ^ [] : [-(sdtlseqdt0(sdtpldt0(_128393, _127951), sdtpldt0(_128393, _127949)))], (467 ^ _114150) ^ [] : [sdtpldt0(_127951, _128393) = sdtpldt0(_127949, _128393)], (469 ^ _114150) ^ [] : [-(sdtlseqdt0(sdtpldt0(_127951, _128393), sdtpldt0(_127949, _128393)))]]]]], (471 ^ _114150) ^ [_128917, _128919, _128921] : [aNaturalNumber0(_128921), aNaturalNumber0(_128919), aNaturalNumber0(_128917), 494 ^ _114150 : [(495 ^ _114150) ^ [] : [sdtasdt0(_128921, _128919) = sdtasdt0(_128921, _128917)], (497 ^ _114150) ^ [] : [-(sdtlseqdt0(sdtasdt0(_128921, _128919), sdtasdt0(_128921, _128917)))], (499 ^ _114150) ^ [] : [sdtasdt0(_128919, _128921) = sdtasdt0(_128917, _128921)], (501 ^ _114150) ^ [] : [-(sdtlseqdt0(sdtasdt0(_128919, _128921), sdtasdt0(_128917, _128921)))]], -(_128921 = sz00), -(_128919 = _128917), sdtlseqdt0(_128919, _128917)], (503 ^ _114150) ^ [_129867] : [aNaturalNumber0(_129867), -(_129867 = sz00), -(_129867 = sz10), 514 ^ _114150 : [(515 ^ _114150) ^ [] : [sz10 = _129867], (517 ^ _114150) ^ [] : [-(sdtlseqdt0(sz10, _129867))]]], (519 ^ _114150) ^ [_130315, _130317] : [aNaturalNumber0(_130317), aNaturalNumber0(_130315), -(_130317 = sz00), -(sdtlseqdt0(_130315, sdtasdt0(_130315, _130317)))], (533 ^ _114150) ^ [_130710, _130712] : [aNaturalNumber0(_130712), aNaturalNumber0(_130710), iLess0(_130712, _130710), true___, -(true___)], (551 ^ _114150) ^ [_131170, _131172] : [aNaturalNumber0(_131172), aNaturalNumber0(_131170), -(iLess0(_131172, _131170)), -(_131172 = _131170), sdtlseqdt0(_131172, _131170)], (569 ^ _114150) ^ [_131648, _131650] : [aNaturalNumber0(_131650), aNaturalNumber0(_131648), 576 ^ _114150 : [(577 ^ _114150) ^ [] : [doDivides0(_131650, _131648), 581 ^ _114150 : [(582 ^ _114150) ^ [] : [-(aNaturalNumber0(580 ^ [_131648, _131650]))], (584 ^ _114150) ^ [] : [-(_131648 = sdtasdt0(_131650, 580 ^ [_131648, _131650]))]]], (586 ^ _114150) ^ [] : [-(doDivides0(_131650, _131648)), 587 ^ _114150 : [(588 ^ _114150) ^ [_132208] : [aNaturalNumber0(_132208), _131648 = sdtasdt0(_131650, _132208)]]]]], (596 ^ _114150) ^ [_132491, _132493] : [aNaturalNumber0(_132493), aNaturalNumber0(_132491), -(_132493 = sz00), doDivides0(_132493, _132491), 611 ^ _114150 : [(612 ^ _114150) ^ [_132930] : [_132930 = sdtsldt0(_132491, _132493), 615 ^ _114150 : [(616 ^ _114150) ^ [] : [-(aNaturalNumber0(_132930))], (618 ^ _114150) ^ [] : [-(_132491 = sdtasdt0(_132493, _132930))]]], (620 ^ _114150) ^ [_133189] : [-(_133189 = sdtsldt0(_132491, _132493)), aNaturalNumber0(_133189), _132491 = sdtasdt0(_132493, _133189)]]], (630 ^ _114150) ^ [_133541, _133543, _133545] : [aNaturalNumber0(_133545), aNaturalNumber0(_133543), aNaturalNumber0(_133541), -(doDivides0(_133545, _133541)), doDivides0(_133545, _133543), doDivides0(_133543, _133541)], (652 ^ _114150) ^ [_134141, _134143, _134145] : [aNaturalNumber0(_134145), aNaturalNumber0(_134143), aNaturalNumber0(_134141), -(doDivides0(_134145, sdtpldt0(_134143, _134141))), doDivides0(_134145, _134143), doDivides0(_134145, _134141)], (674 ^ _114150) ^ [_134747, _134749, _134751] : [aNaturalNumber0(_134751), aNaturalNumber0(_134749), aNaturalNumber0(_134747), -(doDivides0(_134751, _134747)), doDivides0(_134751, _134749), doDivides0(_134751, sdtpldt0(_134749, _134747))], (696 ^ _114150) ^ [_135339, _135341] : [aNaturalNumber0(_135341), aNaturalNumber0(_135339), -(sdtlseqdt0(_135341, _135339)), doDivides0(_135341, _135339), -(_135339 = sz00)], (714 ^ _114150) ^ [_135817, _135819] : [aNaturalNumber0(_135819), aNaturalNumber0(_135817), -(_135819 = sz00), doDivides0(_135819, _135817), 729 ^ _114150 : [(730 ^ _114150) ^ [_136227] : [aNaturalNumber0(_136227), -(sdtasdt0(_136227, sdtsldt0(_135817, _135819)) = sdtsldt0(sdtasdt0(_136227, _135817), _135819))]]], (736 ^ _114150) ^ [_136468] : [aNaturalNumber0(_136468), 739 ^ _114150 : [(762 ^ _114150) ^ [] : [-(isPrime0(_136468)), -(_136468 = sz00), -(_136468 = sz10), 772 ^ _114150 : [(773 ^ _114150) ^ [] : [-(aNaturalNumber0(771 ^ [_136468]))], (775 ^ _114150) ^ [] : [-(doDivides0(771 ^ [_136468], _136468))], (777 ^ _114150) ^ [] : [771 ^ [_136468] = sz10], (779 ^ _114150) ^ [] : [771 ^ [_136468] = _136468]]], (740 ^ _114150) ^ [] : [isPrime0(_136468), 743 ^ _114150 : [(744 ^ _114150) ^ [] : [_136468 = sz00], (746 ^ _114150) ^ [] : [_136468 = sz10], (748 ^ _114150) ^ [_136860] : [aNaturalNumber0(_136860), doDivides0(_136860, _136468), -(_136860 = sz10), -(_136860 = _136468)]]]]], (783 ^ _114150) ^ [_137812] : [795 ^ _114150 : [(796 ^ _114150) ^ [] : [-(aNaturalNumber0(794 ^ [_137812]))], (798 ^ _114150) ^ [] : [-(doDivides0(794 ^ [_137812], _137812))], (800 ^ _114150) ^ [] : [-(isPrime0(794 ^ [_137812]))]], aNaturalNumber0(_137812), -(_137812 = sz00), -(_137812 = sz10)], (802 ^ _114150) ^ [] : [-(aNaturalNumber0(xn))], (804 ^ _114150) ^ [] : [-(aNaturalNumber0(xm))], (806 ^ _114150) ^ [] : [-(aNaturalNumber0(xp))], (838 ^ _114150) ^ [] : [-(isPrime0(xp))], (840 ^ _114150) ^ [] : [-(doDivides0(xp, sdtasdt0(xn, xm)))], (842 ^ _114150) ^ [] : [sdtlseqdt0(xp, xn)], (844 ^ _114150) ^ [] : [sdtlseqdt0(xp, xm)], (846 ^ _114150) ^ [] : [xn = xp], (848 ^ _114150) ^ [] : [-(sdtlseqdt0(xn, xp))], (850 ^ _114150) ^ [] : [xm = xp], (852 ^ _114150) ^ [] : [-(sdtlseqdt0(xm, xp))], (854 ^ _114150) ^ [] : [-(xk = sdtsldt0(sdtasdt0(xn, xm), xp))], (856 ^ _114150) ^ [] : [xk = sz00], (858 ^ _114150) ^ [] : [xk = sz10], (860 ^ _114150) ^ [] : [xk = sz00], (862 ^ _114150) ^ [] : [xk = sz10], (808 ^ _114150) ^ [_138579, _138581, _138583] : [aNaturalNumber0(_138583), aNaturalNumber0(_138581), aNaturalNumber0(_138579), isPrime0(_138579), doDivides0(_138579, sdtasdt0(_138583, _138581)), iLess0(sdtpldt0(sdtpldt0(_138583, _138581), _138579), sdtpldt0(sdtpldt0(xn, xm), xp)), -(doDivides0(_138579, _138583)), -(doDivides0(_138579, _138581))]], input).
% 2.16/2.43 ncf('1',plain,[xk = sz00],start(856 ^ 0)).
% 2.16/2.43 ncf('1.1',plain,[-(xk = sz00), 796 : -(aNaturalNumber0(794 ^ [xk])), 796 : aNaturalNumber0(xk), 796 : -(xk = sz10)],extension(783 ^ 1,bind([[_137812], [xk]]))).
% 2.16/2.43 ncf('1.1.1',plain,[aNaturalNumber0(794 ^ [xk]), doDivides0(794 ^ [xk], xk), isPrime0(794 ^ [xk])],extension(864 ^ 4,bind([[_140324], [794 ^ [xk]]]))).
% 2.16/2.43 ncf('1.1.1.1',plain,[-(doDivides0(794 ^ [xk], xk))],extension(798 ^ 5)).
% 2.16/2.43 ncf('1.1.1.2',plain,[-(isPrime0(794 ^ [xk]))],extension(800 ^ 5)).
% 2.16/2.43 ncf('1.1.2',plain,[-(aNaturalNumber0(xk)), 612 : xk = sdtsldt0(sdtasdt0(xn, xm), xp), 612 : aNaturalNumber0(xp), 612 : aNaturalNumber0(sdtasdt0(xn, xm)), 612 : -(xp = sz00), 612 : doDivides0(xp, sdtasdt0(xn, xm))],extension(596 ^ 2,bind([[_132491, _132493, _132930], [sdtasdt0(xn, xm), xp, xk]]))).
% 2.16/2.43 ncf('1.1.2.1',plain,[-(xk = sdtsldt0(sdtasdt0(xn, xm), xp))],extension(854 ^ 5)).
% 2.16/2.43 ncf('1.1.2.2',plain,[-(aNaturalNumber0(xp))],extension(806 ^ 3)).
% 2.16/2.43 ncf('1.1.2.3',plain,[-(aNaturalNumber0(sdtasdt0(xn, xm))), aNaturalNumber0(xn), aNaturalNumber0(xm)],extension(148 ^ 3,bind([[_118978, _118980], [xm, xn]]))).
% 2.16/2.43 ncf('1.1.2.3.1',plain,[-(aNaturalNumber0(xn))],extension(802 ^ 4)).
% 2.16/2.43 ncf('1.1.2.3.2',plain,[-(aNaturalNumber0(xm))],extension(804 ^ 4)).
% 2.16/2.43 ncf('1.1.2.4',plain,[xp = sz00, 740 : isPrime0(xp), 740 : aNaturalNumber0(xp)],extension(736 ^ 3,bind([[_136468], [xp]]))).
% 2.16/2.43 ncf('1.1.2.4.1',plain,[-(isPrime0(xp))],extension(838 ^ 6)).
% 2.16/2.43 ncf('1.1.2.4.2',plain,[-(aNaturalNumber0(xp))],lemmata('[1, 1].x')).
% 2.16/2.43 ncf('1.1.2.5',plain,[-(doDivides0(xp, sdtasdt0(xn, xm)))],extension(840 ^ 3)).
% 2.16/2.43 ncf('1.1.3',plain,[xk = sz10],extension(858 ^ 2)).
% 2.16/2.43 %-----------------------------------------------------
% 2.16/2.43 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------