%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV058+1 : TPTP v8.1.2. Bugfixed v3.3.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 12:19:51 EDT 2023
% Result : Theorem 0.32s 1.37s
% Output : Proof 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : SWV058+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n010.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 : Fri May 19 02:24:27 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.32/1.37
% 0.32/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.32/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.32/1.37 %-----------------------------------------------------
% 0.32/1.37 ncf(matrix, plain, [(1041 ^ _194695) ^ [] : [geq(pv72, tptp_float_0_001)], (1043 ^ _194695) ^ [] : [true], (2 ^ _194695) ^ [_194839] : [-(_194839 = _194839)], (4 ^ _194695) ^ [_194946, _194948] : [_194948 = _194946, -(_194946 = _194948)], (10 ^ _194695) ^ [_195150, _195152, _195154] : [-(_195154 = _195150), _195154 = _195152, _195152 = _195150], (20 ^ _194695) ^ [_195491, _195493, _195495, _195497] : [-(lt(_195495, _195491)), lt(_195497, _195493), _195497 = _195495, _195493 = _195491], (34 ^ _194695) ^ [_195935, _195937, _195939, _195941] : [-(gt(_195939, _195935)), gt(_195941, _195937), _195941 = _195939, _195937 = _195935], (48 ^ _194695) ^ [_196379, _196381, _196383, _196385] : [-(leq(_196383, _196379)), leq(_196385, _196381), _196385 = _196383, _196381 = _196379], (62 ^ _194695) ^ [_196803, _196805, _196807, _196809] : [-(geq(_196807, _196803)), geq(_196809, _196805), _196809 = _196807, _196805 = _196803], (76 ^ _194695) ^ [_197259, _197261, _197263, _197265] : [-(uniform_int_rnd(_197265, _197261) = uniform_int_rnd(_197263, _197259)), _197265 = _197263, _197261 = _197259], (86 ^ _194695) ^ [_197618, _197620, _197622, _197624] : [-(tptp_const_array1(_197624, _197620) = tptp_const_array1(_197622, _197618)), _197624 = _197622, _197620 = _197618], (96 ^ _194695) ^ [_198005, _198007, _198009, _198011, _198013, _198015] : [-(tptp_const_array2(_198015, _198011, _198007) = tptp_const_array2(_198013, _198009, _198005)), _198015 = _198013, _198011 = _198009, _198007 = _198005], (110 ^ _194695) ^ [_198493, _198495, _198497, _198499] : [-(dim(_198499, _198495) = dim(_198497, _198493)), _198499 = _198497, _198495 = _198493], (120 ^ _194695) ^ [_198824, _198826] : [_198826 = _198824, -(inv(_198826) = inv(_198824))], (126 ^ _194695) ^ [_199070, _199072, _199074, _199076] : [-(tptp_msub(_199076, _199072) = tptp_msub(_199074, _199070)), _199076 = _199074, _199072 = _199070], (136 ^ _194695) ^ [_199429, _199431, _199433, _199435] : [-(tptp_madd(_199435, _199431) = tptp_madd(_199433, _199429)), _199435 = _199433, _199431 = _199429], (146 ^ _194695) ^ [_199788, _199790, _199792, _199794] : [-(tptp_mmul(_199794, _199790) = tptp_mmul(_199792, _199788)), _199794 = _199792, _199790 = _199788], (156 ^ _194695) ^ [_200119, _200121] : [_200121 = _200119, -(trans(_200121) = trans(_200119))], (162 ^ _194695) ^ [_200393, _200395, _200397, _200399, _200401, _200403] : [-(sum(_200403, _200399, _200395) = sum(_200401, _200397, _200393)), _200403 = _200401, _200399 = _200397, _200395 = _200393], (176 ^ _194695) ^ [_200881, _200883, _200885, _200887] : [-(plus(_200887, _200883) = plus(_200885, _200881)), _200887 = _200885, _200883 = _200881], (186 ^ _194695) ^ [_201212, _201214] : [_201214 = _201212, -(pred(_201214) = pred(_201212))], (192 ^ _194695) ^ [_201458, _201460, _201462, _201464] : [-(minus(_201464, _201460) = minus(_201462, _201458)), _201464 = _201462, _201460 = _201458], (202 ^ _194695) ^ [_201845, _201847, _201849, _201851, _201853, _201855] : [-(a_select3(_201855, _201851, _201847) = a_select3(_201853, _201849, _201845)), _201855 = _201853, _201851 = _201849, _201847 = _201845], (216 ^ _194695) ^ [_202389, _202391, _202393, _202395, _202397, _202399, _202401, _202403] : [-(tptp_update3(_202403, _202399, _202395, _202391) = tptp_update3(_202401, _202397, _202393, _202389)), _202403 = _202401, _202399 = _202397, _202395 = _202393, _202391 = _202389], (234 ^ _194695) ^ [_203022, _203024, _203026, _203028] : [-(a_select2(_203028, _203024) = a_select2(_203026, _203022)), _203028 = _203026, _203024 = _203022], (258 ^ _194695) ^ [_203849, _203851] : [_203851 = _203849, -(succ(_203851) = succ(_203849))], (244 ^ _194695) ^ [_203409, _203411, _203413, _203415, _203417, _203419] : [-(tptp_update2(_203419, _203415, _203411) = tptp_update2(_203417, _203413, _203409)), _203419 = _203417, _203415 = _203413, _203411 = _203409], (869 ^ _194695) ^ [] : [-(gt(n5, n4))], (871 ^ _194695) ^ [] : [-(gt(n4, tptp_minus_1))], (873 ^ _194695) ^ [] : [-(gt(n5, tptp_minus_1))], (875 ^ _194695) ^ [] : [-(gt(n0, tptp_minus_1))], (877 ^ _194695) ^ [] : [-(gt(n1, tptp_minus_1))], (879 ^ _194695) ^ [] : [-(gt(n2, tptp_minus_1))], (881 ^ _194695) ^ [] : [-(gt(n3, tptp_minus_1))], (883 ^ _194695) ^ [] : [-(gt(n4, n0))], (885 ^ _194695) ^ [] : [-(gt(n5, n0))], (887 ^ _194695) ^ [] : [-(gt(n1, n0))], (889 ^ _194695) ^ [] : [-(gt(n2, n0))], (891 ^ _194695) ^ [] : [-(gt(n3, n0))], (893 ^ _194695) ^ [] : [-(gt(n4, n1))], (895 ^ _194695) ^ [] : [-(gt(n5, n1))], (897 ^ _194695) ^ [] : [-(gt(n2, n1))], (899 ^ _194695) ^ [] : [-(gt(n3, n1))], (901 ^ _194695) ^ [] : [-(gt(n4, n2))], (903 ^ _194695) ^ [] : [-(gt(n5, n2))], (905 ^ _194695) ^ [] : [-(gt(n3, n2))], (907 ^ _194695) ^ [] : [-(gt(n4, n3))], (909 ^ _194695) ^ [] : [-(gt(n5, n3))], (911 ^ _194695) ^ [_231205] : [leq(n0, _231205), leq(_231205, n4), -(_231205 = n0), -(_231205 = n1), -(_231205 = n2), -(_231205 = n3), -(_231205 = n4)], (937 ^ _194695) ^ [_231826] : [leq(n0, _231826), leq(_231826, n5), -(_231826 = n0), -(_231826 = n1), -(_231826 = n2), -(_231826 = n3), -(_231826 = n4), -(_231826 = n5)], (967 ^ _194695) ^ [_232533] : [-(_232533 = n0), leq(n0, _232533), leq(_232533, n0)], (977 ^ _194695) ^ [_232808] : [leq(n0, _232808), leq(_232808, n1), -(_232808 = n0), -(_232808 = n1)], (991 ^ _194695) ^ [_233171] : [leq(n0, _233171), leq(_233171, n2), -(_233171 = n0), -(_233171 = n1), -(_233171 = n2)], (1031 ^ _194695) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (1033 ^ _194695) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (1035 ^ _194695) ^ [] : [-(succ(n0) = n1)], (1037 ^ _194695) ^ [] : [-(succ(succ(n0)) = n2)], (1039 ^ _194695) ^ [] : [-(succ(succ(succ(n0))) = n3)], (1009 ^ _194695) ^ [_233620] : [leq(n0, _233620), leq(_233620, n3), -(_233620 = n0), -(_233620 = n1), -(_233620 = n2), -(_233620 = n3)], (264 ^ _194695) ^ [_204167, _204169] : [-(gt(_204169, _204167)), -(gt(_204167, _204169)), -(_204169 = _204167)], (274 ^ _194695) ^ [_204482, _204484, _204486] : [-(gt(_204486, _204482)), gt(_204486, _204484), gt(_204484, _204482)], (284 ^ _194695) ^ [_204761] : [gt(_204761, _204761)], (286 ^ _194695) ^ [_204839] : [-(leq(_204839, _204839))], (288 ^ _194695) ^ [_204960, _204962, _204964] : [-(leq(_204964, _204960)), leq(_204964, _204962), leq(_204962, _204960)], (298 ^ _194695) ^ [_205298, _205300] : [lt(_205300, _205298), -(gt(_205298, _205300))], (304 ^ _194695) ^ [_205460, _205462] : [gt(_205460, _205462), -(lt(_205462, _205460))], (310 ^ _194695) ^ [_205701, _205703] : [geq(_205703, _205701), -(leq(_205701, _205703))], (316 ^ _194695) ^ [_205863, _205865] : [leq(_205863, _205865), -(geq(_205865, _205863))], (322 ^ _194695) ^ [_206075, _206077] : [gt(_206075, _206077), -(leq(_206077, _206075))], (328 ^ _194695) ^ [_206285, _206287] : [-(gt(_206285, _206287)), leq(_206287, _206285), -(_206287 = _206285)], (338 ^ _194695) ^ [_206616, _206618] : [leq(_206618, pred(_206616)), -(gt(_206616, _206618))], (344 ^ _194695) ^ [_206782, _206784] : [gt(_206782, _206784), -(leq(_206784, pred(_206782)))], (350 ^ _194695) ^ [_206969] : [-(gt(succ(_206969), _206969))], (352 ^ _194695) ^ [_207078, _207080] : [leq(_207080, _207078), -(leq(_207080, succ(_207078)))], (358 ^ _194695) ^ [_207321, _207323] : [leq(_207323, _207321), -(gt(succ(_207321), _207323))], (364 ^ _194695) ^ [_207487, _207489] : [gt(succ(_207487), _207489), -(leq(_207489, _207487))], (370 ^ _194695) ^ [_207703, _207705] : [leq(n0, _207705), -(leq(uniform_int_rnd(_207703, _207705), _207705))], (376 ^ _194695) ^ [_207919, _207921] : [leq(n0, _207921), -(leq(n0, uniform_int_rnd(_207919, _207921)))], (382 ^ _194695) ^ [_208163, _208165, _208167, _208169] : [-(a_select2(tptp_const_array1(dim(_208167, _208165), _208163), _208169) = _208163), leq(_208167, _208169), leq(_208169, _208165)], (392 ^ _194695) ^ [_208570, _208572, _208574, _208576, _208578, _208580, _208582] : [-(a_select3(tptp_const_array2(dim(_208580, _208578), dim(_208574, _208572), _208570), _208582, _208576) = _208570), leq(_208580, _208582), leq(_208582, _208578), leq(_208574, _208576), leq(_208576, _208572)], (410 ^ _194695) ^ [_209165, _209167] : [413 ^ _194695 : [(414 ^ _194695) ^ [] : [-(leq(n0, 411 ^ [_209165, _209167]))], (416 ^ _194695) ^ [] : [-(leq(411 ^ [_209165, _209167], _209165))], (418 ^ _194695) ^ [] : [-(leq(n0, 412 ^ [_209165, _209167]))], (420 ^ _194695) ^ [] : [-(leq(412 ^ [_209165, _209167], _209165))], (422 ^ _194695) ^ [] : [a_select3(_209167, 411 ^ [_209165, _209167], 412 ^ [_209165, _209167]) = a_select3(_209167, 412 ^ [_209165, _209167], 411 ^ [_209165, _209167])]], 423 ^ _194695 : [(424 ^ _194695) ^ [_209922, _209924] : [-(a_select3(trans(_209167), _209924, _209922) = a_select3(trans(_209167), _209922, _209924)), leq(n0, _209924), leq(_209924, _209165), leq(n0, _209922), leq(_209922, _209165)]]], (442 ^ _194695) ^ [_210469, _210471] : [445 ^ _194695 : [(446 ^ _194695) ^ [] : [-(leq(n0, 443 ^ [_210469, _210471]))], (448 ^ _194695) ^ [] : [-(leq(443 ^ [_210469, _210471], _210469))], (450 ^ _194695) ^ [] : [-(leq(n0, 444 ^ [_210469, _210471]))], (452 ^ _194695) ^ [] : [-(leq(444 ^ [_210469, _210471], _210469))], (454 ^ _194695) ^ [] : [a_select3(_210471, 443 ^ [_210469, _210471], 444 ^ [_210469, _210471]) = a_select3(_210471, 444 ^ [_210469, _210471], 443 ^ [_210469, _210471])]], 455 ^ _194695 : [(456 ^ _194695) ^ [_211226, _211228] : [-(a_select3(inv(_210471), _211228, _211226) = a_select3(inv(_210471), _211226, _211228)), leq(n0, _211228), leq(_211228, _210469), leq(n0, _211226), leq(_211226, _210469)]]], (474 ^ _194695) ^ [_211773, _211775] : [477 ^ _194695 : [(478 ^ _194695) ^ [] : [-(leq(n0, 475 ^ [_211773, _211775]))], (480 ^ _194695) ^ [] : [-(leq(475 ^ [_211773, _211775], _211773))], (482 ^ _194695) ^ [] : [-(leq(n0, 476 ^ [_211773, _211775]))], (484 ^ _194695) ^ [] : [-(leq(476 ^ [_211773, _211775], _211773))], (486 ^ _194695) ^ [] : [a_select3(_211775, 475 ^ [_211773, _211775], 476 ^ [_211773, _211775]) = a_select3(_211775, 476 ^ [_211773, _211775], 475 ^ [_211773, _211775])]], 487 ^ _194695 : [(488 ^ _194695) ^ [_212586, _212588, _212590, _212592] : [-(a_select3(tptp_update3(_211775, _212588, _212588, _212586), _212592, _212590) = a_select3(tptp_update3(_211775, _212588, _212588, _212586), _212590, _212592)), leq(n0, _212592), leq(_212592, _211773), leq(n0, _212590), leq(_212590, _211773), leq(n0, _212588), leq(_212588, _211773)]]], (514 ^ _194695) ^ [_213405, _213407, _213409] : [519 ^ _194695 : [(520 ^ _194695) ^ [] : [-(leq(n0, 517 ^ [_213405, _213407, _213409]))], (522 ^ _194695) ^ [] : [-(leq(517 ^ [_213405, _213407, _213409], _213405))], (524 ^ _194695) ^ [] : [-(leq(n0, 518 ^ [_213405, _213407, _213409]))], (526 ^ _194695) ^ [] : [-(leq(518 ^ [_213405, _213407, _213409], _213405))], (528 ^ _194695) ^ [] : [a_select3(_213409, 517 ^ [_213405, _213407, _213409], 518 ^ [_213405, _213407, _213409]) = a_select3(_213409, 518 ^ [_213405, _213407, _213409], 517 ^ [_213405, _213407, _213409])]], 531 ^ _194695 : [(532 ^ _194695) ^ [] : [-(leq(n0, 529 ^ [_213405, _213407, _213409]))], (534 ^ _194695) ^ [] : [-(leq(529 ^ [_213405, _213407, _213409], _213405))], (536 ^ _194695) ^ [] : [-(leq(n0, 530 ^ [_213405, _213407, _213409]))], (538 ^ _194695) ^ [] : [-(leq(530 ^ [_213405, _213407, _213409], _213405))], (540 ^ _194695) ^ [] : [a_select3(_213407, 529 ^ [_213405, _213407, _213409], 530 ^ [_213405, _213407, _213409]) = a_select3(_213407, 530 ^ [_213405, _213407, _213409], 529 ^ [_213405, _213407, _213409])]], 541 ^ _194695 : [(542 ^ _194695) ^ [_214914, _214916] : [-(a_select3(tptp_madd(_213409, _213407), _214916, _214914) = a_select3(tptp_madd(_213409, _213407), _214914, _214916)), leq(n0, _214916), leq(_214916, _213405), leq(n0, _214914), leq(_214914, _213405)]]], (560 ^ _194695) ^ [_215500, _215502, _215504] : [565 ^ _194695 : [(566 ^ _194695) ^ [] : [-(leq(n0, 563 ^ [_215500, _215502, _215504]))], (568 ^ _194695) ^ [] : [-(leq(563 ^ [_215500, _215502, _215504], _215500))], (570 ^ _194695) ^ [] : [-(leq(n0, 564 ^ [_215500, _215502, _215504]))], (572 ^ _194695) ^ [] : [-(leq(564 ^ [_215500, _215502, _215504], _215500))], (574 ^ _194695) ^ [] : [a_select3(_215504, 563 ^ [_215500, _215502, _215504], 564 ^ [_215500, _215502, _215504]) = a_select3(_215504, 564 ^ [_215500, _215502, _215504], 563 ^ [_215500, _215502, _215504])]], 577 ^ _194695 : [(578 ^ _194695) ^ [] : [-(leq(n0, 575 ^ [_215500, _215502, _215504]))], (580 ^ _194695) ^ [] : [-(leq(575 ^ [_215500, _215502, _215504], _215500))], (582 ^ _194695) ^ [] : [-(leq(n0, 576 ^ [_215500, _215502, _215504]))], (584 ^ _194695) ^ [] : [-(leq(576 ^ [_215500, _215502, _215504], _215500))], (586 ^ _194695) ^ [] : [a_select3(_215502, 575 ^ [_215500, _215502, _215504], 576 ^ [_215500, _215502, _215504]) = a_select3(_215502, 576 ^ [_215500, _215502, _215504], 575 ^ [_215500, _215502, _215504])]], 587 ^ _194695 : [(588 ^ _194695) ^ [_217009, _217011] : [-(a_select3(tptp_msub(_215504, _215502), _217011, _217009) = a_select3(tptp_msub(_215504, _215502), _217009, _217011)), leq(n0, _217011), leq(_217011, _215500), leq(n0, _217009), leq(_217009, _215500)]]], (606 ^ _194695) ^ [_217595, _217597, _217599] : [609 ^ _194695 : [(610 ^ _194695) ^ [] : [-(leq(n0, 607 ^ [_217595, _217597, _217599]))], (612 ^ _194695) ^ [] : [-(leq(607 ^ [_217595, _217597, _217599], _217595))], (614 ^ _194695) ^ [] : [-(leq(n0, 608 ^ [_217595, _217597, _217599]))], (616 ^ _194695) ^ [] : [-(leq(608 ^ [_217595, _217597, _217599], _217595))], (618 ^ _194695) ^ [] : [a_select3(_217597, 607 ^ [_217595, _217597, _217599], 608 ^ [_217595, _217597, _217599]) = a_select3(_217597, 608 ^ [_217595, _217597, _217599], 607 ^ [_217595, _217597, _217599])]], 619 ^ _194695 : [(620 ^ _194695) ^ [_218408, _218410] : [-(a_select3(tptp_mmul(_217599, tptp_mmul(_217597, trans(_217599))), _218410, _218408) = a_select3(tptp_mmul(_217599, tptp_mmul(_217597, trans(_217599))), _218408, _218410)), leq(n0, _218410), leq(_218410, _217595), leq(n0, _218408), leq(_218408, _217595)]]], (638 ^ _194695) ^ [_219027, _219029, _219031, _219033] : [641 ^ _194695 : [(642 ^ _194695) ^ [] : [-(leq(n0, 639 ^ [_219027, _219029, _219031, _219033]))], (644 ^ _194695) ^ [] : [-(leq(639 ^ [_219027, _219029, _219031, _219033], _219027))], (646 ^ _194695) ^ [] : [-(leq(n0, 640 ^ [_219027, _219029, _219031, _219033]))], (648 ^ _194695) ^ [] : [-(leq(640 ^ [_219027, _219029, _219031, _219033], _219027))], (650 ^ _194695) ^ [] : [a_select3(_219031, 639 ^ [_219027, _219029, _219031, _219033], 640 ^ [_219027, _219029, _219031, _219033]) = a_select3(_219031, 640 ^ [_219027, _219029, _219031, _219033], 639 ^ [_219027, _219029, _219031, _219033])]], 651 ^ _194695 : [(652 ^ _194695) ^ [_219884, _219886] : [-(a_select3(tptp_mmul(_219033, tptp_mmul(_219031, trans(_219033))), _219886, _219884) = a_select3(tptp_mmul(_219033, tptp_mmul(_219031, trans(_219033))), _219884, _219886)), leq(n0, _219886), leq(_219886, _219029), leq(n0, _219884), leq(_219884, _219029)]]], (670 ^ _194695) ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593] : [675 ^ _194695 : [(676 ^ _194695) ^ [] : [-(leq(n0, 673 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593]))], (678 ^ _194695) ^ [] : [-(leq(673 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593], _220579))], (680 ^ _194695) ^ [] : [-(leq(n0, 674 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593]))], (682 ^ _194695) ^ [] : [-(leq(674 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593], _220579))], (684 ^ _194695) ^ [] : [a_select3(_220587, 673 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593], 674 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593]) = a_select3(_220587, 674 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593], 673 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593])]], 689 ^ _194695 : [(690 ^ _194695) ^ [] : [-(leq(n0, 687 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593]))], (692 ^ _194695) ^ [] : [-(leq(687 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593], _220581))], (694 ^ _194695) ^ [] : [-(leq(n0, 688 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593]))], (696 ^ _194695) ^ [] : [-(leq(688 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593], _220581))], (698 ^ _194695) ^ [] : [a_select3(_220593, 687 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593], 688 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593]) = a_select3(_220593, 688 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593], 687 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593])]], 701 ^ _194695 : [(702 ^ _194695) ^ [] : [-(leq(n0, 699 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593]))], (704 ^ _194695) ^ [] : [-(leq(699 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593], _220581))], (706 ^ _194695) ^ [] : [-(leq(n0, 700 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593]))], (708 ^ _194695) ^ [] : [-(leq(700 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593], _220581))], (710 ^ _194695) ^ [] : [a_select3(_220583, 699 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593], 700 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593]) = a_select3(_220583, 700 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593], 699 ^ [_220579, _220581, _220583, _220585, _220587, _220589, _220591, _220593])]], 711 ^ _194695 : [(712 ^ _194695) ^ [_223507, _223509] : [-(a_select3(tptp_madd(_220593, tptp_mmul(_220591, tptp_mmul(tptp_madd(tptp_mmul(_220589, tptp_mmul(_220587, trans(_220589))), tptp_mmul(_220585, tptp_mmul(_220583, trans(_220585)))), trans(_220591)))), _223509, _223507) = a_select3(tptp_madd(_220593, tptp_mmul(_220591, tptp_mmul(tptp_madd(tptp_mmul(_220589, tptp_mmul(_220587, trans(_220589))), tptp_mmul(_220585, tptp_mmul(_220583, trans(_220585)))), trans(_220591)))), _223507, _223509)), leq(n0, _223509), leq(_223509, _220581), leq(n0, _223507), leq(_223507, _220581)]]], (730 ^ _194695) ^ [_224260] : [-(sum(n0, tptp_minus_1, _224260) = n0)], (732 ^ _194695) ^ [_224342] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _224342))], (734 ^ _194695) ^ [] : [-(succ(tptp_minus_1) = n0)], (736 ^ _194695) ^ [_224477] : [-(plus(_224477, n1) = succ(_224477))], (738 ^ _194695) ^ [_224560] : [-(plus(n1, _224560) = succ(_224560))], (740 ^ _194695) ^ [_224643] : [-(plus(_224643, n2) = succ(succ(_224643)))], (742 ^ _194695) ^ [_224728] : [-(plus(n2, _224728) = succ(succ(_224728)))], (744 ^ _194695) ^ [_224813] : [-(plus(_224813, n3) = succ(succ(succ(_224813))))], (746 ^ _194695) ^ [_224900] : [-(plus(n3, _224900) = succ(succ(succ(_224900))))], (748 ^ _194695) ^ [_224987] : [-(plus(_224987, n4) = succ(succ(succ(succ(_224987)))))], (750 ^ _194695) ^ [_225076] : [-(plus(n4, _225076) = succ(succ(succ(succ(_225076)))))], (752 ^ _194695) ^ [_225165] : [-(plus(_225165, n5) = succ(succ(succ(succ(succ(_225165))))))], (754 ^ _194695) ^ [_225256] : [-(plus(n5, _225256) = succ(succ(succ(succ(succ(_225256))))))], (756 ^ _194695) ^ [_225347] : [-(minus(_225347, n1) = pred(_225347))], (758 ^ _194695) ^ [_225430] : [-(pred(succ(_225430)) = _225430)], (760 ^ _194695) ^ [_225512] : [-(succ(pred(_225512)) = _225512)], (762 ^ _194695) ^ [_225652, _225654] : [leq(succ(_225654), succ(_225652)), -(leq(_225654, _225652))], (768 ^ _194695) ^ [_225822, _225824] : [leq(_225824, _225822), -(leq(succ(_225824), succ(_225822)))], (774 ^ _194695) ^ [_226042, _226044] : [leq(succ(_226044), _226042), -(gt(_226042, _226044))], (780 ^ _194695) ^ [_226256, _226258] : [leq(minus(_226258, _226256), _226258), -(leq(n0, _226256))], (786 ^ _194695) ^ [_226485, _226487, _226489, _226491] : [-(a_select3(tptp_update3(_226491, _226489, _226487, _226485), _226489, _226487) = _226485)], (788 ^ _194695) ^ [_226677, _226679, _226681, _226683, _226685, _226687, _226689] : [-(a_select3(tptp_update3(_226681, _226689, _226687, _226677), _226685, _226683) = _226679), -(_226689 = _226685), _226687 = _226683, a_select3(_226681, _226685, _226683) = _226679], (802 ^ _194695) ^ [_227220, _227222, _227224, _227226, _227228, _227230] : [-(a_select3(tptp_update3(_227222, _227226, _227224, _227220), _227230, _227228) = _227220), 807 ^ _194695 : [(808 ^ _194695) ^ [] : [-(leq(n0, 805 ^ [_227220, _227222, _227224, _227226, _227228, _227230]))], (810 ^ _194695) ^ [] : [-(leq(n0, 806 ^ [_227220, _227222, _227224, _227226, _227228, _227230]))], (812 ^ _194695) ^ [] : [-(leq(805 ^ [_227220, _227222, _227224, _227226, _227228, _227230], _227226))], (814 ^ _194695) ^ [] : [-(leq(806 ^ [_227220, _227222, _227224, _227226, _227228, _227230], _227224))], (816 ^ _194695) ^ [] : [a_select3(_227222, 805 ^ [_227220, _227222, _227224, _227226, _227228, _227230], 806 ^ [_227220, _227222, _227224, _227226, _227228, _227230]) = _227220]], leq(n0, _227230), leq(_227230, _227226), leq(n0, _227228), leq(_227228, _227224)], (834 ^ _194695) ^ [_228562, _228564, _228566] : [-(a_select2(tptp_update2(_228566, _228564, _228562), _228564) = _228562)], (836 ^ _194695) ^ [_228722, _228724, _228726, _228728, _228730] : [-(a_select2(tptp_update2(_228726, _228730, _228722), _228728) = _228724), -(_228730 = _228728), a_select2(_228726, _228728) = _228724], (865 ^ _194695) ^ [] : [-(true)], (867 ^ _194695) ^ [] : [def = use], (846 ^ _194695) ^ [_229102, _229104, _229106, _229108] : [-(a_select2(tptp_update2(_229104, _229106, _229102), _229108) = _229102), 850 ^ _194695 : [(851 ^ _194695) ^ [] : [-(leq(n0, 849 ^ [_229102, _229104, _229106, _229108]))], (853 ^ _194695) ^ [] : [-(leq(849 ^ [_229102, _229104, _229106, _229108], _229106))], (855 ^ _194695) ^ [] : [a_select2(_229104, 849 ^ [_229102, _229104, _229106, _229108]) = _229102]], leq(n0, _229108), leq(_229108, _229106)]], input).
% 0.32/1.37 ncf('1',plain,[true],start(1043 ^ 0)).
% 0.32/1.37 ncf('1.1',plain,[-(true)],extension(865 ^ 1)).
% 0.32/1.37 %-----------------------------------------------------
% 0.32/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------