%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV179+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n014.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:20:07 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.02/0.11 % Problem : SWV179+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.02/0.12 % Command : nanocop.sh %s %d
% 0.12/0.32 % Computer : n014.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.32 % CPULimit : 300
% 0.16/0.32 % WCLimit : 300
% 0.16/0.32 % DateTime : Fri May 19 02:39:42 EDT 2023
% 0.16/0.32 % CPUTime :
% 0.32/1.37
% 0.32/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.32/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.32/1.37 %-----------------------------------------------------
% 0.32/1.37 ncf(matrix, plain, [(1137 ^ _206485) ^ [] : [a_select2(rho_init, pv68) = init], (1055 ^ _206485) ^ [] : [-(leq(n0, pv68))], (1057 ^ _206485) ^ [] : [-(leq(pv68, n4))], (1059 ^ _206485) ^ [_246907] : [leq(n0, _246907), leq(_246907, n135299), 1066 ^ _206485 : [(1067 ^ _206485) ^ [_247135] : [-(a_select3(q_init, _246907, _247135) = init), leq(n0, _247135), leq(_247135, n4)]]], (1077 ^ _206485) ^ [_247437] : [-(a_select3(center_init, _247437, n0) = init), leq(n0, _247437), leq(_247437, n4)], (1087 ^ _206485) ^ [_247720] : [-(a_select2(muold_init, _247720) = init), leq(n0, _247720), leq(_247720, n4)], (1097 ^ _206485) ^ [_248001] : [-(a_select2(rhoold_init, _248001) = init), leq(n0, _248001), leq(_248001, pred(pv68))], (1107 ^ _206485) ^ [_248282] : [-(a_select2(mu_init, _248282) = init), leq(n0, _248282), leq(_248282, n4)], (1117 ^ _206485) ^ [_248563] : [-(a_select2(rho_init, _248563) = init), leq(n0, _248563), leq(_248563, n4)], (1127 ^ _206485) ^ [_248824] : [-(a_select2(sigma_init, _248824) = init), leq(n0, _248824), leq(_248824, n4)], (2 ^ _206485) ^ [_206629] : [-(_206629 = _206629)], (4 ^ _206485) ^ [_206736, _206738] : [_206738 = _206736, -(_206736 = _206738)], (10 ^ _206485) ^ [_206940, _206942, _206944] : [-(_206944 = _206940), _206944 = _206942, _206942 = _206940], (20 ^ _206485) ^ [_207281, _207283, _207285, _207287] : [-(lt(_207285, _207281)), lt(_207287, _207283), _207287 = _207285, _207283 = _207281], (34 ^ _206485) ^ [_207725, _207727, _207729, _207731] : [-(geq(_207729, _207725)), geq(_207731, _207727), _207731 = _207729, _207727 = _207725], (48 ^ _206485) ^ [_208169, _208171, _208173, _208175] : [-(gt(_208173, _208169)), gt(_208175, _208171), _208175 = _208173, _208171 = _208169], (62 ^ _206485) ^ [_208593, _208595, _208597, _208599] : [-(leq(_208597, _208593)), leq(_208599, _208595), _208599 = _208597, _208595 = _208593], (76 ^ _206485) ^ [_209049, _209051, _209053, _209055] : [-(uniform_int_rnd(_209055, _209051) = uniform_int_rnd(_209053, _209049)), _209055 = _209053, _209051 = _209049], (86 ^ _206485) ^ [_209408, _209410, _209412, _209414] : [-(tptp_const_array1(_209414, _209410) = tptp_const_array1(_209412, _209408)), _209414 = _209412, _209410 = _209408], (96 ^ _206485) ^ [_209795, _209797, _209799, _209801, _209803, _209805] : [-(tptp_const_array2(_209805, _209801, _209797) = tptp_const_array2(_209803, _209799, _209795)), _209805 = _209803, _209801 = _209799, _209797 = _209795], (110 ^ _206485) ^ [_210283, _210285, _210287, _210289] : [-(dim(_210289, _210285) = dim(_210287, _210283)), _210289 = _210287, _210285 = _210283], (120 ^ _206485) ^ [_210614, _210616] : [_210616 = _210614, -(inv(_210616) = inv(_210614))], (126 ^ _206485) ^ [_210860, _210862, _210864, _210866] : [-(tptp_msub(_210866, _210862) = tptp_msub(_210864, _210860)), _210866 = _210864, _210862 = _210860], (136 ^ _206485) ^ [_211219, _211221, _211223, _211225] : [-(tptp_madd(_211225, _211221) = tptp_madd(_211223, _211219)), _211225 = _211223, _211221 = _211219], (146 ^ _206485) ^ [_211578, _211580, _211582, _211584] : [-(tptp_mmul(_211584, _211580) = tptp_mmul(_211582, _211578)), _211584 = _211582, _211580 = _211578], (156 ^ _206485) ^ [_211909, _211911] : [_211911 = _211909, -(trans(_211911) = trans(_211909))], (162 ^ _206485) ^ [_212183, _212185, _212187, _212189, _212191, _212193] : [-(sum(_212193, _212189, _212185) = sum(_212191, _212187, _212183)), _212193 = _212191, _212189 = _212187, _212185 = _212183], (176 ^ _206485) ^ [_212671, _212673, _212675, _212677] : [-(plus(_212677, _212673) = plus(_212675, _212671)), _212677 = _212675, _212673 = _212671], (186 ^ _206485) ^ [_213030, _213032, _213034, _213036] : [-(minus(_213036, _213032) = minus(_213034, _213030)), _213036 = _213034, _213032 = _213030], (196 ^ _206485) ^ [_213445, _213447, _213449, _213451, _213453, _213455, _213457, _213459] : [-(tptp_update3(_213459, _213455, _213451, _213447) = tptp_update3(_213457, _213453, _213449, _213445)), _213459 = _213457, _213455 = _213453, _213451 = _213449, _213447 = _213445], (214 ^ _206485) ^ [_214106, _214108, _214110, _214112, _214114, _214116] : [-(tptp_update2(_214116, _214112, _214108) = tptp_update2(_214114, _214110, _214106)), _214116 = _214114, _214112 = _214110, _214108 = _214106], (228 ^ _206485) ^ [_214566, _214568] : [_214568 = _214566, -(succ(_214568) = succ(_214566))], (234 ^ _206485) ^ [_214840, _214842, _214844, _214846, _214848, _214850] : [-(a_select3(_214850, _214846, _214842) = a_select3(_214848, _214844, _214840)), _214850 = _214848, _214846 = _214844, _214842 = _214840], (248 ^ _206485) ^ [_215300, _215302] : [_215302 = _215300, -(pred(_215302) = pred(_215300))], (254 ^ _206485) ^ [_215526, _215528, _215530, _215532] : [-(a_select2(_215532, _215528) = a_select2(_215530, _215526)), _215532 = _215530, _215528 = _215526], (869 ^ _206485) ^ [] : [-(gt(n5, n4))], (871 ^ _206485) ^ [] : [-(gt(n135299, n4))], (873 ^ _206485) ^ [] : [-(gt(n135299, n5))], (875 ^ _206485) ^ [] : [-(gt(n4, tptp_minus_1))], (877 ^ _206485) ^ [] : [-(gt(n5, tptp_minus_1))], (879 ^ _206485) ^ [] : [-(gt(n135299, tptp_minus_1))], (881 ^ _206485) ^ [] : [-(gt(n0, tptp_minus_1))], (883 ^ _206485) ^ [] : [-(gt(n1, tptp_minus_1))], (885 ^ _206485) ^ [] : [-(gt(n2, tptp_minus_1))], (887 ^ _206485) ^ [] : [-(gt(n3, tptp_minus_1))], (889 ^ _206485) ^ [] : [-(gt(n4, n0))], (891 ^ _206485) ^ [] : [-(gt(n5, n0))], (893 ^ _206485) ^ [] : [-(gt(n135299, n0))], (895 ^ _206485) ^ [] : [-(gt(n1, n0))], (897 ^ _206485) ^ [] : [-(gt(n2, n0))], (899 ^ _206485) ^ [] : [-(gt(n3, n0))], (901 ^ _206485) ^ [] : [-(gt(n4, n1))], (903 ^ _206485) ^ [] : [-(gt(n5, n1))], (905 ^ _206485) ^ [] : [-(gt(n135299, n1))], (907 ^ _206485) ^ [] : [-(gt(n2, n1))], (909 ^ _206485) ^ [] : [-(gt(n3, n1))], (911 ^ _206485) ^ [] : [-(gt(n4, n2))], (913 ^ _206485) ^ [] : [-(gt(n5, n2))], (915 ^ _206485) ^ [] : [-(gt(n135299, n2))], (917 ^ _206485) ^ [] : [-(gt(n3, n2))], (919 ^ _206485) ^ [] : [-(gt(n4, n3))], (921 ^ _206485) ^ [] : [-(gt(n5, n3))], (923 ^ _206485) ^ [] : [-(gt(n135299, n3))], (925 ^ _206485) ^ [_243366] : [leq(n0, _243366), leq(_243366, n4), -(_243366 = n0), -(_243366 = n1), -(_243366 = n2), -(_243366 = n3), -(_243366 = n4)], (951 ^ _206485) ^ [_243987] : [leq(n0, _243987), leq(_243987, n5), -(_243987 = n0), -(_243987 = n1), -(_243987 = n2), -(_243987 = n3), -(_243987 = n4), -(_243987 = n5)], (981 ^ _206485) ^ [_244694] : [-(_244694 = n0), leq(n0, _244694), leq(_244694, n0)], (991 ^ _206485) ^ [_244969] : [leq(n0, _244969), leq(_244969, n1), -(_244969 = n0), -(_244969 = n1)], (1005 ^ _206485) ^ [_245332] : [leq(n0, _245332), leq(_245332, n2), -(_245332 = n0), -(_245332 = n1), -(_245332 = n2)], (1045 ^ _206485) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (1047 ^ _206485) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (1049 ^ _206485) ^ [] : [-(succ(n0) = n1)], (1051 ^ _206485) ^ [] : [-(succ(succ(n0)) = n2)], (1053 ^ _206485) ^ [] : [-(succ(succ(succ(n0))) = n3)], (1023 ^ _206485) ^ [_245781] : [leq(n0, _245781), leq(_245781, n3), -(_245781 = n0), -(_245781 = n1), -(_245781 = n2), -(_245781 = n3)], (264 ^ _206485) ^ [_215957, _215959] : [-(gt(_215959, _215957)), -(gt(_215957, _215959)), -(_215959 = _215957)], (274 ^ _206485) ^ [_216272, _216274, _216276] : [-(gt(_216276, _216272)), gt(_216276, _216274), gt(_216274, _216272)], (284 ^ _206485) ^ [_216551] : [gt(_216551, _216551)], (286 ^ _206485) ^ [_216629] : [-(leq(_216629, _216629))], (288 ^ _206485) ^ [_216750, _216752, _216754] : [-(leq(_216754, _216750)), leq(_216754, _216752), leq(_216752, _216750)], (298 ^ _206485) ^ [_217088, _217090] : [lt(_217090, _217088), -(gt(_217088, _217090))], (304 ^ _206485) ^ [_217250, _217252] : [gt(_217250, _217252), -(lt(_217252, _217250))], (310 ^ _206485) ^ [_217491, _217493] : [geq(_217493, _217491), -(leq(_217491, _217493))], (316 ^ _206485) ^ [_217653, _217655] : [leq(_217653, _217655), -(geq(_217655, _217653))], (322 ^ _206485) ^ [_217865, _217867] : [gt(_217865, _217867), -(leq(_217867, _217865))], (328 ^ _206485) ^ [_218075, _218077] : [-(gt(_218075, _218077)), leq(_218077, _218075), -(_218077 = _218075)], (338 ^ _206485) ^ [_218406, _218408] : [leq(_218408, pred(_218406)), -(gt(_218406, _218408))], (344 ^ _206485) ^ [_218572, _218574] : [gt(_218572, _218574), -(leq(_218574, pred(_218572)))], (350 ^ _206485) ^ [_218759] : [-(gt(succ(_218759), _218759))], (352 ^ _206485) ^ [_218868, _218870] : [leq(_218870, _218868), -(leq(_218870, succ(_218868)))], (358 ^ _206485) ^ [_219111, _219113] : [leq(_219113, _219111), -(gt(succ(_219111), _219113))], (364 ^ _206485) ^ [_219277, _219279] : [gt(succ(_219277), _219279), -(leq(_219279, _219277))], (370 ^ _206485) ^ [_219493, _219495] : [leq(n0, _219495), -(leq(uniform_int_rnd(_219493, _219495), _219495))], (376 ^ _206485) ^ [_219709, _219711] : [leq(n0, _219711), -(leq(n0, uniform_int_rnd(_219709, _219711)))], (382 ^ _206485) ^ [_219953, _219955, _219957, _219959] : [-(a_select2(tptp_const_array1(dim(_219957, _219955), _219953), _219959) = _219953), leq(_219957, _219959), leq(_219959, _219955)], (392 ^ _206485) ^ [_220360, _220362, _220364, _220366, _220368, _220370, _220372] : [-(a_select3(tptp_const_array2(dim(_220370, _220368), dim(_220364, _220362), _220360), _220372, _220366) = _220360), leq(_220370, _220372), leq(_220372, _220368), leq(_220364, _220366), leq(_220366, _220362)], (410 ^ _206485) ^ [_220955, _220957] : [413 ^ _206485 : [(414 ^ _206485) ^ [] : [-(leq(n0, 411 ^ [_220955, _220957]))], (416 ^ _206485) ^ [] : [-(leq(411 ^ [_220955, _220957], _220955))], (418 ^ _206485) ^ [] : [-(leq(n0, 412 ^ [_220955, _220957]))], (420 ^ _206485) ^ [] : [-(leq(412 ^ [_220955, _220957], _220955))], (422 ^ _206485) ^ [] : [a_select3(_220957, 411 ^ [_220955, _220957], 412 ^ [_220955, _220957]) = a_select3(_220957, 412 ^ [_220955, _220957], 411 ^ [_220955, _220957])]], 423 ^ _206485 : [(424 ^ _206485) ^ [_221712, _221714] : [-(a_select3(trans(_220957), _221714, _221712) = a_select3(trans(_220957), _221712, _221714)), leq(n0, _221714), leq(_221714, _220955), leq(n0, _221712), leq(_221712, _220955)]]], (442 ^ _206485) ^ [_222259, _222261] : [445 ^ _206485 : [(446 ^ _206485) ^ [] : [-(leq(n0, 443 ^ [_222259, _222261]))], (448 ^ _206485) ^ [] : [-(leq(443 ^ [_222259, _222261], _222259))], (450 ^ _206485) ^ [] : [-(leq(n0, 444 ^ [_222259, _222261]))], (452 ^ _206485) ^ [] : [-(leq(444 ^ [_222259, _222261], _222259))], (454 ^ _206485) ^ [] : [a_select3(_222261, 443 ^ [_222259, _222261], 444 ^ [_222259, _222261]) = a_select3(_222261, 444 ^ [_222259, _222261], 443 ^ [_222259, _222261])]], 455 ^ _206485 : [(456 ^ _206485) ^ [_223016, _223018] : [-(a_select3(inv(_222261), _223018, _223016) = a_select3(inv(_222261), _223016, _223018)), leq(n0, _223018), leq(_223018, _222259), leq(n0, _223016), leq(_223016, _222259)]]], (474 ^ _206485) ^ [_223563, _223565] : [477 ^ _206485 : [(478 ^ _206485) ^ [] : [-(leq(n0, 475 ^ [_223563, _223565]))], (480 ^ _206485) ^ [] : [-(leq(475 ^ [_223563, _223565], _223563))], (482 ^ _206485) ^ [] : [-(leq(n0, 476 ^ [_223563, _223565]))], (484 ^ _206485) ^ [] : [-(leq(476 ^ [_223563, _223565], _223563))], (486 ^ _206485) ^ [] : [a_select3(_223565, 475 ^ [_223563, _223565], 476 ^ [_223563, _223565]) = a_select3(_223565, 476 ^ [_223563, _223565], 475 ^ [_223563, _223565])]], 487 ^ _206485 : [(488 ^ _206485) ^ [_224376, _224378, _224380, _224382] : [-(a_select3(tptp_update3(_223565, _224378, _224378, _224376), _224382, _224380) = a_select3(tptp_update3(_223565, _224378, _224378, _224376), _224380, _224382)), leq(n0, _224382), leq(_224382, _223563), leq(n0, _224380), leq(_224380, _223563), leq(n0, _224378), leq(_224378, _223563)]]], (514 ^ _206485) ^ [_225195, _225197, _225199] : [519 ^ _206485 : [(520 ^ _206485) ^ [] : [-(leq(n0, 517 ^ [_225195, _225197, _225199]))], (522 ^ _206485) ^ [] : [-(leq(517 ^ [_225195, _225197, _225199], _225195))], (524 ^ _206485) ^ [] : [-(leq(n0, 518 ^ [_225195, _225197, _225199]))], (526 ^ _206485) ^ [] : [-(leq(518 ^ [_225195, _225197, _225199], _225195))], (528 ^ _206485) ^ [] : [a_select3(_225199, 517 ^ [_225195, _225197, _225199], 518 ^ [_225195, _225197, _225199]) = a_select3(_225199, 518 ^ [_225195, _225197, _225199], 517 ^ [_225195, _225197, _225199])]], 531 ^ _206485 : [(532 ^ _206485) ^ [] : [-(leq(n0, 529 ^ [_225195, _225197, _225199]))], (534 ^ _206485) ^ [] : [-(leq(529 ^ [_225195, _225197, _225199], _225195))], (536 ^ _206485) ^ [] : [-(leq(n0, 530 ^ [_225195, _225197, _225199]))], (538 ^ _206485) ^ [] : [-(leq(530 ^ [_225195, _225197, _225199], _225195))], (540 ^ _206485) ^ [] : [a_select3(_225197, 529 ^ [_225195, _225197, _225199], 530 ^ [_225195, _225197, _225199]) = a_select3(_225197, 530 ^ [_225195, _225197, _225199], 529 ^ [_225195, _225197, _225199])]], 541 ^ _206485 : [(542 ^ _206485) ^ [_226704, _226706] : [-(a_select3(tptp_madd(_225199, _225197), _226706, _226704) = a_select3(tptp_madd(_225199, _225197), _226704, _226706)), leq(n0, _226706), leq(_226706, _225195), leq(n0, _226704), leq(_226704, _225195)]]], (560 ^ _206485) ^ [_227290, _227292, _227294] : [565 ^ _206485 : [(566 ^ _206485) ^ [] : [-(leq(n0, 563 ^ [_227290, _227292, _227294]))], (568 ^ _206485) ^ [] : [-(leq(563 ^ [_227290, _227292, _227294], _227290))], (570 ^ _206485) ^ [] : [-(leq(n0, 564 ^ [_227290, _227292, _227294]))], (572 ^ _206485) ^ [] : [-(leq(564 ^ [_227290, _227292, _227294], _227290))], (574 ^ _206485) ^ [] : [a_select3(_227294, 563 ^ [_227290, _227292, _227294], 564 ^ [_227290, _227292, _227294]) = a_select3(_227294, 564 ^ [_227290, _227292, _227294], 563 ^ [_227290, _227292, _227294])]], 577 ^ _206485 : [(578 ^ _206485) ^ [] : [-(leq(n0, 575 ^ [_227290, _227292, _227294]))], (580 ^ _206485) ^ [] : [-(leq(575 ^ [_227290, _227292, _227294], _227290))], (582 ^ _206485) ^ [] : [-(leq(n0, 576 ^ [_227290, _227292, _227294]))], (584 ^ _206485) ^ [] : [-(leq(576 ^ [_227290, _227292, _227294], _227290))], (586 ^ _206485) ^ [] : [a_select3(_227292, 575 ^ [_227290, _227292, _227294], 576 ^ [_227290, _227292, _227294]) = a_select3(_227292, 576 ^ [_227290, _227292, _227294], 575 ^ [_227290, _227292, _227294])]], 587 ^ _206485 : [(588 ^ _206485) ^ [_228799, _228801] : [-(a_select3(tptp_msub(_227294, _227292), _228801, _228799) = a_select3(tptp_msub(_227294, _227292), _228799, _228801)), leq(n0, _228801), leq(_228801, _227290), leq(n0, _228799), leq(_228799, _227290)]]], (606 ^ _206485) ^ [_229385, _229387, _229389] : [609 ^ _206485 : [(610 ^ _206485) ^ [] : [-(leq(n0, 607 ^ [_229385, _229387, _229389]))], (612 ^ _206485) ^ [] : [-(leq(607 ^ [_229385, _229387, _229389], _229385))], (614 ^ _206485) ^ [] : [-(leq(n0, 608 ^ [_229385, _229387, _229389]))], (616 ^ _206485) ^ [] : [-(leq(608 ^ [_229385, _229387, _229389], _229385))], (618 ^ _206485) ^ [] : [a_select3(_229387, 607 ^ [_229385, _229387, _229389], 608 ^ [_229385, _229387, _229389]) = a_select3(_229387, 608 ^ [_229385, _229387, _229389], 607 ^ [_229385, _229387, _229389])]], 619 ^ _206485 : [(620 ^ _206485) ^ [_230198, _230200] : [-(a_select3(tptp_mmul(_229389, tptp_mmul(_229387, trans(_229389))), _230200, _230198) = a_select3(tptp_mmul(_229389, tptp_mmul(_229387, trans(_229389))), _230198, _230200)), leq(n0, _230200), leq(_230200, _229385), leq(n0, _230198), leq(_230198, _229385)]]], (638 ^ _206485) ^ [_230817, _230819, _230821, _230823] : [641 ^ _206485 : [(642 ^ _206485) ^ [] : [-(leq(n0, 639 ^ [_230817, _230819, _230821, _230823]))], (644 ^ _206485) ^ [] : [-(leq(639 ^ [_230817, _230819, _230821, _230823], _230817))], (646 ^ _206485) ^ [] : [-(leq(n0, 640 ^ [_230817, _230819, _230821, _230823]))], (648 ^ _206485) ^ [] : [-(leq(640 ^ [_230817, _230819, _230821, _230823], _230817))], (650 ^ _206485) ^ [] : [a_select3(_230821, 639 ^ [_230817, _230819, _230821, _230823], 640 ^ [_230817, _230819, _230821, _230823]) = a_select3(_230821, 640 ^ [_230817, _230819, _230821, _230823], 639 ^ [_230817, _230819, _230821, _230823])]], 651 ^ _206485 : [(652 ^ _206485) ^ [_231674, _231676] : [-(a_select3(tptp_mmul(_230823, tptp_mmul(_230821, trans(_230823))), _231676, _231674) = a_select3(tptp_mmul(_230823, tptp_mmul(_230821, trans(_230823))), _231674, _231676)), leq(n0, _231676), leq(_231676, _230819), leq(n0, _231674), leq(_231674, _230819)]]], (670 ^ _206485) ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383] : [675 ^ _206485 : [(676 ^ _206485) ^ [] : [-(leq(n0, 673 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383]))], (678 ^ _206485) ^ [] : [-(leq(673 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383], _232369))], (680 ^ _206485) ^ [] : [-(leq(n0, 674 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383]))], (682 ^ _206485) ^ [] : [-(leq(674 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383], _232369))], (684 ^ _206485) ^ [] : [a_select3(_232377, 673 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383], 674 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383]) = a_select3(_232377, 674 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383], 673 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383])]], 689 ^ _206485 : [(690 ^ _206485) ^ [] : [-(leq(n0, 687 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383]))], (692 ^ _206485) ^ [] : [-(leq(687 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383], _232371))], (694 ^ _206485) ^ [] : [-(leq(n0, 688 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383]))], (696 ^ _206485) ^ [] : [-(leq(688 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383], _232371))], (698 ^ _206485) ^ [] : [a_select3(_232383, 687 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383], 688 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383]) = a_select3(_232383, 688 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383], 687 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383])]], 701 ^ _206485 : [(702 ^ _206485) ^ [] : [-(leq(n0, 699 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383]))], (704 ^ _206485) ^ [] : [-(leq(699 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383], _232371))], (706 ^ _206485) ^ [] : [-(leq(n0, 700 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383]))], (708 ^ _206485) ^ [] : [-(leq(700 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383], _232371))], (710 ^ _206485) ^ [] : [a_select3(_232373, 699 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383], 700 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383]) = a_select3(_232373, 700 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383], 699 ^ [_232369, _232371, _232373, _232375, _232377, _232379, _232381, _232383])]], 711 ^ _206485 : [(712 ^ _206485) ^ [_235297, _235299] : [-(a_select3(tptp_madd(_232383, tptp_mmul(_232381, tptp_mmul(tptp_madd(tptp_mmul(_232379, tptp_mmul(_232377, trans(_232379))), tptp_mmul(_232375, tptp_mmul(_232373, trans(_232375)))), trans(_232381)))), _235299, _235297) = a_select3(tptp_madd(_232383, tptp_mmul(_232381, tptp_mmul(tptp_madd(tptp_mmul(_232379, tptp_mmul(_232377, trans(_232379))), tptp_mmul(_232375, tptp_mmul(_232373, trans(_232375)))), trans(_232381)))), _235297, _235299)), leq(n0, _235299), leq(_235299, _232371), leq(n0, _235297), leq(_235297, _232371)]]], (730 ^ _206485) ^ [_236050] : [-(sum(n0, tptp_minus_1, _236050) = n0)], (732 ^ _206485) ^ [_236132] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _236132))], (734 ^ _206485) ^ [] : [-(succ(tptp_minus_1) = n0)], (736 ^ _206485) ^ [_236267] : [-(plus(_236267, n1) = succ(_236267))], (738 ^ _206485) ^ [_236350] : [-(plus(n1, _236350) = succ(_236350))], (740 ^ _206485) ^ [_236433] : [-(plus(_236433, n2) = succ(succ(_236433)))], (742 ^ _206485) ^ [_236518] : [-(plus(n2, _236518) = succ(succ(_236518)))], (744 ^ _206485) ^ [_236603] : [-(plus(_236603, n3) = succ(succ(succ(_236603))))], (746 ^ _206485) ^ [_236690] : [-(plus(n3, _236690) = succ(succ(succ(_236690))))], (748 ^ _206485) ^ [_236777] : [-(plus(_236777, n4) = succ(succ(succ(succ(_236777)))))], (750 ^ _206485) ^ [_236866] : [-(plus(n4, _236866) = succ(succ(succ(succ(_236866)))))], (752 ^ _206485) ^ [_236955] : [-(plus(_236955, n5) = succ(succ(succ(succ(succ(_236955))))))], (754 ^ _206485) ^ [_237046] : [-(plus(n5, _237046) = succ(succ(succ(succ(succ(_237046))))))], (756 ^ _206485) ^ [_237137] : [-(minus(_237137, n1) = pred(_237137))], (758 ^ _206485) ^ [_237220] : [-(pred(succ(_237220)) = _237220)], (760 ^ _206485) ^ [_237302] : [-(succ(pred(_237302)) = _237302)], (762 ^ _206485) ^ [_237442, _237444] : [leq(succ(_237444), succ(_237442)), -(leq(_237444, _237442))], (768 ^ _206485) ^ [_237612, _237614] : [leq(_237614, _237612), -(leq(succ(_237614), succ(_237612)))], (774 ^ _206485) ^ [_237832, _237834] : [leq(succ(_237834), _237832), -(gt(_237832, _237834))], (780 ^ _206485) ^ [_238046, _238048] : [leq(minus(_238048, _238046), _238048), -(leq(n0, _238046))], (786 ^ _206485) ^ [_238275, _238277, _238279, _238281] : [-(a_select3(tptp_update3(_238281, _238279, _238277, _238275), _238279, _238277) = _238275)], (788 ^ _206485) ^ [_238467, _238469, _238471, _238473, _238475, _238477, _238479] : [-(a_select3(tptp_update3(_238471, _238479, _238477, _238467), _238475, _238473) = _238469), -(_238479 = _238475), _238477 = _238473, a_select3(_238471, _238475, _238473) = _238469], (802 ^ _206485) ^ [_239010, _239012, _239014, _239016, _239018, _239020] : [-(a_select3(tptp_update3(_239012, _239016, _239014, _239010), _239020, _239018) = _239010), 807 ^ _206485 : [(808 ^ _206485) ^ [] : [-(leq(n0, 805 ^ [_239010, _239012, _239014, _239016, _239018, _239020]))], (810 ^ _206485) ^ [] : [-(leq(n0, 806 ^ [_239010, _239012, _239014, _239016, _239018, _239020]))], (812 ^ _206485) ^ [] : [-(leq(805 ^ [_239010, _239012, _239014, _239016, _239018, _239020], _239016))], (814 ^ _206485) ^ [] : [-(leq(806 ^ [_239010, _239012, _239014, _239016, _239018, _239020], _239014))], (816 ^ _206485) ^ [] : [a_select3(_239012, 805 ^ [_239010, _239012, _239014, _239016, _239018, _239020], 806 ^ [_239010, _239012, _239014, _239016, _239018, _239020]) = _239010]], leq(n0, _239020), leq(_239020, _239016), leq(n0, _239018), leq(_239018, _239014)], (834 ^ _206485) ^ [_240352, _240354, _240356] : [-(a_select2(tptp_update2(_240356, _240354, _240352), _240354) = _240352)], (836 ^ _206485) ^ [_240512, _240514, _240516, _240518, _240520] : [-(a_select2(tptp_update2(_240516, _240520, _240512), _240518) = _240514), -(_240520 = _240518), a_select2(_240516, _240518) = _240514], (865 ^ _206485) ^ [] : [-(true)], (867 ^ _206485) ^ [] : [def = use], (846 ^ _206485) ^ [_240892, _240894, _240896, _240898] : [-(a_select2(tptp_update2(_240894, _240896, _240892), _240898) = _240892), 850 ^ _206485 : [(851 ^ _206485) ^ [] : [-(leq(n0, 849 ^ [_240892, _240894, _240896, _240898]))], (853 ^ _206485) ^ [] : [-(leq(849 ^ [_240892, _240894, _240896, _240898], _240896))], (855 ^ _206485) ^ [] : [a_select2(_240894, 849 ^ [_240892, _240894, _240896, _240898]) = _240892]], leq(n0, _240898), leq(_240898, _240896)]], input).
% 0.32/1.37 ncf('1',plain,[a_select2(rho_init, pv68) = init],start(1137 ^ 0)).
% 0.32/1.37 ncf('1.1',plain,[-(a_select2(rho_init, pv68) = init), leq(n0, pv68), leq(pv68, n4)],extension(1117 ^ 1,bind([[_248563], [pv68]]))).
% 0.32/1.37 ncf('1.1.1',plain,[-(leq(n0, pv68))],extension(1055 ^ 2)).
% 0.32/1.37 ncf('1.1.2',plain,[-(leq(pv68, n4))],extension(1057 ^ 2)).
% 0.32/1.37 %-----------------------------------------------------
% 0.32/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------