%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NUM482+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n024.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:45 EDT 2023
% Result : Theorem 161.85s 156.49s
% Output : Proof 161.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NUM482+3 : TPTP v8.1.2. Released v4.0.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n024.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:34:51 EDT 2023
% 0.12/0.33 % CPUTime :
% 161.85/156.49
% 161.85/156.49 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 161.85/156.49 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 161.85/156.49 %-----------------------------------------------------
% 161.85/156.49 ncf(matrix, plain, [(863 ^ _153553) ^ [_154251] : [aNaturalNumber0(_154251), 868 ^ _153553 : [(875 ^ _153553) ^ [] : [doDivides0(_154251, xk)], (869 ^ _153553) ^ [_154510] : [aNaturalNumber0(_154510), xk = sdtasdt0(_154251, _154510)]], 876 ^ _153553 : [(899 ^ _153553) ^ [] : [isPrime0(_154251)], (877 ^ _153553) ^ [] : [-(_154251 = sz00), -(_154251 = sz10), 885 ^ _153553 : [(891 ^ _153553) ^ [] : [-(_154251 = sdtasdt0(884 ^ [_154251], 887 ^ [_154251]))], (886 ^ _153553) ^ [] : [-(aNaturalNumber0(884 ^ [_154251]))], (897 ^ _153553) ^ [] : [884 ^ [_154251] = _154251], (893 ^ _153553) ^ [] : [-(doDivides0(884 ^ [_154251], _154251))], (895 ^ _153553) ^ [] : [884 ^ [_154251] = sz10], (889 ^ _153553) ^ [] : [-(aNaturalNumber0(887 ^ [_154251]))]]]]], (841 ^ _153553) ^ [_153652] : [-(_153652 = sz10), -(_153652 = xk), aNaturalNumber0(_153652), 846 ^ _153553 : [(853 ^ _153553) ^ [] : [doDivides0(_153652, xk)], (847 ^ _153553) ^ [_153855] : [aNaturalNumber0(_153855), xk = sdtasdt0(_153652, _153855)]]], (861 ^ _153553) ^ [] : [-(isPrime0(xk))], !, (134 ^ _127762) ^ [] : [-(aNaturalNumber0(sz10))], (136 ^ _127762) ^ [] : [sz10 = sz00], (20 ^ _127762) ^ [_128538, _128540, _128542, _128544] : [-(sdtlseqdt0(_128542, _128538)), sdtlseqdt0(_128544, _128540), _128544 = _128542, _128540 = _128538], (266 ^ _127762) ^ [_136308] : [aNaturalNumber0(_136308), -(_136308 = sz00), 273 ^ _127762 : [(274 ^ _127762) ^ [_136570, _136572] : [aNaturalNumber0(_136572), aNaturalNumber0(_136570), 283 ^ _127762 : [(284 ^ _127762) ^ [] : [sdtasdt0(_136308, _136572) = sdtasdt0(_136308, _136570)], (286 ^ _127762) ^ [] : [sdtasdt0(_136572, _136308) = sdtasdt0(_136570, _136308)]], -(_136572 = _136570)]]], (230 ^ _127762) ^ [_135184, _135186, _135188] : [241 ^ _127762 : [(242 ^ _127762) ^ [] : [-(sdtasdt0(_135188, sdtpldt0(_135186, _135184)) = sdtpldt0(sdtasdt0(_135188, _135186), sdtasdt0(_135188, _135184)))], (244 ^ _127762) ^ [] : [-(sdtasdt0(sdtpldt0(_135186, _135184), _135188) = sdtpldt0(sdtasdt0(_135186, _135188), sdtasdt0(_135184, _135188)))]], aNaturalNumber0(_135188), aNaturalNumber0(_135186), aNaturalNumber0(_135184)], (214 ^ _127762) ^ [_134610] : [aNaturalNumber0(_134610), 217 ^ _127762 : [(218 ^ _127762) ^ [] : [-(sdtasdt0(_134610, sz10) = _134610)], (220 ^ _127762) ^ [] : [-(_134610 = sdtasdt0(sz10, _134610))]]], (48 ^ _127762) ^ [_129398, _129400] : [-(aNaturalNumber0(_129398)), _129400 = _129398, aNaturalNumber0(_129400)], (351 ^ _127762) ^ [_138873, _138875] : [aNaturalNumber0(_138875), aNaturalNumber0(_138873), sdtlseqdt0(_138875, _138873), 362 ^ _127762 : [(363 ^ _127762) ^ [_139220] : [_139220 = sdtmndt0(_138873, _138875), 366 ^ _127762 : [(367 ^ _127762) ^ [] : [-(aNaturalNumber0(_139220))], (369 ^ _127762) ^ [] : [-(sdtpldt0(_138875, _139220) = _138873)]]], (371 ^ _127762) ^ [_139479] : [-(_139479 = sdtmndt0(_138873, _138875)), aNaturalNumber0(_139479), sdtpldt0(_138875, _139479) = _138873]]], (443 ^ _127762) ^ [_141541, _141543] : [aNaturalNumber0(_141543), aNaturalNumber0(_141541), -(_141543 = _141541), sdtlseqdt0(_141543, _141541), 458 ^ _127762 : [(459 ^ _127762) ^ [_141985] : [aNaturalNumber0(_141985), 462 ^ _127762 : [(463 ^ _127762) ^ [] : [sdtpldt0(_141985, _141543) = sdtpldt0(_141985, _141541)], (469 ^ _127762) ^ [] : [-(sdtlseqdt0(sdtpldt0(_141543, _141985), sdtpldt0(_141541, _141985)))], (467 ^ _127762) ^ [] : [sdtpldt0(_141543, _141985) = sdtpldt0(_141541, _141985)], (465 ^ _127762) ^ [] : [-(sdtlseqdt0(sdtpldt0(_141985, _141543), sdtpldt0(_141985, _141541)))]]]]], (102 ^ _127762) ^ [_131172, _131174, _131176, _131178] : [-(sdtsldt0(_131178, _131174) = sdtsldt0(_131176, _131172)), _131178 = _131176, _131174 = _131172], (674 ^ _127762) ^ [_148339, _148341, _148343] : [aNaturalNumber0(_148343), aNaturalNumber0(_148341), aNaturalNumber0(_148339), -(doDivides0(_148343, _148339)), doDivides0(_148343, _148341), doDivides0(_148343, sdtpldt0(_148341, _148339))], (519 ^ _127762) ^ [_143907, _143909] : [aNaturalNumber0(_143909), aNaturalNumber0(_143907), -(_143909 = sz00), -(sdtlseqdt0(_143907, sdtasdt0(_143907, _143909)))], (837 ^ _127762) ^ [] : [xk = sz00], (222 ^ _127762) ^ [_134883] : [aNaturalNumber0(_134883), 225 ^ _127762 : [(226 ^ _127762) ^ [] : [-(sdtasdt0(_134883, sz00) = sz00)], (228 ^ _127762) ^ [] : [-(sz00 = sdtasdt0(sz00, _134883))]]], (381 ^ _127762) ^ [_139801] : [aNaturalNumber0(_139801), -(sdtlseqdt0(_139801, _139801))], (630 ^ _127762) ^ [_147133, _147135, _147137] : [aNaturalNumber0(_147137), aNaturalNumber0(_147135), aNaturalNumber0(_147133), -(doDivides0(_147137, _147133)), doDivides0(_147137, _147135), doDivides0(_147135, _147133)], (387 ^ _127762) ^ [_140003, _140005] : [aNaturalNumber0(_140005), aNaturalNumber0(_140003), -(_140005 = _140003), sdtlseqdt0(_140005, _140003), sdtlseqdt0(_140003, _140005)], (427 ^ _127762) ^ [_141078, _141080] : [aNaturalNumber0(_141080), aNaturalNumber0(_141078), -(sdtlseqdt0(_141080, _141078)), 438 ^ _127762 : [(439 ^ _127762) ^ [] : [_141078 = _141080], (441 ^ _127762) ^ [] : [-(sdtlseqdt0(_141078, _141080))]]], (132 ^ _127762) ^ [] : [-(aNaturalNumber0(sz00))], (246 ^ _127762) ^ [_135731, _135733, _135735] : [259 ^ _127762 : [(260 ^ _127762) ^ [] : [sdtpldt0(_135735, _135733) = sdtpldt0(_135735, _135731)], (262 ^ _127762) ^ [] : [sdtpldt0(_135733, _135735) = sdtpldt0(_135731, _135735)]], -(_135733 = _135731), aNaturalNumber0(_135735), aNaturalNumber0(_135733), aNaturalNumber0(_135731)], (10 ^ _127762) ^ [_128197, _128199, _128201] : [-(_128201 = _128197), _128201 = _128199, _128199 = _128197], (596 ^ _127762) ^ [_146083, _146085] : [aNaturalNumber0(_146085), aNaturalNumber0(_146083), -(_146085 = sz00), doDivides0(_146085, _146083), 611 ^ _127762 : [(612 ^ _127762) ^ [_146522] : [_146522 = sdtsldt0(_146083, _146085), 615 ^ _127762 : [(616 ^ _127762) ^ [] : [-(aNaturalNumber0(_146522))], (618 ^ _127762) ^ [] : [-(_146083 = sdtasdt0(_146085, _146522))]]], (620 ^ _127762) ^ [_146781] : [-(_146781 = sdtsldt0(_146083, _146085)), aNaturalNumber0(_146781), _146083 = sdtasdt0(_146085, _146781)]]], (471 ^ _127762) ^ [_142509, _142511, _142513] : [aNaturalNumber0(_142513), aNaturalNumber0(_142511), aNaturalNumber0(_142509), 494 ^ _127762 : [(495 ^ _127762) ^ [] : [sdtasdt0(_142513, _142511) = sdtasdt0(_142513, _142509)], (501 ^ _127762) ^ [] : [-(sdtlseqdt0(sdtasdt0(_142511, _142513), sdtasdt0(_142509, _142513)))], (499 ^ _127762) ^ [] : [sdtasdt0(_142511, _142513) = sdtasdt0(_142509, _142513)], (497 ^ _127762) ^ [] : [-(sdtlseqdt0(sdtasdt0(_142513, _142511), sdtasdt0(_142513, _142509)))]], -(_142513 = sz00), -(_142511 = _142509), sdtlseqdt0(_142511, _142509)], (148 ^ _127762) ^ [_132570, _132572] : [-(aNaturalNumber0(sdtasdt0(_132572, _132570))), aNaturalNumber0(_132572), aNaturalNumber0(_132570)], (4 ^ _127762) ^ [_127993, _127995] : [_127995 = _127993, -(_127993 = _127995)], (783 ^ _127762) ^ [] : [-(aNaturalNumber0(xk))], (652 ^ _127762) ^ [_147733, _147735, _147737] : [aNaturalNumber0(_147737), aNaturalNumber0(_147735), aNaturalNumber0(_147733), -(doDivides0(_147737, sdtpldt0(_147735, _147733))), doDivides0(_147737, _147735), doDivides0(_147737, _147733)], (200 ^ _127762) ^ [_134204, _134206, _134208] : [-(sdtasdt0(sdtasdt0(_134208, _134206), _134204) = sdtasdt0(_134208, sdtasdt0(_134206, _134204))), aNaturalNumber0(_134208), aNaturalNumber0(_134206), aNaturalNumber0(_134204)], (405 ^ _127762) ^ [_140492, _140494, _140496] : [aNaturalNumber0(_140496), aNaturalNumber0(_140494), aNaturalNumber0(_140492), -(sdtlseqdt0(_140496, _140492)), sdtlseqdt0(_140496, _140494), sdtlseqdt0(_140494, _140492)], (190 ^ _127762) ^ [_133883, _133885] : [-(sdtasdt0(_133885, _133883) = sdtasdt0(_133883, _133885)), aNaturalNumber0(_133885), aNaturalNumber0(_133883)], (569 ^ _127762) ^ [_145240, _145242] : [aNaturalNumber0(_145242), aNaturalNumber0(_145240), 576 ^ _127762 : [(577 ^ _127762) ^ [] : [doDivides0(_145242, _145240), 581 ^ _127762 : [(582 ^ _127762) ^ [] : [-(aNaturalNumber0(580 ^ [_145240, _145242]))], (584 ^ _127762) ^ [] : [-(_145240 = sdtasdt0(_145242, 580 ^ [_145240, _145242]))]]], (586 ^ _127762) ^ [] : [-(doDivides0(_145242, _145240)), 587 ^ _127762 : [(588 ^ _127762) ^ [_145800] : [aNaturalNumber0(_145800), _145240 = sdtasdt0(_145242, _145800)]]]]], (736 ^ _127762) ^ [_150060] : [aNaturalNumber0(_150060), 739 ^ _127762 : [(762 ^ _127762) ^ [] : [-(isPrime0(_150060)), -(_150060 = sz00), -(_150060 = sz10), 772 ^ _127762 : [(773 ^ _127762) ^ [] : [-(aNaturalNumber0(771 ^ [_150060]))], (779 ^ _127762) ^ [] : [771 ^ [_150060] = _150060], (777 ^ _127762) ^ [] : [771 ^ [_150060] = sz10], (775 ^ _127762) ^ [] : [-(doDivides0(771 ^ [_150060], _150060))]]], (740 ^ _127762) ^ [] : [isPrime0(_150060), 743 ^ _127762 : [(748 ^ _127762) ^ [_150452] : [aNaturalNumber0(_150452), doDivides0(_150452, _150060), -(_150452 = sz10), -(_150452 = _150060)], (746 ^ _127762) ^ [] : [_150060 = sz10], (744 ^ _127762) ^ [] : [_150060 = sz00]]]]], (122 ^ _127762) ^ [_131842] : [aNaturalNumber0(_131842), true___, -(true___)], (58 ^ _127762) ^ [_129721, _129723, _129725, _129727] : [-(doDivides0(_129725, _129721)), doDivides0(_129727, _129723), _129727 = _129725, _129723 = _129721], (306 ^ _127762) ^ [_137548, _137550] : [aNaturalNumber0(_137550), aNaturalNumber0(_137548), sdtasdt0(_137550, _137548) = sz00, -(_137550 = sz00), -(_137548 = sz00)], (72 ^ _127762) ^ [_130117, _130119] : [-(isPrime0(_130117)), _130119 = _130117, isPrime0(_130119)], (82 ^ _127762) ^ [_130454, _130456, _130458, _130460] : [-(sdtmndt0(_130460, _130456) = sdtmndt0(_130458, _130454)), _130460 = _130458, _130456 = _130454], (696 ^ _127762) ^ [_148931, _148933] : [aNaturalNumber0(_148933), aNaturalNumber0(_148931), -(sdtlseqdt0(_148933, _148931)), doDivides0(_148933, _148931), -(_148931 = sz00)], (290 ^ _127762) ^ [_137081, _137083] : [aNaturalNumber0(_137083), aNaturalNumber0(_137081), sdtpldt0(_137083, _137081) = sz00, 301 ^ _127762 : [(302 ^ _127762) ^ [] : [-(_137083 = sz00)], (304 ^ _127762) ^ [] : [-(_137081 = sz00)]]], (92 ^ _127762) ^ [_130813, _130815, _130817, _130819] : [-(sdtpldt0(_130819, _130815) = sdtpldt0(_130817, _130813)), _130819 = _130817, _130815 = _130813], (138 ^ _127762) ^ [_132271, _132273] : [-(aNaturalNumber0(sdtpldt0(_132273, _132271))), aNaturalNumber0(_132273), aNaturalNumber0(_132271)], (112 ^ _127762) ^ [_131511, _131513, _131515, _131517] : [-(sdtasdt0(_131517, _131513) = sdtasdt0(_131515, _131511)), _131517 = _131515, _131513 = _131511], (785 ^ _127762) ^ [_151457] : [aNaturalNumber0(_151457), -(_151457 = sz00), -(_151457 = sz10), iLess0(_151457, xk), 801 ^ _127762 : [(805 ^ _127762) ^ [] : [-(aNaturalNumber0(803 ^ [_151457]))], (835 ^ _127762) ^ [] : [-(isPrime0(800 ^ [_151457]))], (802 ^ _127762) ^ [] : [-(aNaturalNumber0(800 ^ [_151457]))], (815 ^ _127762) ^ [_152558] : [-(_152558 = sz10), -(_152558 = 800 ^ [_151457]), aNaturalNumber0(_152558), 820 ^ _127762 : [(827 ^ _127762) ^ [] : [doDivides0(_152558, 800 ^ [_151457])], (821 ^ _127762) ^ [_152784] : [aNaturalNumber0(_152784), 800 ^ [_151457] = sdtasdt0(_152558, _152784)]]], (809 ^ _127762) ^ [] : [-(doDivides0(800 ^ [_151457], _151457))], (813 ^ _127762) ^ [] : [800 ^ [_151457] = sz10], (811 ^ _127762) ^ [] : [800 ^ [_151457] = sz00], (807 ^ _127762) ^ [] : [-(_151457 = sdtasdt0(800 ^ [_151457], 803 ^ [_151457]))]]], (2 ^ _127762) ^ [_127886] : [-(_127886 = _127886)], (551 ^ _127762) ^ [_144762, _144764] : [aNaturalNumber0(_144764), aNaturalNumber0(_144762), -(iLess0(_144764, _144762)), -(_144764 = _144762), sdtlseqdt0(_144764, _144762)], (714 ^ _127762) ^ [_149409, _149411] : [aNaturalNumber0(_149411), aNaturalNumber0(_149409), -(_149411 = sz00), doDivides0(_149411, _149409), 729 ^ _127762 : [(730 ^ _127762) ^ [_149819] : [aNaturalNumber0(_149819), -(sdtasdt0(_149819, sdtsldt0(_149409, _149411)) = sdtsldt0(sdtasdt0(_149819, _149409), _149411))]]], (34 ^ _127762) ^ [_128982, _128984, _128986, _128988] : [-(iLess0(_128986, _128982)), iLess0(_128988, _128984), _128988 = _128986, _128984 = _128982], (533 ^ _127762) ^ [_144302, _144304] : [aNaturalNumber0(_144304), aNaturalNumber0(_144302), iLess0(_144304, _144302), true___, -(true___)], (182 ^ _127762) ^ [_133596] : [aNaturalNumber0(_133596), 185 ^ _127762 : [(186 ^ _127762) ^ [] : [-(sdtpldt0(_133596, sz00) = _133596)], (188 ^ _127762) ^ [] : [-(_133596 = sdtpldt0(sz00, _133596))]]], (324 ^ _127762) ^ [_138030, _138032] : [aNaturalNumber0(_138032), aNaturalNumber0(_138030), 331 ^ _127762 : [(332 ^ _127762) ^ [] : [sdtlseqdt0(_138032, _138030), 336 ^ _127762 : [(337 ^ _127762) ^ [] : [-(aNaturalNumber0(335 ^ [_138030, _138032]))], (339 ^ _127762) ^ [] : [-(sdtpldt0(_138032, 335 ^ [_138030, _138032]) = _138030)]]], (341 ^ _127762) ^ [] : [-(sdtlseqdt0(_138032, _138030)), 342 ^ _127762 : [(343 ^ _127762) ^ [_138590] : [aNaturalNumber0(_138590), sdtpldt0(_138032, _138590) = _138030]]]]], (503 ^ _127762) ^ [_143459] : [aNaturalNumber0(_143459), -(_143459 = sz00), -(_143459 = sz10), 514 ^ _127762 : [(515 ^ _127762) ^ [] : [sz10 = _143459], (517 ^ _127762) ^ [] : [-(sdtlseqdt0(sz10, _143459))]]], (839 ^ _127762) ^ [] : [xk = sz10], (158 ^ _127762) ^ [_132869, _132871] : [-(sdtpldt0(_132871, _132869) = sdtpldt0(_132869, _132871)), aNaturalNumber0(_132871), aNaturalNumber0(_132869)], (168 ^ _127762) ^ [_133190, _133192, _133194] : [-(sdtpldt0(sdtpldt0(_133194, _133192), _133190) = sdtpldt0(_133194, sdtpldt0(_133192, _133190))), aNaturalNumber0(_133194), aNaturalNumber0(_133192), aNaturalNumber0(_133190)]], input).
% 161.85/156.49 ncf('1',plain,[-(xk = sz10), -(xk = xk), aNaturalNumber0(xk), 853 : doDivides0(xk, xk)],start(841 ^ 0,bind([[_153652], [xk]]))).
% 161.85/156.49 ncf('1.1',plain,[xk = sz10, -(sdtlseqdt0(sz10, sz10)), sdtlseqdt0(xk, sz10), sz10 = sz10],extension(20 ^ 1,bind([[_128538, _128540, _128542, _128544], [sz10, sz10, sz10, xk]]))).
% 161.85/156.49 ncf('1.1.1',plain,[sdtlseqdt0(sz10, sz10), aNaturalNumber0(sz10), aNaturalNumber0(sz10), -(sz10 = sz10), 459 : aNaturalNumber0(sz10), 463 : sdtpldt0(sz10, sz10) = sdtpldt0(sz10, sz10)],extension(443 ^ 2,bind([[_141541, _141543, _141985], [sz10, sz10, sz10]]))).
% 161.85/156.49 ncf('1.1.1.1',plain,[-(aNaturalNumber0(sz10))],extension(134 ^ 3)).
% 161.85/156.49 ncf('1.1.1.2',plain,[-(aNaturalNumber0(sz10))],extension(134 ^ 3)).
% 161.85/156.49 ncf('1.1.1.3',plain,[sz10 = sz10, -(xk = sz10), xk = sz10],extension(10 ^ 3,bind([[_128197, _128199, _128201], [sz10, sz10, xk]]))).
% 161.85/156.49 ncf('1.1.1.3.1',plain,[xk = sz10],extension(839 ^ 4)).
% 161.85/156.49 ncf('1.1.1.3.2',plain,[-(xk = sz10)],reduction('1')).
% 161.85/156.49 ncf('1.1.1.4',plain,[-(aNaturalNumber0(sz10))],extension(134 ^ 5)).
% 161.85/156.49 ncf('1.1.1.5',plain,[-(sdtpldt0(sz10, sz10) = sdtpldt0(sz10, sz10))],extension(2 ^ 7,bind([[_127886], [sdtpldt0(sz10, sz10)]]))).
% 161.85/156.49 ncf('1.1.2',plain,[-(sdtlseqdt0(xk, sz10)), sdtlseqdt0(sz10, sdtasdt0(sz10, sz10)), sz10 = xk, sdtasdt0(sz10, sz10) = sz10],extension(20 ^ 2,bind([[_128538, _128540, _128542, _128544], [sz10, sdtasdt0(sz10, sz10), xk, sz10]]))).
% 161.85/156.49 ncf('1.1.2.1',plain,[-(sdtlseqdt0(sz10, sdtasdt0(sz10, sz10))), aNaturalNumber0(sz10), aNaturalNumber0(sz10), -(sz10 = sz00)],extension(519 ^ 3,bind([[_143907, _143909], [sz10, sz10]]))).
% 161.85/156.49 ncf('1.1.2.1.1',plain,[-(aNaturalNumber0(sz10))],extension(134 ^ 4)).
% 161.85/156.49 ncf('1.1.2.1.2',plain,[-(aNaturalNumber0(sz10))],extension(134 ^ 4)).
% 161.85/156.49 ncf('1.1.2.1.3',plain,[sz10 = sz00],extension(136 ^ 4)).
% 161.85/156.49 ncf('1.1.2.2',plain,[-(sz10 = xk), xk = sz10],extension(4 ^ 3,bind([[_127993, _127995], [sz10, xk]]))).
% 161.85/156.49 ncf('1.1.2.2.1',plain,[-(xk = sz10)],reduction('1')).
% 161.85/156.49 ncf('1.1.2.3',plain,[-(sdtasdt0(sz10, sz10) = sz10), aNaturalNumber0(sz10)],extension(214 ^ 3,bind([[_134610], [sz10]]))).
% 161.85/156.49 ncf('1.1.2.3.1',plain,[-(aNaturalNumber0(sz10))],extension(134 ^ 4)).
% 161.85/156.49 ncf('1.1.3',plain,[-(sz10 = sz10), 274 : aNaturalNumber0(sz10), 274 : aNaturalNumber0(sz10), 284 : sdtasdt0(sz10, sz10) = sdtasdt0(sz10, sz10), 274 : aNaturalNumber0(sz10), 274 : -(sz10 = sz00)],extension(266 ^ 2,bind([[_136308, _136570, _136572], [sz10, sz10, sz10]]))).
% 161.85/156.49 ncf('1.1.3.1',plain,[-(aNaturalNumber0(sz10))],extension(134 ^ 5)).
% 161.85/156.49 ncf('1.1.3.2',plain,[-(aNaturalNumber0(sz10))],lemmata('[1, 1].x')).
% 161.85/156.49 ncf('1.1.3.3',plain,[-(sdtasdt0(sz10, sz10) = sdtasdt0(sz10, sz10)), aNaturalNumber0(sz10), aNaturalNumber0(sz10)],extension(190 ^ 7,bind([[_133883, _133885], [sz10, sz10]]))).
% 161.85/156.49 ncf('1.1.3.3.1',plain,[-(aNaturalNumber0(sz10))],lemmata('[1, 1].x')).
% 161.85/156.49 ncf('1.1.3.3.2',plain,[-(aNaturalNumber0(sz10))],lemmata('[3, 1, 1].x')).
% 161.85/156.49 ncf('1.1.3.4',plain,[-(aNaturalNumber0(sz10))],extension(134 ^ 3)).
% 161.85/156.49 ncf('1.1.3.5',plain,[sz10 = sz00],extension(136 ^ 3)).
% 161.85/156.49 ncf('1.2',plain,[xk = xk, -(doDivides0(xk, xk)), doDivides0(xk, sdtasdt0(sz10, xk)), sdtasdt0(sz10, xk) = xk],extension(58 ^ 1,bind([[_129721, _129723, _129725, _129727], [xk, sdtasdt0(sz10, xk), xk, xk]]))).
% 161.85/156.49 ncf('1.2.1',plain,[doDivides0(xk, xk), aNaturalNumber0(xk), 899 : isPrime0(xk)],extension(863 ^ 2,bind([[_154251], [xk]]))).
% 161.85/156.49 ncf('1.2.1.1',plain,[-(aNaturalNumber0(xk))],extension(783 ^ 3)).
% 161.85/156.49 ncf('1.2.1.2',plain,[-(isPrime0(xk))],extension(861 ^ 5)).
% 161.85/156.49 ncf('1.2.2',plain,[-(doDivides0(xk, sdtasdt0(sz10, xk))), 588 : aNaturalNumber0(sz10), 588 : sdtasdt0(sz10, xk) = sdtasdt0(xk, sz10), 586 : aNaturalNumber0(xk), 586 : aNaturalNumber0(sdtasdt0(sz10, xk))],extension(569 ^ 2,bind([[_145240, _145242, _145800], [sdtasdt0(sz10, xk), xk, sz10]]))).
% 161.85/156.49 ncf('1.2.2.1',plain,[-(aNaturalNumber0(sz10))],extension(134 ^ 7)).
% 161.85/156.49 ncf('1.2.2.2',plain,[-(sdtasdt0(sz10, xk) = sdtasdt0(xk, sz10)), aNaturalNumber0(sz10), aNaturalNumber0(xk)],extension(190 ^ 7,bind([[_133883, _133885], [xk, sz10]]))).
% 161.85/156.49 ncf('1.2.2.2.1',plain,[-(aNaturalNumber0(sz10))],lemmata('[2, 1].x')).
% 161.85/156.49 ncf('1.2.2.2.2',plain,[-(aNaturalNumber0(xk))],extension(783 ^ 8)).
% 161.85/156.49 ncf('1.2.2.3',plain,[-(aNaturalNumber0(xk))],extension(783 ^ 3)).
% 161.85/156.49 ncf('1.2.2.4',plain,[-(aNaturalNumber0(sdtasdt0(sz10, xk))), aNaturalNumber0(sz10), aNaturalNumber0(xk)],extension(148 ^ 3,bind([[_132570, _132572], [xk, sz10]]))).
% 161.85/156.49 ncf('1.2.2.4.1',plain,[-(aNaturalNumber0(sz10))],extension(134 ^ 4)).
% 161.85/156.49 ncf('1.2.2.4.2',plain,[-(aNaturalNumber0(xk))],lemmata('[2, 1].x')).
% 161.85/156.49 ncf('1.2.3',plain,[-(sdtasdt0(sz10, xk) = xk), sdtasdt0(sz10, xk) = sdtasdt0(xk, sz10), sdtasdt0(xk, sz10) = xk],extension(10 ^ 2,bind([[_128197, _128199, _128201], [xk, sdtasdt0(xk, sz10), sdtasdt0(sz10, xk)]]))).
% 161.85/156.49 ncf('1.2.3.1',plain,[-(sdtasdt0(sz10, xk) = sdtasdt0(xk, sz10)), aNaturalNumber0(sz10), aNaturalNumber0(xk)],extension(190 ^ 3,bind([[_133883, _133885], [xk, sz10]]))).
% 161.85/156.49 ncf('1.2.3.1.1',plain,[-(aNaturalNumber0(sz10))],extension(134 ^ 4)).
% 161.85/156.49 ncf('1.2.3.1.2',plain,[-(aNaturalNumber0(xk))],extension(783 ^ 4)).
% 161.85/156.49 ncf('1.2.3.2',plain,[-(sdtasdt0(xk, sz10) = xk), aNaturalNumber0(xk)],extension(214 ^ 3,bind([[_134610], [xk]]))).
% 161.85/156.49 ncf('1.2.3.2.1',plain,[-(aNaturalNumber0(xk))],extension(783 ^ 4)).
% 161.85/156.49 ncf('1.3',plain,[-(aNaturalNumber0(xk))],extension(783 ^ 1)).
% 161.85/156.49 ncf('1.4',plain,[-(doDivides0(xk, xk)), 588 : aNaturalNumber0(sz10), 588 : xk = sdtasdt0(xk, sz10), 586 : aNaturalNumber0(xk), 586 : aNaturalNumber0(xk)],extension(569 ^ 3,bind([[_145240, _145242, _145800], [xk, xk, sz10]]))).
% 161.85/156.49 ncf('1.4.1',plain,[-(aNaturalNumber0(sz10))],extension(134 ^ 8)).
% 161.85/156.49 ncf('1.4.2',plain,[-(xk = sdtasdt0(xk, sz10)), xk = sdtasdt0(sz10, xk), sdtasdt0(sz10, xk) = sdtasdt0(xk, sz10)],extension(10 ^ 8,bind([[_128197, _128199, _128201], [sdtasdt0(xk, sz10), sdtasdt0(sz10, xk), xk]]))).
% 161.85/156.49 ncf('1.4.2.1',plain,[-(xk = sdtasdt0(sz10, xk)), aNaturalNumber0(xk)],extension(214 ^ 9,bind([[_134610], [xk]]))).
% 161.85/156.49 ncf('1.4.2.1.1',plain,[-(aNaturalNumber0(xk))],lemmata('x')).
% 161.85/156.49 ncf('1.4.2.2',plain,[-(sdtasdt0(sz10, xk) = sdtasdt0(xk, sz10)), aNaturalNumber0(sz10), aNaturalNumber0(xk)],extension(190 ^ 9,bind([[_133883, _133885], [xk, sz10]]))).
% 161.85/156.49 ncf('1.4.2.2.1',plain,[-(aNaturalNumber0(sz10))],lemmata('[1].x')).
% 161.85/156.49 ncf('1.4.2.2.2',plain,[-(aNaturalNumber0(xk))],lemmata('x')).
% 161.85/156.49 ncf('1.4.3',plain,[-(aNaturalNumber0(xk))],lemmata('x')).
% 161.85/156.49 ncf('1.4.4',plain,[-(aNaturalNumber0(xk))],lemmata('[1].x')).
% 161.85/156.49 %-----------------------------------------------------
% 161.85/156.49 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------