%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM493+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n031.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:46 EDT 2023
% Result : Theorem 168.25s 163.56s
% Output : Proof 168.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : NUM493+3 : TPTP v8.1.2. Released v4.0.0.
% 0.11/0.13 % Command : nanocop.sh %s %d
% 0.14/0.34 % Computer : n031.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 18 17:07:40 EDT 2023
% 0.14/0.34 % CPUTime :
% 168.25/163.56
% 168.25/163.56 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 168.25/163.56 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 168.25/163.56 %-----------------------------------------------------
% 168.25/163.56 ncf(matrix, plain, [(938 ^ _169524) ^ [_169603] : [aNaturalNumber0(_169603), xr = sdtasdt0(xp, _169603)], (946 ^ _169524) ^ [_169848] : [aNaturalNumber0(_169848), xm = sdtasdt0(xp, _169848)], (952 ^ _169524) ^ [] : [doDivides0(xp, xm)], (944 ^ _169524) ^ [] : [doDivides0(xp, xr)], !, (927 ^ _140653) ^ [] : [-(sdtpldt0(xr, 923 ^ []) = xn)], (427 ^ _140653) ^ [_153969, _153971] : [aNaturalNumber0(_153971), aNaturalNumber0(_153969), -(sdtlseqdt0(_153971, _153969)), 438 ^ _140653 : [(439 ^ _140653) ^ [] : [_153969 = _153971], (441 ^ _140653) ^ [] : [-(sdtlseqdt0(_153969, _153971))]]], (533 ^ _140653) ^ [_157193, _157195] : [aNaturalNumber0(_157195), aNaturalNumber0(_157193), iLess0(_157195, _157193), true___, -(true___)], (596 ^ _140653) ^ [_158974, _158976] : [aNaturalNumber0(_158976), aNaturalNumber0(_158974), -(_158976 = sz00), doDivides0(_158976, _158974), 611 ^ _140653 : [(612 ^ _140653) ^ [_159413] : [_159413 = sdtsldt0(_158974, _158976), 615 ^ _140653 : [(616 ^ _140653) ^ [] : [-(aNaturalNumber0(_159413))], (618 ^ _140653) ^ [] : [-(_158974 = sdtasdt0(_158976, _159413))]]], (620 ^ _140653) ^ [_159672] : [-(_159672 = sdtsldt0(_158974, _158976)), aNaturalNumber0(_159672), _158974 = sdtasdt0(_158976, _159672)]]], (351 ^ _140653) ^ [_151764, _151766] : [aNaturalNumber0(_151766), aNaturalNumber0(_151764), sdtlseqdt0(_151766, _151764), 362 ^ _140653 : [(363 ^ _140653) ^ [_152111] : [_152111 = sdtmndt0(_151764, _151766), 366 ^ _140653 : [(367 ^ _140653) ^ [] : [-(aNaturalNumber0(_152111))], (369 ^ _140653) ^ [] : [-(sdtpldt0(_151766, _152111) = _151764)]]], (371 ^ _140653) ^ [_152370] : [-(_152370 = sdtmndt0(_151764, _151766)), aNaturalNumber0(_152370), sdtpldt0(_151766, _152370) = _151764]]], (58 ^ _140653) ^ [_142584, _142586] : [-(aNaturalNumber0(_142584)), _142586 = _142584, aNaturalNumber0(_142586)], (290 ^ _140653) ^ [_149972, _149974] : [aNaturalNumber0(_149974), aNaturalNumber0(_149972), sdtpldt0(_149974, _149972) = sz00, 301 ^ _140653 : [(302 ^ _140653) ^ [] : [-(_149974 = sz00)], (304 ^ _140653) ^ [] : [-(_149972 = sz00)]]], (569 ^ _140653) ^ [_158131, _158133] : [aNaturalNumber0(_158133), aNaturalNumber0(_158131), 576 ^ _140653 : [(577 ^ _140653) ^ [] : [doDivides0(_158133, _158131), 581 ^ _140653 : [(582 ^ _140653) ^ [] : [-(aNaturalNumber0(580 ^ [_158131, _158133]))], (584 ^ _140653) ^ [] : [-(_158131 = sdtasdt0(_158133, 580 ^ [_158131, _158133]))]]], (586 ^ _140653) ^ [] : [-(doDivides0(_158133, _158131)), 587 ^ _140653 : [(588 ^ _140653) ^ [_158691] : [aNaturalNumber0(_158691), _158131 = sdtasdt0(_158133, _158691)]]]]], (900 ^ _140653) ^ [] : [-(isPrime0(xp))], (68 ^ _140653) ^ [_142887, _142889, _142891, _142893] : [-(doDivides0(_142891, _142887)), doDivides0(_142893, _142889), _142893 = _142891, _142889 = _142887], (876 ^ _140653) ^ [] : [xp = sz00], (878 ^ _140653) ^ [] : [xp = sz10], (503 ^ _140653) ^ [_156350] : [aNaturalNumber0(_156350), -(_156350 = sz00), -(_156350 = sz10), 514 ^ _140653 : [(515 ^ _140653) ^ [] : [sz10 = _156350], (517 ^ _140653) ^ [] : [-(sdtlseqdt0(sz10, _156350))]]], (132 ^ _140653) ^ [] : [-(aNaturalNumber0(sz00))], (246 ^ _140653) ^ [_148622, _148624, _148626] : [259 ^ _140653 : [(260 ^ _140653) ^ [] : [sdtpldt0(_148626, _148624) = sdtpldt0(_148626, _148622)], (262 ^ _140653) ^ [] : [sdtpldt0(_148624, _148626) = sdtpldt0(_148622, _148626)]], -(_148624 = _148622), aNaturalNumber0(_148626), aNaturalNumber0(_148624), aNaturalNumber0(_148622)], (230 ^ _140653) ^ [_148075, _148077, _148079] : [241 ^ _140653 : [(242 ^ _140653) ^ [] : [-(sdtasdt0(_148079, sdtpldt0(_148077, _148075)) = sdtpldt0(sdtasdt0(_148079, _148077), sdtasdt0(_148079, _148075)))], (244 ^ _140653) ^ [] : [-(sdtasdt0(sdtpldt0(_148077, _148075), _148079) = sdtpldt0(sdtasdt0(_148077, _148079), sdtasdt0(_148075, _148079)))]], aNaturalNumber0(_148079), aNaturalNumber0(_148077), aNaturalNumber0(_148075)], (112 ^ _140653) ^ [_144402, _144404, _144406, _144408] : [-(sdtasdt0(_144408, _144404) = sdtasdt0(_144406, _144402)), _144408 = _144406, _144404 = _144402], (443 ^ _140653) ^ [_154432, _154434] : [aNaturalNumber0(_154434), aNaturalNumber0(_154432), -(_154434 = _154432), sdtlseqdt0(_154434, _154432), 458 ^ _140653 : [(459 ^ _140653) ^ [_154876] : [aNaturalNumber0(_154876), 462 ^ _140653 : [(463 ^ _140653) ^ [] : [sdtpldt0(_154876, _154434) = sdtpldt0(_154876, _154432)], (469 ^ _140653) ^ [] : [-(sdtlseqdt0(sdtpldt0(_154434, _154876), sdtpldt0(_154432, _154876)))], (467 ^ _140653) ^ [] : [sdtpldt0(_154434, _154876) = sdtpldt0(_154432, _154876)], (465 ^ _140653) ^ [] : [-(sdtlseqdt0(sdtpldt0(_154876, _154434), sdtpldt0(_154876, _154432)))]]]]], (806 ^ _140653) ^ [] : [-(aNaturalNumber0(xp))], (804 ^ _140653) ^ [] : [-(aNaturalNumber0(xm))], (920 ^ _140653) ^ [] : [-(xr = sdtmndt0(xn, xp))], (551 ^ _140653) ^ [_157653, _157655] : [aNaturalNumber0(_157655), aNaturalNumber0(_157653), -(iLess0(_157655, _157653)), -(_157655 = _157653), sdtlseqdt0(_157655, _157653)], (158 ^ _140653) ^ [_145760, _145762] : [-(sdtpldt0(_145762, _145760) = sdtpldt0(_145760, _145762)), aNaturalNumber0(_145762), aNaturalNumber0(_145760)], (925 ^ _140653) ^ [] : [-(aNaturalNumber0(923 ^ []))], (182 ^ _140653) ^ [_146487] : [aNaturalNumber0(_146487), 185 ^ _140653 : [(186 ^ _140653) ^ [] : [-(sdtpldt0(_146487, sz00) = _146487)], (188 ^ _140653) ^ [] : [-(_146487 = sdtpldt0(sz00, _146487))]]], (905 ^ _140653) ^ [] : [-(sdtasdt0(xn, xm) = sdtasdt0(xp, 901 ^ []))], (134 ^ _140653) ^ [] : [-(aNaturalNumber0(sz10))], (102 ^ _140653) ^ [_144063, _144065, _144067, _144069] : [-(sdtpldt0(_144069, _144065) = sdtpldt0(_144067, _144063)), _144069 = _144067, _144065 = _144063], (630 ^ _140653) ^ [_160024, _160026, _160028] : [aNaturalNumber0(_160028), aNaturalNumber0(_160026), aNaturalNumber0(_160024), -(doDivides0(_160028, _160024)), doDivides0(_160028, _160026), doDivides0(_160026, _160024)], (136 ^ _140653) ^ [] : [sz10 = sz00], (714 ^ _140653) ^ [_162300, _162302] : [aNaturalNumber0(_162302), aNaturalNumber0(_162300), -(_162302 = sz00), doDivides0(_162302, _162300), 729 ^ _140653 : [(730 ^ _140653) ^ [_162710] : [aNaturalNumber0(_162710), -(sdtasdt0(_162710, sdtsldt0(_162300, _162302)) = sdtsldt0(sdtasdt0(_162710, _162300), _162302))]]], (802 ^ _140653) ^ [] : [-(aNaturalNumber0(xn))], (880 ^ _140653) ^ [_167573] : [-(_167573 = sz10), -(_167573 = xp), aNaturalNumber0(_167573), 885 ^ _140653 : [(892 ^ _140653) ^ [] : [doDivides0(_167573, xp)], (886 ^ _140653) ^ [_167776] : [aNaturalNumber0(_167776), xp = sdtasdt0(_167573, _167776)]]], (907 ^ _140653) ^ [] : [-(doDivides0(xp, sdtasdt0(xn, xm)))], (932 ^ _140653) ^ [] : [-(aNaturalNumber0(930 ^ []))], (914 ^ _140653) ^ [] : [-(sdtlseqdt0(xp, xn))], (381 ^ _140653) ^ [_152692] : [aNaturalNumber0(_152692), -(sdtlseqdt0(_152692, _152692))], (922 ^ _140653) ^ [] : [xr = xn], (2 ^ _140653) ^ [_140777] : [-(_140777 = _140777)], (916 ^ _140653) ^ [] : [-(aNaturalNumber0(xr))], (222 ^ _140653) ^ [_147774] : [aNaturalNumber0(_147774), 225 ^ _140653 : [(226 ^ _140653) ^ [] : [-(sdtasdt0(_147774, sz00) = sz00)], (228 ^ _140653) ^ [] : [-(sz00 = sdtasdt0(sz00, _147774))]]], (934 ^ _140653) ^ [] : [-(sdtasdt0(xr, xm) = sdtasdt0(xp, 930 ^ []))], (910 ^ _140653) ^ [] : [-(aNaturalNumber0(908 ^ []))], (903 ^ _140653) ^ [] : [-(aNaturalNumber0(901 ^ []))], (936 ^ _140653) ^ [] : [-(doDivides0(xp, sdtasdt0(xr, xm)))], (34 ^ _140653) ^ [_141845, _141847] : [-(isPrime0(_141845)), _141847 = _141845, isPrime0(_141847)], (696 ^ _140653) ^ [_161822, _161824] : [aNaturalNumber0(_161824), aNaturalNumber0(_161822), -(sdtlseqdt0(_161824, _161822)), doDivides0(_161824, _161822), -(_161822 = sz00)], (912 ^ _140653) ^ [] : [-(sdtpldt0(xp, 908 ^ []) = xn)], (10 ^ _140653) ^ [_141088, _141090, _141092] : [-(_141092 = _141088), _141092 = _141090, _141090 = _141088], (652 ^ _140653) ^ [_160624, _160626, _160628] : [aNaturalNumber0(_160628), aNaturalNumber0(_160626), aNaturalNumber0(_160624), -(doDivides0(_160628, sdtpldt0(_160626, _160624))), doDivides0(_160628, _160626), doDivides0(_160628, _160624)], (44 ^ _140653) ^ [_142168, _142170, _142172, _142174] : [-(sdtlseqdt0(_142172, _142168)), sdtlseqdt0(_142174, _142170), _142174 = _142172, _142170 = _142168], (200 ^ _140653) ^ [_147095, _147097, _147099] : [-(sdtasdt0(sdtasdt0(_147099, _147097), _147095) = sdtasdt0(_147099, sdtasdt0(_147097, _147095))), aNaturalNumber0(_147099), aNaturalNumber0(_147097), aNaturalNumber0(_147095)], (266 ^ _140653) ^ [_149199] : [aNaturalNumber0(_149199), -(_149199 = sz00), 273 ^ _140653 : [(274 ^ _140653) ^ [_149461, _149463] : [aNaturalNumber0(_149463), aNaturalNumber0(_149461), 283 ^ _140653 : [(284 ^ _140653) ^ [] : [sdtasdt0(_149199, _149463) = sdtasdt0(_149199, _149461)], (286 ^ _140653) ^ [] : [sdtasdt0(_149463, _149199) = sdtasdt0(_149461, _149199)]], -(_149463 = _149461)]]], (387 ^ _140653) ^ [_152894, _152896] : [aNaturalNumber0(_152896), aNaturalNumber0(_152894), -(_152896 = _152894), sdtlseqdt0(_152896, _152894), sdtlseqdt0(_152894, _152896)], (4 ^ _140653) ^ [_140884, _140886] : [_140886 = _140884, -(_140884 = _140886)], (148 ^ _140653) ^ [_145461, _145463] : [-(aNaturalNumber0(sdtasdt0(_145463, _145461))), aNaturalNumber0(_145463), aNaturalNumber0(_145461)], (190 ^ _140653) ^ [_146774, _146776] : [-(sdtasdt0(_146776, _146774) = sdtasdt0(_146774, _146776)), aNaturalNumber0(_146776), aNaturalNumber0(_146774)], (306 ^ _140653) ^ [_150439, _150441] : [aNaturalNumber0(_150441), aNaturalNumber0(_150439), sdtasdt0(_150441, _150439) = sz00, -(_150441 = sz00), -(_150439 = sz00)], (929 ^ _140653) ^ [] : [-(sdtlseqdt0(xr, xn))], (214 ^ _140653) ^ [_147501] : [aNaturalNumber0(_147501), 217 ^ _140653 : [(218 ^ _140653) ^ [] : [-(sdtasdt0(_147501, sz10) = _147501)], (220 ^ _140653) ^ [] : [-(_147501 = sdtasdt0(sz10, _147501))]]], (82 ^ _140653) ^ [_143345, _143347, _143349, _143351] : [-(sdtsldt0(_143351, _143347) = sdtsldt0(_143349, _143345)), _143351 = _143349, _143347 = _143345], (20 ^ _140653) ^ [_141429, _141431, _141433, _141435] : [-(iLess0(_141433, _141429)), iLess0(_141435, _141431), _141435 = _141433, _141431 = _141429], (168 ^ _140653) ^ [_146081, _146083, _146085] : [-(sdtpldt0(sdtpldt0(_146085, _146083), _146081) = sdtpldt0(_146085, sdtpldt0(_146083, _146081))), aNaturalNumber0(_146085), aNaturalNumber0(_146083), aNaturalNumber0(_146081)], (405 ^ _140653) ^ [_153383, _153385, _153387] : [aNaturalNumber0(_153387), aNaturalNumber0(_153385), aNaturalNumber0(_153383), -(sdtlseqdt0(_153387, _153383)), sdtlseqdt0(_153387, _153385), sdtlseqdt0(_153385, _153383)], (808 ^ _140653) ^ [_165062, _165064, _165066] : [aNaturalNumber0(_165066), aNaturalNumber0(_165064), aNaturalNumber0(_165062), iLess0(sdtpldt0(sdtpldt0(_165066, _165064), _165062), sdtpldt0(sdtpldt0(xn, xm), xp)), 862 ^ _140653 : [(867 ^ _140653) ^ [] : [-(doDivides0(_165062, _165066))], (865 ^ _140653) ^ [] : [-(_165066 = sdtasdt0(_165062, 861 ^ [_165062, _165064, _165066]))], (863 ^ _140653) ^ [] : [-(aNaturalNumber0(861 ^ [_165062, _165064, _165066]))]], 869 ^ _140653 : [(874 ^ _140653) ^ [] : [-(doDivides0(_165062, _165064))], (872 ^ _140653) ^ [] : [-(_165064 = sdtasdt0(_165062, 868 ^ [_165062, _165064, _165066]))], (870 ^ _140653) ^ [] : [-(aNaturalNumber0(868 ^ [_165062, _165064, _165066]))]], 847 ^ _140653 : [(854 ^ _140653) ^ [] : [doDivides0(_165062, sdtasdt0(_165066, _165064))], (848 ^ _140653) ^ [_166483] : [aNaturalNumber0(_166483), sdtasdt0(_165066, _165064) = sdtasdt0(_165062, _166483)]], 823 ^ _140653 : [(846 ^ _140653) ^ [] : [isPrime0(_165062)], (824 ^ _140653) ^ [] : [-(_165062 = sz00), -(_165062 = sz10), 832 ^ _140653 : [(838 ^ _140653) ^ [] : [-(_165062 = sdtasdt0(831 ^ [_165062, _165064, _165066], 834 ^ [_165062, _165064, _165066]))], (833 ^ _140653) ^ [] : [-(aNaturalNumber0(831 ^ [_165062, _165064, _165066]))], (844 ^ _140653) ^ [] : [831 ^ [_165062, _165064, _165066] = _165062], (840 ^ _140653) ^ [] : [-(doDivides0(831 ^ [_165062, _165064, _165066], _165062))], (842 ^ _140653) ^ [] : [831 ^ [_165062, _165064, _165066] = sz10], (836 ^ _140653) ^ [] : [-(aNaturalNumber0(834 ^ [_165062, _165064, _165066]))]]]]], (122 ^ _140653) ^ [_144733] : [aNaturalNumber0(_144733), true___, -(true___)], (324 ^ _140653) ^ [_150921, _150923] : [aNaturalNumber0(_150923), aNaturalNumber0(_150921), 331 ^ _140653 : [(332 ^ _140653) ^ [] : [sdtlseqdt0(_150923, _150921), 336 ^ _140653 : [(337 ^ _140653) ^ [] : [-(aNaturalNumber0(335 ^ [_150921, _150923]))], (339 ^ _140653) ^ [] : [-(sdtpldt0(_150923, 335 ^ [_150921, _150923]) = _150921)]]], (341 ^ _140653) ^ [] : [-(sdtlseqdt0(_150923, _150921)), 342 ^ _140653 : [(343 ^ _140653) ^ [_151481] : [aNaturalNumber0(_151481), sdtpldt0(_150923, _151481) = _150921]]]]], (783 ^ _140653) ^ [_164295] : [795 ^ _140653 : [(800 ^ _140653) ^ [] : [-(isPrime0(794 ^ [_164295]))], (798 ^ _140653) ^ [] : [-(doDivides0(794 ^ [_164295], _164295))], (796 ^ _140653) ^ [] : [-(aNaturalNumber0(794 ^ [_164295]))]], aNaturalNumber0(_164295), -(_164295 = sz00), -(_164295 = sz10)], (92 ^ _140653) ^ [_143704, _143706, _143708, _143710] : [-(sdtmndt0(_143710, _143706) = sdtmndt0(_143708, _143704)), _143710 = _143708, _143706 = _143704], (471 ^ _140653) ^ [_155400, _155402, _155404] : [aNaturalNumber0(_155404), aNaturalNumber0(_155402), aNaturalNumber0(_155400), 494 ^ _140653 : [(495 ^ _140653) ^ [] : [sdtasdt0(_155404, _155402) = sdtasdt0(_155404, _155400)], (501 ^ _140653) ^ [] : [-(sdtlseqdt0(sdtasdt0(_155402, _155404), sdtasdt0(_155400, _155404)))], (499 ^ _140653) ^ [] : [sdtasdt0(_155402, _155404) = sdtasdt0(_155400, _155404)], (497 ^ _140653) ^ [] : [-(sdtlseqdt0(sdtasdt0(_155404, _155402), sdtasdt0(_155404, _155400)))]], -(_155404 = sz00), -(_155402 = _155400), sdtlseqdt0(_155402, _155400)], (674 ^ _140653) ^ [_161230, _161232, _161234] : [aNaturalNumber0(_161234), aNaturalNumber0(_161232), aNaturalNumber0(_161230), -(doDivides0(_161234, _161230)), doDivides0(_161234, _161232), doDivides0(_161234, sdtpldt0(_161232, _161230))], (736 ^ _140653) ^ [_162951] : [aNaturalNumber0(_162951), 739 ^ _140653 : [(762 ^ _140653) ^ [] : [-(isPrime0(_162951)), -(_162951 = sz00), -(_162951 = sz10), 772 ^ _140653 : [(773 ^ _140653) ^ [] : [-(aNaturalNumber0(771 ^ [_162951]))], (779 ^ _140653) ^ [] : [771 ^ [_162951] = _162951], (777 ^ _140653) ^ [] : [771 ^ [_162951] = sz10], (775 ^ _140653) ^ [] : [-(doDivides0(771 ^ [_162951], _162951))]]], (740 ^ _140653) ^ [] : [isPrime0(_162951), 743 ^ _140653 : [(748 ^ _140653) ^ [_163343] : [aNaturalNumber0(_163343), doDivides0(_163343, _162951), -(_163343 = sz10), -(_163343 = _162951)], (746 ^ _140653) ^ [] : [_162951 = sz10], (744 ^ _140653) ^ [] : [_162951 = sz00]]]]], (918 ^ _140653) ^ [] : [-(sdtpldt0(xp, xr) = xn)], (519 ^ _140653) ^ [_156798, _156800] : [aNaturalNumber0(_156800), aNaturalNumber0(_156798), -(_156800 = sz00), -(sdtlseqdt0(_156798, sdtasdt0(_156798, _156800)))], (138 ^ _140653) ^ [_145162, _145164] : [-(aNaturalNumber0(sdtpldt0(_145164, _145162))), aNaturalNumber0(_145164), aNaturalNumber0(_145162)]], input).
% 168.25/163.56 ncf('1',plain,[doDivides0(xp, xm)],start(952 ^ 0)).
% 168.25/163.56 ncf('1.1',plain,[-(doDivides0(xp, xm)), aNaturalNumber0(xr), aNaturalNumber0(xm), aNaturalNumber0(xp), iLess0(sdtpldt0(sdtpldt0(xr, xm), xp), sdtpldt0(sdtpldt0(xn, xm), xp)), 867 : -(doDivides0(xp, xr)), 854 : doDivides0(xp, sdtasdt0(xr, xm)), 846 : isPrime0(xp)],extension(808 ^ 1,bind([[_165062, _165064, _165066], [xp, xm, xr]]))).
% 168.25/163.56 ncf('1.1.1',plain,[-(aNaturalNumber0(xr)), 363 : xr = sdtmndt0(xn, xp), 363 : aNaturalNumber0(xp), 363 : aNaturalNumber0(xn), 363 : sdtlseqdt0(xp, xn)],extension(351 ^ 2,bind([[_151764, _151766, _152111], [xn, xp, xr]]))).
% 168.25/163.56 ncf('1.1.1.1',plain,[-(xr = sdtmndt0(xn, xp))],extension(920 ^ 5)).
% 168.25/163.56 ncf('1.1.1.2',plain,[-(aNaturalNumber0(xp))],extension(806 ^ 3)).
% 168.25/163.56 ncf('1.1.1.3',plain,[-(aNaturalNumber0(xn))],extension(802 ^ 3)).
% 168.25/163.56 ncf('1.1.1.4',plain,[-(sdtlseqdt0(xp, xn))],extension(914 ^ 3)).
% 168.25/163.56 ncf('1.1.2',plain,[-(aNaturalNumber0(xm))],extension(804 ^ 2)).
% 168.25/163.56 ncf('1.1.3',plain,[-(aNaturalNumber0(xp))],extension(806 ^ 2)).
% 168.25/163.56 ncf('1.1.4',plain,[-(iLess0(sdtpldt0(sdtpldt0(xr, xm), xp), sdtpldt0(sdtpldt0(xn, xm), xp))), aNaturalNumber0(sdtpldt0(sdtpldt0(xr, xm), xp)), aNaturalNumber0(sdtpldt0(sdtpldt0(xn, xm), xp)), -(sdtpldt0(sdtpldt0(xr, xm), xp) = sdtpldt0(sdtpldt0(xn, xm), xp)), sdtlseqdt0(sdtpldt0(sdtpldt0(xr, xm), xp), sdtpldt0(sdtpldt0(xn, xm), xp))],extension(551 ^ 2,bind([[_157653, _157655], [sdtpldt0(sdtpldt0(xn, xm), xp), sdtpldt0(sdtpldt0(xr, xm), xp)]]))).
% 168.25/163.56 ncf('1.1.4.1',plain,[-(aNaturalNumber0(sdtpldt0(sdtpldt0(xr, xm), xp))), aNaturalNumber0(sdtpldt0(xr, xm)), aNaturalNumber0(xp)],extension(138 ^ 3,bind([[_145162, _145164], [xp, sdtpldt0(xr, xm)]]))).
% 168.25/163.56 ncf('1.1.4.1.1',plain,[-(aNaturalNumber0(sdtpldt0(xr, xm))), aNaturalNumber0(xr), aNaturalNumber0(xm)],extension(138 ^ 4,bind([[_145162, _145164], [xm, xr]]))).
% 168.25/163.56 ncf('1.1.4.1.1.1',plain,[-(aNaturalNumber0(xr))],lemmata('[1].x')).
% 168.25/163.56 ncf('1.1.4.1.1.2',plain,[-(aNaturalNumber0(xm))],lemmata('[1].x')).
% 168.25/163.56 ncf('1.1.4.1.2',plain,[-(aNaturalNumber0(xp))],lemmata('[1].x')).
% 168.25/163.56 ncf('1.1.4.2',plain,[-(aNaturalNumber0(sdtpldt0(sdtpldt0(xn, xm), xp))), aNaturalNumber0(sdtpldt0(xn, xm)), aNaturalNumber0(xp)],extension(138 ^ 3,bind([[_145162, _145164], [xp, sdtpldt0(xn, xm)]]))).
% 168.25/163.56 ncf('1.1.4.2.1',plain,[-(aNaturalNumber0(sdtpldt0(xn, xm))), aNaturalNumber0(xn), aNaturalNumber0(xm)],extension(138 ^ 4,bind([[_145162, _145164], [xm, xn]]))).
% 168.25/163.56 ncf('1.1.4.2.1.1',plain,[-(aNaturalNumber0(xn))],extension(802 ^ 5)).
% 168.25/163.56 ncf('1.1.4.2.1.2',plain,[-(aNaturalNumber0(xm))],lemmata('[1].x')).
% 168.25/163.56 ncf('1.1.4.2.2',plain,[-(aNaturalNumber0(xp))],lemmata('[1].x')).
% 168.25/163.56 ncf('1.1.4.3',plain,[sdtpldt0(sdtpldt0(xr, xm), xp) = sdtpldt0(sdtpldt0(xn, xm), xp), -(sdtpldt0(xr, xm) = sdtpldt0(xn, xm)), aNaturalNumber0(xp), aNaturalNumber0(sdtpldt0(xr, xm)), aNaturalNumber0(sdtpldt0(xn, xm))],extension(246 ^ 3,bind([[_148622, _148624, _148626], [sdtpldt0(xn, xm), sdtpldt0(xr, xm), xp]]))).
% 168.25/163.56 ncf('1.1.4.3.1',plain,[sdtpldt0(xr, xm) = sdtpldt0(xn, xm), -(xr = xn), aNaturalNumber0(xm), aNaturalNumber0(xr), aNaturalNumber0(xn)],extension(246 ^ 4,bind([[_148622, _148624, _148626], [xn, xr, xm]]))).
% 168.25/163.56 ncf('1.1.4.3.1.1',plain,[xr = xn],extension(922 ^ 5)).
% 168.25/163.56 ncf('1.1.4.3.1.2',plain,[-(aNaturalNumber0(xm))],lemmata('[1].x')).
% 168.25/163.56 ncf('1.1.4.3.1.3',plain,[-(aNaturalNumber0(xr))],lemmata('[1].x')).
% 168.25/163.56 ncf('1.1.4.3.1.4',plain,[-(aNaturalNumber0(xn))],extension(802 ^ 5)).
% 168.25/163.56 ncf('1.1.4.3.2',plain,[-(aNaturalNumber0(xp))],lemmata('[1].x')).
% 168.25/163.56 ncf('1.1.4.3.3',plain,[-(aNaturalNumber0(sdtpldt0(xr, xm))), aNaturalNumber0(xr), aNaturalNumber0(xm)],extension(138 ^ 4,bind([[_145162, _145164], [xm, xr]]))).
% 168.25/163.56 ncf('1.1.4.3.3.1',plain,[-(aNaturalNumber0(xr))],lemmata('[1].x')).
% 168.25/163.56 ncf('1.1.4.3.3.2',plain,[-(aNaturalNumber0(xm))],lemmata('[1].x')).
% 168.25/163.56 ncf('1.1.4.3.4',plain,[-(aNaturalNumber0(sdtpldt0(xn, xm))), aNaturalNumber0(xn), aNaturalNumber0(xm)],extension(138 ^ 4,bind([[_145162, _145164], [xm, xn]]))).
% 168.25/163.56 ncf('1.1.4.3.4.1',plain,[-(aNaturalNumber0(xn))],extension(802 ^ 5)).
% 168.25/163.56 ncf('1.1.4.3.4.2',plain,[-(aNaturalNumber0(xm))],lemmata('[1].x')).
% 168.25/163.56 ncf('1.1.4.4',plain,[-(sdtlseqdt0(sdtpldt0(sdtpldt0(xr, xm), xp), sdtpldt0(sdtpldt0(xn, xm), xp))), 459 : aNaturalNumber0(xp), 459 : aNaturalNumber0(sdtpldt0(xr, xm)), 459 : aNaturalNumber0(sdtpldt0(xn, xm)), 459 : -(sdtpldt0(xr, xm) = sdtpldt0(xn, xm)), 459 : sdtlseqdt0(sdtpldt0(xr, xm), sdtpldt0(xn, xm))],extension(443 ^ 3,bind([[_154432, _154434, _154876], [sdtpldt0(xn, xm), sdtpldt0(xr, xm), xp]]))).
% 168.25/163.56 ncf('1.1.4.4.1',plain,[-(aNaturalNumber0(xp))],lemmata('[1].x')).
% 168.25/163.56 ncf('1.1.4.4.2',plain,[-(aNaturalNumber0(sdtpldt0(xr, xm))), aNaturalNumber0(xr), aNaturalNumber0(xm)],extension(138 ^ 4,bind([[_145162, _145164], [xm, xr]]))).
% 168.25/163.56 ncf('1.1.4.4.2.1',plain,[-(aNaturalNumber0(xr))],lemmata('[1].x')).
% 168.25/163.56 ncf('1.1.4.4.2.2',plain,[-(aNaturalNumber0(xm))],lemmata('[1].x')).
% 168.25/163.56 ncf('1.1.4.4.3',plain,[-(aNaturalNumber0(sdtpldt0(xn, xm))), aNaturalNumber0(xn), aNaturalNumber0(xm)],extension(138 ^ 4,bind([[_145162, _145164], [xm, xn]]))).
% 168.25/163.56 ncf('1.1.4.4.3.1',plain,[-(aNaturalNumber0(xn))],extension(802 ^ 5)).
% 168.25/163.56 ncf('1.1.4.4.3.2',plain,[-(aNaturalNumber0(xm))],lemmata('[1].x')).
% 168.25/163.56 ncf('1.1.4.4.4',plain,[sdtpldt0(xr, xm) = sdtpldt0(xn, xm), -(xr = xn), aNaturalNumber0(xm), aNaturalNumber0(xr), aNaturalNumber0(xn)],extension(246 ^ 4,bind([[_148622, _148624, _148626], [xn, xr, xm]]))).
% 168.25/163.56 ncf('1.1.4.4.4.1',plain,[xr = xn],extension(922 ^ 5)).
% 168.25/163.56 ncf('1.1.4.4.4.2',plain,[-(aNaturalNumber0(xm))],lemmata('[1].x')).
% 168.25/163.56 ncf('1.1.4.4.4.3',plain,[-(aNaturalNumber0(xr))],lemmata('[1].x')).
% 168.25/163.56 ncf('1.1.4.4.4.4',plain,[-(aNaturalNumber0(xn))],extension(802 ^ 5)).
% 168.25/163.56 ncf('1.1.4.4.5',plain,[-(sdtlseqdt0(sdtpldt0(xr, xm), sdtpldt0(xn, xm))), 459 : aNaturalNumber0(xm), 459 : aNaturalNumber0(xr), 459 : aNaturalNumber0(xn), 459 : -(xr = xn), 459 : sdtlseqdt0(xr, xn)],extension(443 ^ 4,bind([[_154432, _154434, _154876], [xn, xr, xm]]))).
% 168.25/163.56 ncf('1.1.4.4.5.1',plain,[-(aNaturalNumber0(xm))],lemmata('[1].x')).
% 168.25/163.56 ncf('1.1.4.4.5.2',plain,[-(aNaturalNumber0(xr))],lemmata('[1].x')).
% 168.25/163.56 ncf('1.1.4.4.5.3',plain,[-(aNaturalNumber0(xn))],extension(802 ^ 5)).
% 168.25/163.56 ncf('1.1.4.4.5.4',plain,[xr = xn],extension(922 ^ 5)).
% 168.25/163.56 ncf('1.1.4.4.5.5',plain,[-(sdtlseqdt0(xr, xn))],extension(929 ^ 5)).
% 168.25/163.56 ncf('1.1.5',plain,[doDivides0(xp, xr)],extension(944 ^ 4)).
% 168.25/163.56 ncf('1.1.6',plain,[-(doDivides0(xp, sdtasdt0(xr, xm)))],extension(936 ^ 4)).
% 168.25/163.56 ncf('1.1.7',plain,[-(isPrime0(xp))],extension(900 ^ 4)).
% 168.25/163.56 %-----------------------------------------------------
% 168.25/163.56 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------