%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV086+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n020.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:56 EDT 2023
% Result : Theorem 0.35s 1.40s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SWV086+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.03/0.14 % Command : nanocop.sh %s %d
% 0.14/0.35 % Computer : n020.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Fri May 19 02:30:32 EDT 2023
% 0.14/0.35 % CPUTime :
% 0.35/1.40
% 0.35/1.40 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.35/1.40 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.35/1.40 %-----------------------------------------------------
% 0.35/1.40 ncf(matrix, plain, [(1041 ^ _194663) ^ [] : [geq(pv65, tptp_float_0_001)], (1043 ^ _194663) ^ [] : [true], (2 ^ _194663) ^ [_194807] : [-(_194807 = _194807)], (4 ^ _194663) ^ [_194914, _194916] : [_194916 = _194914, -(_194914 = _194916)], (10 ^ _194663) ^ [_195118, _195120, _195122] : [-(_195122 = _195118), _195122 = _195120, _195120 = _195118], (20 ^ _194663) ^ [_195459, _195461, _195463, _195465] : [-(lt(_195463, _195459)), lt(_195465, _195461), _195465 = _195463, _195461 = _195459], (34 ^ _194663) ^ [_195903, _195905, _195907, _195909] : [-(gt(_195907, _195903)), gt(_195909, _195905), _195909 = _195907, _195905 = _195903], (48 ^ _194663) ^ [_196347, _196349, _196351, _196353] : [-(leq(_196351, _196347)), leq(_196353, _196349), _196353 = _196351, _196349 = _196347], (62 ^ _194663) ^ [_196771, _196773, _196775, _196777] : [-(geq(_196775, _196771)), geq(_196777, _196773), _196777 = _196775, _196773 = _196771], (76 ^ _194663) ^ [_197227, _197229, _197231, _197233] : [-(uniform_int_rnd(_197233, _197229) = uniform_int_rnd(_197231, _197227)), _197233 = _197231, _197229 = _197227], (86 ^ _194663) ^ [_197586, _197588, _197590, _197592] : [-(tptp_const_array1(_197592, _197588) = tptp_const_array1(_197590, _197586)), _197592 = _197590, _197588 = _197586], (96 ^ _194663) ^ [_197973, _197975, _197977, _197979, _197981, _197983] : [-(tptp_const_array2(_197983, _197979, _197975) = tptp_const_array2(_197981, _197977, _197973)), _197983 = _197981, _197979 = _197977, _197975 = _197973], (110 ^ _194663) ^ [_198461, _198463, _198465, _198467] : [-(dim(_198467, _198463) = dim(_198465, _198461)), _198467 = _198465, _198463 = _198461], (120 ^ _194663) ^ [_198792, _198794] : [_198794 = _198792, -(inv(_198794) = inv(_198792))], (126 ^ _194663) ^ [_199038, _199040, _199042, _199044] : [-(tptp_msub(_199044, _199040) = tptp_msub(_199042, _199038)), _199044 = _199042, _199040 = _199038], (136 ^ _194663) ^ [_199397, _199399, _199401, _199403] : [-(tptp_madd(_199403, _199399) = tptp_madd(_199401, _199397)), _199403 = _199401, _199399 = _199397], (146 ^ _194663) ^ [_199756, _199758, _199760, _199762] : [-(tptp_mmul(_199762, _199758) = tptp_mmul(_199760, _199756)), _199762 = _199760, _199758 = _199756], (156 ^ _194663) ^ [_200087, _200089] : [_200089 = _200087, -(trans(_200089) = trans(_200087))], (162 ^ _194663) ^ [_200361, _200363, _200365, _200367, _200369, _200371] : [-(sum(_200371, _200367, _200363) = sum(_200369, _200365, _200361)), _200371 = _200369, _200367 = _200365, _200363 = _200361], (176 ^ _194663) ^ [_200849, _200851, _200853, _200855] : [-(plus(_200855, _200851) = plus(_200853, _200849)), _200855 = _200853, _200851 = _200849], (186 ^ _194663) ^ [_201180, _201182] : [_201182 = _201180, -(pred(_201182) = pred(_201180))], (192 ^ _194663) ^ [_201426, _201428, _201430, _201432] : [-(minus(_201432, _201428) = minus(_201430, _201426)), _201432 = _201430, _201428 = _201426], (202 ^ _194663) ^ [_201813, _201815, _201817, _201819, _201821, _201823] : [-(a_select3(_201823, _201819, _201815) = a_select3(_201821, _201817, _201813)), _201823 = _201821, _201819 = _201817, _201815 = _201813], (216 ^ _194663) ^ [_202357, _202359, _202361, _202363, _202365, _202367, _202369, _202371] : [-(tptp_update3(_202371, _202367, _202363, _202359) = tptp_update3(_202369, _202365, _202361, _202357)), _202371 = _202369, _202367 = _202365, _202363 = _202361, _202359 = _202357], (234 ^ _194663) ^ [_202990, _202992, _202994, _202996] : [-(a_select2(_202996, _202992) = a_select2(_202994, _202990)), _202996 = _202994, _202992 = _202990], (258 ^ _194663) ^ [_203817, _203819] : [_203819 = _203817, -(succ(_203819) = succ(_203817))], (244 ^ _194663) ^ [_203377, _203379, _203381, _203383, _203385, _203387] : [-(tptp_update2(_203387, _203383, _203379) = tptp_update2(_203385, _203381, _203377)), _203387 = _203385, _203383 = _203381, _203379 = _203377], (869 ^ _194663) ^ [] : [-(gt(n5, n4))], (871 ^ _194663) ^ [] : [-(gt(n4, tptp_minus_1))], (873 ^ _194663) ^ [] : [-(gt(n5, tptp_minus_1))], (875 ^ _194663) ^ [] : [-(gt(n0, tptp_minus_1))], (877 ^ _194663) ^ [] : [-(gt(n1, tptp_minus_1))], (879 ^ _194663) ^ [] : [-(gt(n2, tptp_minus_1))], (881 ^ _194663) ^ [] : [-(gt(n3, tptp_minus_1))], (883 ^ _194663) ^ [] : [-(gt(n4, n0))], (885 ^ _194663) ^ [] : [-(gt(n5, n0))], (887 ^ _194663) ^ [] : [-(gt(n1, n0))], (889 ^ _194663) ^ [] : [-(gt(n2, n0))], (891 ^ _194663) ^ [] : [-(gt(n3, n0))], (893 ^ _194663) ^ [] : [-(gt(n4, n1))], (895 ^ _194663) ^ [] : [-(gt(n5, n1))], (897 ^ _194663) ^ [] : [-(gt(n2, n1))], (899 ^ _194663) ^ [] : [-(gt(n3, n1))], (901 ^ _194663) ^ [] : [-(gt(n4, n2))], (903 ^ _194663) ^ [] : [-(gt(n5, n2))], (905 ^ _194663) ^ [] : [-(gt(n3, n2))], (907 ^ _194663) ^ [] : [-(gt(n4, n3))], (909 ^ _194663) ^ [] : [-(gt(n5, n3))], (911 ^ _194663) ^ [_231173] : [leq(n0, _231173), leq(_231173, n4), -(_231173 = n0), -(_231173 = n1), -(_231173 = n2), -(_231173 = n3), -(_231173 = n4)], (937 ^ _194663) ^ [_231794] : [leq(n0, _231794), leq(_231794, n5), -(_231794 = n0), -(_231794 = n1), -(_231794 = n2), -(_231794 = n3), -(_231794 = n4), -(_231794 = n5)], (967 ^ _194663) ^ [_232501] : [-(_232501 = n0), leq(n0, _232501), leq(_232501, n0)], (977 ^ _194663) ^ [_232776] : [leq(n0, _232776), leq(_232776, n1), -(_232776 = n0), -(_232776 = n1)], (991 ^ _194663) ^ [_233139] : [leq(n0, _233139), leq(_233139, n2), -(_233139 = n0), -(_233139 = n1), -(_233139 = n2)], (1031 ^ _194663) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (1033 ^ _194663) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (1035 ^ _194663) ^ [] : [-(succ(n0) = n1)], (1037 ^ _194663) ^ [] : [-(succ(succ(n0)) = n2)], (1039 ^ _194663) ^ [] : [-(succ(succ(succ(n0))) = n3)], (1009 ^ _194663) ^ [_233588] : [leq(n0, _233588), leq(_233588, n3), -(_233588 = n0), -(_233588 = n1), -(_233588 = n2), -(_233588 = n3)], (264 ^ _194663) ^ [_204135, _204137] : [-(gt(_204137, _204135)), -(gt(_204135, _204137)), -(_204137 = _204135)], (274 ^ _194663) ^ [_204450, _204452, _204454] : [-(gt(_204454, _204450)), gt(_204454, _204452), gt(_204452, _204450)], (284 ^ _194663) ^ [_204729] : [gt(_204729, _204729)], (286 ^ _194663) ^ [_204807] : [-(leq(_204807, _204807))], (288 ^ _194663) ^ [_204928, _204930, _204932] : [-(leq(_204932, _204928)), leq(_204932, _204930), leq(_204930, _204928)], (298 ^ _194663) ^ [_205266, _205268] : [lt(_205268, _205266), -(gt(_205266, _205268))], (304 ^ _194663) ^ [_205428, _205430] : [gt(_205428, _205430), -(lt(_205430, _205428))], (310 ^ _194663) ^ [_205669, _205671] : [geq(_205671, _205669), -(leq(_205669, _205671))], (316 ^ _194663) ^ [_205831, _205833] : [leq(_205831, _205833), -(geq(_205833, _205831))], (322 ^ _194663) ^ [_206043, _206045] : [gt(_206043, _206045), -(leq(_206045, _206043))], (328 ^ _194663) ^ [_206253, _206255] : [-(gt(_206253, _206255)), leq(_206255, _206253), -(_206255 = _206253)], (338 ^ _194663) ^ [_206584, _206586] : [leq(_206586, pred(_206584)), -(gt(_206584, _206586))], (344 ^ _194663) ^ [_206750, _206752] : [gt(_206750, _206752), -(leq(_206752, pred(_206750)))], (350 ^ _194663) ^ [_206937] : [-(gt(succ(_206937), _206937))], (352 ^ _194663) ^ [_207046, _207048] : [leq(_207048, _207046), -(leq(_207048, succ(_207046)))], (358 ^ _194663) ^ [_207289, _207291] : [leq(_207291, _207289), -(gt(succ(_207289), _207291))], (364 ^ _194663) ^ [_207455, _207457] : [gt(succ(_207455), _207457), -(leq(_207457, _207455))], (370 ^ _194663) ^ [_207671, _207673] : [leq(n0, _207673), -(leq(uniform_int_rnd(_207671, _207673), _207673))], (376 ^ _194663) ^ [_207887, _207889] : [leq(n0, _207889), -(leq(n0, uniform_int_rnd(_207887, _207889)))], (382 ^ _194663) ^ [_208131, _208133, _208135, _208137] : [-(a_select2(tptp_const_array1(dim(_208135, _208133), _208131), _208137) = _208131), leq(_208135, _208137), leq(_208137, _208133)], (392 ^ _194663) ^ [_208538, _208540, _208542, _208544, _208546, _208548, _208550] : [-(a_select3(tptp_const_array2(dim(_208548, _208546), dim(_208542, _208540), _208538), _208550, _208544) = _208538), leq(_208548, _208550), leq(_208550, _208546), leq(_208542, _208544), leq(_208544, _208540)], (410 ^ _194663) ^ [_209133, _209135] : [413 ^ _194663 : [(414 ^ _194663) ^ [] : [-(leq(n0, 411 ^ [_209133, _209135]))], (416 ^ _194663) ^ [] : [-(leq(411 ^ [_209133, _209135], _209133))], (418 ^ _194663) ^ [] : [-(leq(n0, 412 ^ [_209133, _209135]))], (420 ^ _194663) ^ [] : [-(leq(412 ^ [_209133, _209135], _209133))], (422 ^ _194663) ^ [] : [a_select3(_209135, 411 ^ [_209133, _209135], 412 ^ [_209133, _209135]) = a_select3(_209135, 412 ^ [_209133, _209135], 411 ^ [_209133, _209135])]], 423 ^ _194663 : [(424 ^ _194663) ^ [_209890, _209892] : [-(a_select3(trans(_209135), _209892, _209890) = a_select3(trans(_209135), _209890, _209892)), leq(n0, _209892), leq(_209892, _209133), leq(n0, _209890), leq(_209890, _209133)]]], (442 ^ _194663) ^ [_210437, _210439] : [445 ^ _194663 : [(446 ^ _194663) ^ [] : [-(leq(n0, 443 ^ [_210437, _210439]))], (448 ^ _194663) ^ [] : [-(leq(443 ^ [_210437, _210439], _210437))], (450 ^ _194663) ^ [] : [-(leq(n0, 444 ^ [_210437, _210439]))], (452 ^ _194663) ^ [] : [-(leq(444 ^ [_210437, _210439], _210437))], (454 ^ _194663) ^ [] : [a_select3(_210439, 443 ^ [_210437, _210439], 444 ^ [_210437, _210439]) = a_select3(_210439, 444 ^ [_210437, _210439], 443 ^ [_210437, _210439])]], 455 ^ _194663 : [(456 ^ _194663) ^ [_211194, _211196] : [-(a_select3(inv(_210439), _211196, _211194) = a_select3(inv(_210439), _211194, _211196)), leq(n0, _211196), leq(_211196, _210437), leq(n0, _211194), leq(_211194, _210437)]]], (474 ^ _194663) ^ [_211741, _211743] : [477 ^ _194663 : [(478 ^ _194663) ^ [] : [-(leq(n0, 475 ^ [_211741, _211743]))], (480 ^ _194663) ^ [] : [-(leq(475 ^ [_211741, _211743], _211741))], (482 ^ _194663) ^ [] : [-(leq(n0, 476 ^ [_211741, _211743]))], (484 ^ _194663) ^ [] : [-(leq(476 ^ [_211741, _211743], _211741))], (486 ^ _194663) ^ [] : [a_select3(_211743, 475 ^ [_211741, _211743], 476 ^ [_211741, _211743]) = a_select3(_211743, 476 ^ [_211741, _211743], 475 ^ [_211741, _211743])]], 487 ^ _194663 : [(488 ^ _194663) ^ [_212554, _212556, _212558, _212560] : [-(a_select3(tptp_update3(_211743, _212556, _212556, _212554), _212560, _212558) = a_select3(tptp_update3(_211743, _212556, _212556, _212554), _212558, _212560)), leq(n0, _212560), leq(_212560, _211741), leq(n0, _212558), leq(_212558, _211741), leq(n0, _212556), leq(_212556, _211741)]]], (514 ^ _194663) ^ [_213373, _213375, _213377] : [519 ^ _194663 : [(520 ^ _194663) ^ [] : [-(leq(n0, 517 ^ [_213373, _213375, _213377]))], (522 ^ _194663) ^ [] : [-(leq(517 ^ [_213373, _213375, _213377], _213373))], (524 ^ _194663) ^ [] : [-(leq(n0, 518 ^ [_213373, _213375, _213377]))], (526 ^ _194663) ^ [] : [-(leq(518 ^ [_213373, _213375, _213377], _213373))], (528 ^ _194663) ^ [] : [a_select3(_213377, 517 ^ [_213373, _213375, _213377], 518 ^ [_213373, _213375, _213377]) = a_select3(_213377, 518 ^ [_213373, _213375, _213377], 517 ^ [_213373, _213375, _213377])]], 531 ^ _194663 : [(532 ^ _194663) ^ [] : [-(leq(n0, 529 ^ [_213373, _213375, _213377]))], (534 ^ _194663) ^ [] : [-(leq(529 ^ [_213373, _213375, _213377], _213373))], (536 ^ _194663) ^ [] : [-(leq(n0, 530 ^ [_213373, _213375, _213377]))], (538 ^ _194663) ^ [] : [-(leq(530 ^ [_213373, _213375, _213377], _213373))], (540 ^ _194663) ^ [] : [a_select3(_213375, 529 ^ [_213373, _213375, _213377], 530 ^ [_213373, _213375, _213377]) = a_select3(_213375, 530 ^ [_213373, _213375, _213377], 529 ^ [_213373, _213375, _213377])]], 541 ^ _194663 : [(542 ^ _194663) ^ [_214882, _214884] : [-(a_select3(tptp_madd(_213377, _213375), _214884, _214882) = a_select3(tptp_madd(_213377, _213375), _214882, _214884)), leq(n0, _214884), leq(_214884, _213373), leq(n0, _214882), leq(_214882, _213373)]]], (560 ^ _194663) ^ [_215468, _215470, _215472] : [565 ^ _194663 : [(566 ^ _194663) ^ [] : [-(leq(n0, 563 ^ [_215468, _215470, _215472]))], (568 ^ _194663) ^ [] : [-(leq(563 ^ [_215468, _215470, _215472], _215468))], (570 ^ _194663) ^ [] : [-(leq(n0, 564 ^ [_215468, _215470, _215472]))], (572 ^ _194663) ^ [] : [-(leq(564 ^ [_215468, _215470, _215472], _215468))], (574 ^ _194663) ^ [] : [a_select3(_215472, 563 ^ [_215468, _215470, _215472], 564 ^ [_215468, _215470, _215472]) = a_select3(_215472, 564 ^ [_215468, _215470, _215472], 563 ^ [_215468, _215470, _215472])]], 577 ^ _194663 : [(578 ^ _194663) ^ [] : [-(leq(n0, 575 ^ [_215468, _215470, _215472]))], (580 ^ _194663) ^ [] : [-(leq(575 ^ [_215468, _215470, _215472], _215468))], (582 ^ _194663) ^ [] : [-(leq(n0, 576 ^ [_215468, _215470, _215472]))], (584 ^ _194663) ^ [] : [-(leq(576 ^ [_215468, _215470, _215472], _215468))], (586 ^ _194663) ^ [] : [a_select3(_215470, 575 ^ [_215468, _215470, _215472], 576 ^ [_215468, _215470, _215472]) = a_select3(_215470, 576 ^ [_215468, _215470, _215472], 575 ^ [_215468, _215470, _215472])]], 587 ^ _194663 : [(588 ^ _194663) ^ [_216977, _216979] : [-(a_select3(tptp_msub(_215472, _215470), _216979, _216977) = a_select3(tptp_msub(_215472, _215470), _216977, _216979)), leq(n0, _216979), leq(_216979, _215468), leq(n0, _216977), leq(_216977, _215468)]]], (606 ^ _194663) ^ [_217563, _217565, _217567] : [609 ^ _194663 : [(610 ^ _194663) ^ [] : [-(leq(n0, 607 ^ [_217563, _217565, _217567]))], (612 ^ _194663) ^ [] : [-(leq(607 ^ [_217563, _217565, _217567], _217563))], (614 ^ _194663) ^ [] : [-(leq(n0, 608 ^ [_217563, _217565, _217567]))], (616 ^ _194663) ^ [] : [-(leq(608 ^ [_217563, _217565, _217567], _217563))], (618 ^ _194663) ^ [] : [a_select3(_217565, 607 ^ [_217563, _217565, _217567], 608 ^ [_217563, _217565, _217567]) = a_select3(_217565, 608 ^ [_217563, _217565, _217567], 607 ^ [_217563, _217565, _217567])]], 619 ^ _194663 : [(620 ^ _194663) ^ [_218376, _218378] : [-(a_select3(tptp_mmul(_217567, tptp_mmul(_217565, trans(_217567))), _218378, _218376) = a_select3(tptp_mmul(_217567, tptp_mmul(_217565, trans(_217567))), _218376, _218378)), leq(n0, _218378), leq(_218378, _217563), leq(n0, _218376), leq(_218376, _217563)]]], (638 ^ _194663) ^ [_218995, _218997, _218999, _219001] : [641 ^ _194663 : [(642 ^ _194663) ^ [] : [-(leq(n0, 639 ^ [_218995, _218997, _218999, _219001]))], (644 ^ _194663) ^ [] : [-(leq(639 ^ [_218995, _218997, _218999, _219001], _218995))], (646 ^ _194663) ^ [] : [-(leq(n0, 640 ^ [_218995, _218997, _218999, _219001]))], (648 ^ _194663) ^ [] : [-(leq(640 ^ [_218995, _218997, _218999, _219001], _218995))], (650 ^ _194663) ^ [] : [a_select3(_218999, 639 ^ [_218995, _218997, _218999, _219001], 640 ^ [_218995, _218997, _218999, _219001]) = a_select3(_218999, 640 ^ [_218995, _218997, _218999, _219001], 639 ^ [_218995, _218997, _218999, _219001])]], 651 ^ _194663 : [(652 ^ _194663) ^ [_219852, _219854] : [-(a_select3(tptp_mmul(_219001, tptp_mmul(_218999, trans(_219001))), _219854, _219852) = a_select3(tptp_mmul(_219001, tptp_mmul(_218999, trans(_219001))), _219852, _219854)), leq(n0, _219854), leq(_219854, _218997), leq(n0, _219852), leq(_219852, _218997)]]], (670 ^ _194663) ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561] : [675 ^ _194663 : [(676 ^ _194663) ^ [] : [-(leq(n0, 673 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561]))], (678 ^ _194663) ^ [] : [-(leq(673 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561], _220547))], (680 ^ _194663) ^ [] : [-(leq(n0, 674 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561]))], (682 ^ _194663) ^ [] : [-(leq(674 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561], _220547))], (684 ^ _194663) ^ [] : [a_select3(_220555, 673 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561], 674 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561]) = a_select3(_220555, 674 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561], 673 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561])]], 689 ^ _194663 : [(690 ^ _194663) ^ [] : [-(leq(n0, 687 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561]))], (692 ^ _194663) ^ [] : [-(leq(687 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561], _220549))], (694 ^ _194663) ^ [] : [-(leq(n0, 688 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561]))], (696 ^ _194663) ^ [] : [-(leq(688 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561], _220549))], (698 ^ _194663) ^ [] : [a_select3(_220561, 687 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561], 688 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561]) = a_select3(_220561, 688 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561], 687 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561])]], 701 ^ _194663 : [(702 ^ _194663) ^ [] : [-(leq(n0, 699 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561]))], (704 ^ _194663) ^ [] : [-(leq(699 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561], _220549))], (706 ^ _194663) ^ [] : [-(leq(n0, 700 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561]))], (708 ^ _194663) ^ [] : [-(leq(700 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561], _220549))], (710 ^ _194663) ^ [] : [a_select3(_220551, 699 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561], 700 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561]) = a_select3(_220551, 700 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561], 699 ^ [_220547, _220549, _220551, _220553, _220555, _220557, _220559, _220561])]], 711 ^ _194663 : [(712 ^ _194663) ^ [_223475, _223477] : [-(a_select3(tptp_madd(_220561, tptp_mmul(_220559, tptp_mmul(tptp_madd(tptp_mmul(_220557, tptp_mmul(_220555, trans(_220557))), tptp_mmul(_220553, tptp_mmul(_220551, trans(_220553)))), trans(_220559)))), _223477, _223475) = a_select3(tptp_madd(_220561, tptp_mmul(_220559, tptp_mmul(tptp_madd(tptp_mmul(_220557, tptp_mmul(_220555, trans(_220557))), tptp_mmul(_220553, tptp_mmul(_220551, trans(_220553)))), trans(_220559)))), _223475, _223477)), leq(n0, _223477), leq(_223477, _220549), leq(n0, _223475), leq(_223475, _220549)]]], (730 ^ _194663) ^ [_224228] : [-(sum(n0, tptp_minus_1, _224228) = n0)], (732 ^ _194663) ^ [_224310] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _224310))], (734 ^ _194663) ^ [] : [-(succ(tptp_minus_1) = n0)], (736 ^ _194663) ^ [_224445] : [-(plus(_224445, n1) = succ(_224445))], (738 ^ _194663) ^ [_224528] : [-(plus(n1, _224528) = succ(_224528))], (740 ^ _194663) ^ [_224611] : [-(plus(_224611, n2) = succ(succ(_224611)))], (742 ^ _194663) ^ [_224696] : [-(plus(n2, _224696) = succ(succ(_224696)))], (744 ^ _194663) ^ [_224781] : [-(plus(_224781, n3) = succ(succ(succ(_224781))))], (746 ^ _194663) ^ [_224868] : [-(plus(n3, _224868) = succ(succ(succ(_224868))))], (748 ^ _194663) ^ [_224955] : [-(plus(_224955, n4) = succ(succ(succ(succ(_224955)))))], (750 ^ _194663) ^ [_225044] : [-(plus(n4, _225044) = succ(succ(succ(succ(_225044)))))], (752 ^ _194663) ^ [_225133] : [-(plus(_225133, n5) = succ(succ(succ(succ(succ(_225133))))))], (754 ^ _194663) ^ [_225224] : [-(plus(n5, _225224) = succ(succ(succ(succ(succ(_225224))))))], (756 ^ _194663) ^ [_225315] : [-(minus(_225315, n1) = pred(_225315))], (758 ^ _194663) ^ [_225398] : [-(pred(succ(_225398)) = _225398)], (760 ^ _194663) ^ [_225480] : [-(succ(pred(_225480)) = _225480)], (762 ^ _194663) ^ [_225620, _225622] : [leq(succ(_225622), succ(_225620)), -(leq(_225622, _225620))], (768 ^ _194663) ^ [_225790, _225792] : [leq(_225792, _225790), -(leq(succ(_225792), succ(_225790)))], (774 ^ _194663) ^ [_226010, _226012] : [leq(succ(_226012), _226010), -(gt(_226010, _226012))], (780 ^ _194663) ^ [_226224, _226226] : [leq(minus(_226226, _226224), _226226), -(leq(n0, _226224))], (786 ^ _194663) ^ [_226453, _226455, _226457, _226459] : [-(a_select3(tptp_update3(_226459, _226457, _226455, _226453), _226457, _226455) = _226453)], (788 ^ _194663) ^ [_226645, _226647, _226649, _226651, _226653, _226655, _226657] : [-(a_select3(tptp_update3(_226649, _226657, _226655, _226645), _226653, _226651) = _226647), -(_226657 = _226653), _226655 = _226651, a_select3(_226649, _226653, _226651) = _226647], (802 ^ _194663) ^ [_227188, _227190, _227192, _227194, _227196, _227198] : [-(a_select3(tptp_update3(_227190, _227194, _227192, _227188), _227198, _227196) = _227188), 807 ^ _194663 : [(808 ^ _194663) ^ [] : [-(leq(n0, 805 ^ [_227188, _227190, _227192, _227194, _227196, _227198]))], (810 ^ _194663) ^ [] : [-(leq(n0, 806 ^ [_227188, _227190, _227192, _227194, _227196, _227198]))], (812 ^ _194663) ^ [] : [-(leq(805 ^ [_227188, _227190, _227192, _227194, _227196, _227198], _227194))], (814 ^ _194663) ^ [] : [-(leq(806 ^ [_227188, _227190, _227192, _227194, _227196, _227198], _227192))], (816 ^ _194663) ^ [] : [a_select3(_227190, 805 ^ [_227188, _227190, _227192, _227194, _227196, _227198], 806 ^ [_227188, _227190, _227192, _227194, _227196, _227198]) = _227188]], leq(n0, _227198), leq(_227198, _227194), leq(n0, _227196), leq(_227196, _227192)], (834 ^ _194663) ^ [_228530, _228532, _228534] : [-(a_select2(tptp_update2(_228534, _228532, _228530), _228532) = _228530)], (836 ^ _194663) ^ [_228690, _228692, _228694, _228696, _228698] : [-(a_select2(tptp_update2(_228694, _228698, _228690), _228696) = _228692), -(_228698 = _228696), a_select2(_228694, _228696) = _228692], (865 ^ _194663) ^ [] : [-(true)], (867 ^ _194663) ^ [] : [def = use], (846 ^ _194663) ^ [_229070, _229072, _229074, _229076] : [-(a_select2(tptp_update2(_229072, _229074, _229070), _229076) = _229070), 850 ^ _194663 : [(851 ^ _194663) ^ [] : [-(leq(n0, 849 ^ [_229070, _229072, _229074, _229076]))], (853 ^ _194663) ^ [] : [-(leq(849 ^ [_229070, _229072, _229074, _229076], _229074))], (855 ^ _194663) ^ [] : [a_select2(_229072, 849 ^ [_229070, _229072, _229074, _229076]) = _229070]], leq(n0, _229076), leq(_229076, _229074)]], input).
% 0.35/1.40 ncf('1',plain,[true],start(1043 ^ 0)).
% 0.35/1.40 ncf('1.1',plain,[-(true)],extension(865 ^ 1)).
% 0.35/1.40 %-----------------------------------------------------
% 0.35/1.40 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------