%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV165+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n012.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:05 EDT 2023
% Result : Theorem 17.93s 18.01s
% Output : Proof 17.93s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWV165+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.14/0.35 % Computer : n012.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:27:46 EDT 2023
% 0.14/0.35 % CPUTime :
% 17.93/18.01
% 17.93/18.01 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 17.93/18.01 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.93/18.01 %-----------------------------------------------------
% 17.93/18.01 ncf(matrix, plain, [(1042 ^ _196559) ^ [] : [-(leq(n0, 1040 ^ []))], (1044 ^ _196559) ^ [] : [-(leq(1040 ^ [], tptp_minus_1))], (1046 ^ _196559) ^ [] : [uninit = init], (2 ^ _196559) ^ [_196703] : [-(_196703 = _196703)], (4 ^ _196559) ^ [_196810, _196812] : [_196812 = _196810, -(_196810 = _196812)], (10 ^ _196559) ^ [_197014, _197016, _197018] : [-(_197018 = _197014), _197018 = _197016, _197016 = _197014], (20 ^ _196559) ^ [_197355, _197357, _197359, _197361] : [-(lt(_197359, _197355)), lt(_197361, _197357), _197361 = _197359, _197357 = _197355], (34 ^ _196559) ^ [_197799, _197801, _197803, _197805] : [-(geq(_197803, _197799)), geq(_197805, _197801), _197805 = _197803, _197801 = _197799], (48 ^ _196559) ^ [_198243, _198245, _198247, _198249] : [-(gt(_198247, _198243)), gt(_198249, _198245), _198249 = _198247, _198245 = _198243], (62 ^ _196559) ^ [_198667, _198669, _198671, _198673] : [-(leq(_198671, _198667)), leq(_198673, _198669), _198673 = _198671, _198669 = _198667], (76 ^ _196559) ^ [_199123, _199125, _199127, _199129] : [-(uniform_int_rnd(_199129, _199125) = uniform_int_rnd(_199127, _199123)), _199129 = _199127, _199125 = _199123], (86 ^ _196559) ^ [_199482, _199484, _199486, _199488] : [-(tptp_const_array1(_199488, _199484) = tptp_const_array1(_199486, _199482)), _199488 = _199486, _199484 = _199482], (96 ^ _196559) ^ [_199869, _199871, _199873, _199875, _199877, _199879] : [-(tptp_const_array2(_199879, _199875, _199871) = tptp_const_array2(_199877, _199873, _199869)), _199879 = _199877, _199875 = _199873, _199871 = _199869], (110 ^ _196559) ^ [_200357, _200359, _200361, _200363] : [-(dim(_200363, _200359) = dim(_200361, _200357)), _200363 = _200361, _200359 = _200357], (120 ^ _196559) ^ [_200688, _200690] : [_200690 = _200688, -(inv(_200690) = inv(_200688))], (126 ^ _196559) ^ [_200934, _200936, _200938, _200940] : [-(tptp_msub(_200940, _200936) = tptp_msub(_200938, _200934)), _200940 = _200938, _200936 = _200934], (136 ^ _196559) ^ [_201293, _201295, _201297, _201299] : [-(tptp_madd(_201299, _201295) = tptp_madd(_201297, _201293)), _201299 = _201297, _201295 = _201293], (146 ^ _196559) ^ [_201652, _201654, _201656, _201658] : [-(tptp_mmul(_201658, _201654) = tptp_mmul(_201656, _201652)), _201658 = _201656, _201654 = _201652], (156 ^ _196559) ^ [_201983, _201985] : [_201985 = _201983, -(trans(_201985) = trans(_201983))], (162 ^ _196559) ^ [_202257, _202259, _202261, _202263, _202265, _202267] : [-(sum(_202267, _202263, _202259) = sum(_202265, _202261, _202257)), _202267 = _202265, _202263 = _202261, _202259 = _202257], (176 ^ _196559) ^ [_202745, _202747, _202749, _202751] : [-(plus(_202751, _202747) = plus(_202749, _202745)), _202751 = _202749, _202747 = _202745], (186 ^ _196559) ^ [_203076, _203078] : [_203078 = _203076, -(pred(_203078) = pred(_203076))], (192 ^ _196559) ^ [_203322, _203324, _203326, _203328] : [-(minus(_203328, _203324) = minus(_203326, _203322)), _203328 = _203326, _203324 = _203322], (202 ^ _196559) ^ [_203709, _203711, _203713, _203715, _203717, _203719] : [-(a_select3(_203719, _203715, _203711) = a_select3(_203717, _203713, _203709)), _203719 = _203717, _203715 = _203713, _203711 = _203709], (216 ^ _196559) ^ [_204253, _204255, _204257, _204259, _204261, _204263, _204265, _204267] : [-(tptp_update3(_204267, _204263, _204259, _204255) = tptp_update3(_204265, _204261, _204257, _204253)), _204267 = _204265, _204263 = _204261, _204259 = _204257, _204255 = _204253], (234 ^ _196559) ^ [_204886, _204888, _204890, _204892] : [-(a_select2(_204892, _204888) = a_select2(_204890, _204886)), _204892 = _204890, _204888 = _204886], (258 ^ _196559) ^ [_205713, _205715] : [_205715 = _205713, -(succ(_205715) = succ(_205713))], (244 ^ _196559) ^ [_205273, _205275, _205277, _205279, _205281, _205283] : [-(tptp_update2(_205283, _205279, _205275) = tptp_update2(_205281, _205277, _205273)), _205283 = _205281, _205279 = _205277, _205275 = _205273], (869 ^ _196559) ^ [] : [-(gt(n5, n4))], (871 ^ _196559) ^ [] : [-(gt(n4, tptp_minus_1))], (873 ^ _196559) ^ [] : [-(gt(n5, tptp_minus_1))], (875 ^ _196559) ^ [] : [-(gt(n0, tptp_minus_1))], (877 ^ _196559) ^ [] : [-(gt(n1, tptp_minus_1))], (879 ^ _196559) ^ [] : [-(gt(n2, tptp_minus_1))], (881 ^ _196559) ^ [] : [-(gt(n3, tptp_minus_1))], (883 ^ _196559) ^ [] : [-(gt(n4, n0))], (885 ^ _196559) ^ [] : [-(gt(n5, n0))], (887 ^ _196559) ^ [] : [-(gt(n1, n0))], (889 ^ _196559) ^ [] : [-(gt(n2, n0))], (891 ^ _196559) ^ [] : [-(gt(n3, n0))], (893 ^ _196559) ^ [] : [-(gt(n4, n1))], (895 ^ _196559) ^ [] : [-(gt(n5, n1))], (897 ^ _196559) ^ [] : [-(gt(n2, n1))], (899 ^ _196559) ^ [] : [-(gt(n3, n1))], (901 ^ _196559) ^ [] : [-(gt(n4, n2))], (903 ^ _196559) ^ [] : [-(gt(n5, n2))], (905 ^ _196559) ^ [] : [-(gt(n3, n2))], (907 ^ _196559) ^ [] : [-(gt(n4, n3))], (909 ^ _196559) ^ [] : [-(gt(n5, n3))], (911 ^ _196559) ^ [_233069] : [leq(n0, _233069), leq(_233069, n4), -(_233069 = n0), -(_233069 = n1), -(_233069 = n2), -(_233069 = n3), -(_233069 = n4)], (937 ^ _196559) ^ [_233690] : [leq(n0, _233690), leq(_233690, n5), -(_233690 = n0), -(_233690 = n1), -(_233690 = n2), -(_233690 = n3), -(_233690 = n4), -(_233690 = n5)], (967 ^ _196559) ^ [_234397] : [-(_234397 = n0), leq(n0, _234397), leq(_234397, n0)], (977 ^ _196559) ^ [_234672] : [leq(n0, _234672), leq(_234672, n1), -(_234672 = n0), -(_234672 = n1)], (991 ^ _196559) ^ [_235035] : [leq(n0, _235035), leq(_235035, n2), -(_235035 = n0), -(_235035 = n1), -(_235035 = n2)], (1031 ^ _196559) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (1033 ^ _196559) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (1035 ^ _196559) ^ [] : [-(succ(n0) = n1)], (1037 ^ _196559) ^ [] : [-(succ(succ(n0)) = n2)], (1039 ^ _196559) ^ [] : [-(succ(succ(succ(n0))) = n3)], (1009 ^ _196559) ^ [_235484] : [leq(n0, _235484), leq(_235484, n3), -(_235484 = n0), -(_235484 = n1), -(_235484 = n2), -(_235484 = n3)], (264 ^ _196559) ^ [_206031, _206033] : [-(gt(_206033, _206031)), -(gt(_206031, _206033)), -(_206033 = _206031)], (274 ^ _196559) ^ [_206346, _206348, _206350] : [-(gt(_206350, _206346)), gt(_206350, _206348), gt(_206348, _206346)], (284 ^ _196559) ^ [_206625] : [gt(_206625, _206625)], (286 ^ _196559) ^ [_206703] : [-(leq(_206703, _206703))], (288 ^ _196559) ^ [_206824, _206826, _206828] : [-(leq(_206828, _206824)), leq(_206828, _206826), leq(_206826, _206824)], (298 ^ _196559) ^ [_207162, _207164] : [lt(_207164, _207162), -(gt(_207162, _207164))], (304 ^ _196559) ^ [_207324, _207326] : [gt(_207324, _207326), -(lt(_207326, _207324))], (310 ^ _196559) ^ [_207565, _207567] : [geq(_207567, _207565), -(leq(_207565, _207567))], (316 ^ _196559) ^ [_207727, _207729] : [leq(_207727, _207729), -(geq(_207729, _207727))], (322 ^ _196559) ^ [_207939, _207941] : [gt(_207939, _207941), -(leq(_207941, _207939))], (328 ^ _196559) ^ [_208149, _208151] : [-(gt(_208149, _208151)), leq(_208151, _208149), -(_208151 = _208149)], (338 ^ _196559) ^ [_208480, _208482] : [leq(_208482, pred(_208480)), -(gt(_208480, _208482))], (344 ^ _196559) ^ [_208646, _208648] : [gt(_208646, _208648), -(leq(_208648, pred(_208646)))], (350 ^ _196559) ^ [_208833] : [-(gt(succ(_208833), _208833))], (352 ^ _196559) ^ [_208942, _208944] : [leq(_208944, _208942), -(leq(_208944, succ(_208942)))], (358 ^ _196559) ^ [_209185, _209187] : [leq(_209187, _209185), -(gt(succ(_209185), _209187))], (364 ^ _196559) ^ [_209351, _209353] : [gt(succ(_209351), _209353), -(leq(_209353, _209351))], (370 ^ _196559) ^ [_209567, _209569] : [leq(n0, _209569), -(leq(uniform_int_rnd(_209567, _209569), _209569))], (376 ^ _196559) ^ [_209783, _209785] : [leq(n0, _209785), -(leq(n0, uniform_int_rnd(_209783, _209785)))], (382 ^ _196559) ^ [_210027, _210029, _210031, _210033] : [-(a_select2(tptp_const_array1(dim(_210031, _210029), _210027), _210033) = _210027), leq(_210031, _210033), leq(_210033, _210029)], (392 ^ _196559) ^ [_210434, _210436, _210438, _210440, _210442, _210444, _210446] : [-(a_select3(tptp_const_array2(dim(_210444, _210442), dim(_210438, _210436), _210434), _210446, _210440) = _210434), leq(_210444, _210446), leq(_210446, _210442), leq(_210438, _210440), leq(_210440, _210436)], (410 ^ _196559) ^ [_211029, _211031] : [413 ^ _196559 : [(414 ^ _196559) ^ [] : [-(leq(n0, 411 ^ [_211029, _211031]))], (416 ^ _196559) ^ [] : [-(leq(411 ^ [_211029, _211031], _211029))], (418 ^ _196559) ^ [] : [-(leq(n0, 412 ^ [_211029, _211031]))], (420 ^ _196559) ^ [] : [-(leq(412 ^ [_211029, _211031], _211029))], (422 ^ _196559) ^ [] : [a_select3(_211031, 411 ^ [_211029, _211031], 412 ^ [_211029, _211031]) = a_select3(_211031, 412 ^ [_211029, _211031], 411 ^ [_211029, _211031])]], 423 ^ _196559 : [(424 ^ _196559) ^ [_211786, _211788] : [-(a_select3(trans(_211031), _211788, _211786) = a_select3(trans(_211031), _211786, _211788)), leq(n0, _211788), leq(_211788, _211029), leq(n0, _211786), leq(_211786, _211029)]]], (442 ^ _196559) ^ [_212333, _212335] : [445 ^ _196559 : [(446 ^ _196559) ^ [] : [-(leq(n0, 443 ^ [_212333, _212335]))], (448 ^ _196559) ^ [] : [-(leq(443 ^ [_212333, _212335], _212333))], (450 ^ _196559) ^ [] : [-(leq(n0, 444 ^ [_212333, _212335]))], (452 ^ _196559) ^ [] : [-(leq(444 ^ [_212333, _212335], _212333))], (454 ^ _196559) ^ [] : [a_select3(_212335, 443 ^ [_212333, _212335], 444 ^ [_212333, _212335]) = a_select3(_212335, 444 ^ [_212333, _212335], 443 ^ [_212333, _212335])]], 455 ^ _196559 : [(456 ^ _196559) ^ [_213090, _213092] : [-(a_select3(inv(_212335), _213092, _213090) = a_select3(inv(_212335), _213090, _213092)), leq(n0, _213092), leq(_213092, _212333), leq(n0, _213090), leq(_213090, _212333)]]], (474 ^ _196559) ^ [_213637, _213639] : [477 ^ _196559 : [(478 ^ _196559) ^ [] : [-(leq(n0, 475 ^ [_213637, _213639]))], (480 ^ _196559) ^ [] : [-(leq(475 ^ [_213637, _213639], _213637))], (482 ^ _196559) ^ [] : [-(leq(n0, 476 ^ [_213637, _213639]))], (484 ^ _196559) ^ [] : [-(leq(476 ^ [_213637, _213639], _213637))], (486 ^ _196559) ^ [] : [a_select3(_213639, 475 ^ [_213637, _213639], 476 ^ [_213637, _213639]) = a_select3(_213639, 476 ^ [_213637, _213639], 475 ^ [_213637, _213639])]], 487 ^ _196559 : [(488 ^ _196559) ^ [_214450, _214452, _214454, _214456] : [-(a_select3(tptp_update3(_213639, _214452, _214452, _214450), _214456, _214454) = a_select3(tptp_update3(_213639, _214452, _214452, _214450), _214454, _214456)), leq(n0, _214456), leq(_214456, _213637), leq(n0, _214454), leq(_214454, _213637), leq(n0, _214452), leq(_214452, _213637)]]], (514 ^ _196559) ^ [_215269, _215271, _215273] : [519 ^ _196559 : [(520 ^ _196559) ^ [] : [-(leq(n0, 517 ^ [_215269, _215271, _215273]))], (522 ^ _196559) ^ [] : [-(leq(517 ^ [_215269, _215271, _215273], _215269))], (524 ^ _196559) ^ [] : [-(leq(n0, 518 ^ [_215269, _215271, _215273]))], (526 ^ _196559) ^ [] : [-(leq(518 ^ [_215269, _215271, _215273], _215269))], (528 ^ _196559) ^ [] : [a_select3(_215273, 517 ^ [_215269, _215271, _215273], 518 ^ [_215269, _215271, _215273]) = a_select3(_215273, 518 ^ [_215269, _215271, _215273], 517 ^ [_215269, _215271, _215273])]], 531 ^ _196559 : [(532 ^ _196559) ^ [] : [-(leq(n0, 529 ^ [_215269, _215271, _215273]))], (534 ^ _196559) ^ [] : [-(leq(529 ^ [_215269, _215271, _215273], _215269))], (536 ^ _196559) ^ [] : [-(leq(n0, 530 ^ [_215269, _215271, _215273]))], (538 ^ _196559) ^ [] : [-(leq(530 ^ [_215269, _215271, _215273], _215269))], (540 ^ _196559) ^ [] : [a_select3(_215271, 529 ^ [_215269, _215271, _215273], 530 ^ [_215269, _215271, _215273]) = a_select3(_215271, 530 ^ [_215269, _215271, _215273], 529 ^ [_215269, _215271, _215273])]], 541 ^ _196559 : [(542 ^ _196559) ^ [_216778, _216780] : [-(a_select3(tptp_madd(_215273, _215271), _216780, _216778) = a_select3(tptp_madd(_215273, _215271), _216778, _216780)), leq(n0, _216780), leq(_216780, _215269), leq(n0, _216778), leq(_216778, _215269)]]], (560 ^ _196559) ^ [_217364, _217366, _217368] : [565 ^ _196559 : [(566 ^ _196559) ^ [] : [-(leq(n0, 563 ^ [_217364, _217366, _217368]))], (568 ^ _196559) ^ [] : [-(leq(563 ^ [_217364, _217366, _217368], _217364))], (570 ^ _196559) ^ [] : [-(leq(n0, 564 ^ [_217364, _217366, _217368]))], (572 ^ _196559) ^ [] : [-(leq(564 ^ [_217364, _217366, _217368], _217364))], (574 ^ _196559) ^ [] : [a_select3(_217368, 563 ^ [_217364, _217366, _217368], 564 ^ [_217364, _217366, _217368]) = a_select3(_217368, 564 ^ [_217364, _217366, _217368], 563 ^ [_217364, _217366, _217368])]], 577 ^ _196559 : [(578 ^ _196559) ^ [] : [-(leq(n0, 575 ^ [_217364, _217366, _217368]))], (580 ^ _196559) ^ [] : [-(leq(575 ^ [_217364, _217366, _217368], _217364))], (582 ^ _196559) ^ [] : [-(leq(n0, 576 ^ [_217364, _217366, _217368]))], (584 ^ _196559) ^ [] : [-(leq(576 ^ [_217364, _217366, _217368], _217364))], (586 ^ _196559) ^ [] : [a_select3(_217366, 575 ^ [_217364, _217366, _217368], 576 ^ [_217364, _217366, _217368]) = a_select3(_217366, 576 ^ [_217364, _217366, _217368], 575 ^ [_217364, _217366, _217368])]], 587 ^ _196559 : [(588 ^ _196559) ^ [_218873, _218875] : [-(a_select3(tptp_msub(_217368, _217366), _218875, _218873) = a_select3(tptp_msub(_217368, _217366), _218873, _218875)), leq(n0, _218875), leq(_218875, _217364), leq(n0, _218873), leq(_218873, _217364)]]], (606 ^ _196559) ^ [_219459, _219461, _219463] : [609 ^ _196559 : [(610 ^ _196559) ^ [] : [-(leq(n0, 607 ^ [_219459, _219461, _219463]))], (612 ^ _196559) ^ [] : [-(leq(607 ^ [_219459, _219461, _219463], _219459))], (614 ^ _196559) ^ [] : [-(leq(n0, 608 ^ [_219459, _219461, _219463]))], (616 ^ _196559) ^ [] : [-(leq(608 ^ [_219459, _219461, _219463], _219459))], (618 ^ _196559) ^ [] : [a_select3(_219461, 607 ^ [_219459, _219461, _219463], 608 ^ [_219459, _219461, _219463]) = a_select3(_219461, 608 ^ [_219459, _219461, _219463], 607 ^ [_219459, _219461, _219463])]], 619 ^ _196559 : [(620 ^ _196559) ^ [_220272, _220274] : [-(a_select3(tptp_mmul(_219463, tptp_mmul(_219461, trans(_219463))), _220274, _220272) = a_select3(tptp_mmul(_219463, tptp_mmul(_219461, trans(_219463))), _220272, _220274)), leq(n0, _220274), leq(_220274, _219459), leq(n0, _220272), leq(_220272, _219459)]]], (638 ^ _196559) ^ [_220891, _220893, _220895, _220897] : [641 ^ _196559 : [(642 ^ _196559) ^ [] : [-(leq(n0, 639 ^ [_220891, _220893, _220895, _220897]))], (644 ^ _196559) ^ [] : [-(leq(639 ^ [_220891, _220893, _220895, _220897], _220891))], (646 ^ _196559) ^ [] : [-(leq(n0, 640 ^ [_220891, _220893, _220895, _220897]))], (648 ^ _196559) ^ [] : [-(leq(640 ^ [_220891, _220893, _220895, _220897], _220891))], (650 ^ _196559) ^ [] : [a_select3(_220895, 639 ^ [_220891, _220893, _220895, _220897], 640 ^ [_220891, _220893, _220895, _220897]) = a_select3(_220895, 640 ^ [_220891, _220893, _220895, _220897], 639 ^ [_220891, _220893, _220895, _220897])]], 651 ^ _196559 : [(652 ^ _196559) ^ [_221748, _221750] : [-(a_select3(tptp_mmul(_220897, tptp_mmul(_220895, trans(_220897))), _221750, _221748) = a_select3(tptp_mmul(_220897, tptp_mmul(_220895, trans(_220897))), _221748, _221750)), leq(n0, _221750), leq(_221750, _220893), leq(n0, _221748), leq(_221748, _220893)]]], (670 ^ _196559) ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457] : [675 ^ _196559 : [(676 ^ _196559) ^ [] : [-(leq(n0, 673 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457]))], (678 ^ _196559) ^ [] : [-(leq(673 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457], _222443))], (680 ^ _196559) ^ [] : [-(leq(n0, 674 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457]))], (682 ^ _196559) ^ [] : [-(leq(674 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457], _222443))], (684 ^ _196559) ^ [] : [a_select3(_222451, 673 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457], 674 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457]) = a_select3(_222451, 674 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457], 673 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457])]], 689 ^ _196559 : [(690 ^ _196559) ^ [] : [-(leq(n0, 687 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457]))], (692 ^ _196559) ^ [] : [-(leq(687 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457], _222445))], (694 ^ _196559) ^ [] : [-(leq(n0, 688 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457]))], (696 ^ _196559) ^ [] : [-(leq(688 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457], _222445))], (698 ^ _196559) ^ [] : [a_select3(_222457, 687 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457], 688 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457]) = a_select3(_222457, 688 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457], 687 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457])]], 701 ^ _196559 : [(702 ^ _196559) ^ [] : [-(leq(n0, 699 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457]))], (704 ^ _196559) ^ [] : [-(leq(699 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457], _222445))], (706 ^ _196559) ^ [] : [-(leq(n0, 700 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457]))], (708 ^ _196559) ^ [] : [-(leq(700 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457], _222445))], (710 ^ _196559) ^ [] : [a_select3(_222447, 699 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457], 700 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457]) = a_select3(_222447, 700 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457], 699 ^ [_222443, _222445, _222447, _222449, _222451, _222453, _222455, _222457])]], 711 ^ _196559 : [(712 ^ _196559) ^ [_225371, _225373] : [-(a_select3(tptp_madd(_222457, tptp_mmul(_222455, tptp_mmul(tptp_madd(tptp_mmul(_222453, tptp_mmul(_222451, trans(_222453))), tptp_mmul(_222449, tptp_mmul(_222447, trans(_222449)))), trans(_222455)))), _225373, _225371) = a_select3(tptp_madd(_222457, tptp_mmul(_222455, tptp_mmul(tptp_madd(tptp_mmul(_222453, tptp_mmul(_222451, trans(_222453))), tptp_mmul(_222449, tptp_mmul(_222447, trans(_222449)))), trans(_222455)))), _225371, _225373)), leq(n0, _225373), leq(_225373, _222445), leq(n0, _225371), leq(_225371, _222445)]]], (730 ^ _196559) ^ [_226124] : [-(sum(n0, tptp_minus_1, _226124) = n0)], (732 ^ _196559) ^ [_226206] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _226206))], (734 ^ _196559) ^ [] : [-(succ(tptp_minus_1) = n0)], (736 ^ _196559) ^ [_226341] : [-(plus(_226341, n1) = succ(_226341))], (738 ^ _196559) ^ [_226424] : [-(plus(n1, _226424) = succ(_226424))], (740 ^ _196559) ^ [_226507] : [-(plus(_226507, n2) = succ(succ(_226507)))], (742 ^ _196559) ^ [_226592] : [-(plus(n2, _226592) = succ(succ(_226592)))], (744 ^ _196559) ^ [_226677] : [-(plus(_226677, n3) = succ(succ(succ(_226677))))], (746 ^ _196559) ^ [_226764] : [-(plus(n3, _226764) = succ(succ(succ(_226764))))], (748 ^ _196559) ^ [_226851] : [-(plus(_226851, n4) = succ(succ(succ(succ(_226851)))))], (750 ^ _196559) ^ [_226940] : [-(plus(n4, _226940) = succ(succ(succ(succ(_226940)))))], (752 ^ _196559) ^ [_227029] : [-(plus(_227029, n5) = succ(succ(succ(succ(succ(_227029))))))], (754 ^ _196559) ^ [_227120] : [-(plus(n5, _227120) = succ(succ(succ(succ(succ(_227120))))))], (756 ^ _196559) ^ [_227211] : [-(minus(_227211, n1) = pred(_227211))], (758 ^ _196559) ^ [_227294] : [-(pred(succ(_227294)) = _227294)], (760 ^ _196559) ^ [_227376] : [-(succ(pred(_227376)) = _227376)], (762 ^ _196559) ^ [_227516, _227518] : [leq(succ(_227518), succ(_227516)), -(leq(_227518, _227516))], (768 ^ _196559) ^ [_227686, _227688] : [leq(_227688, _227686), -(leq(succ(_227688), succ(_227686)))], (774 ^ _196559) ^ [_227906, _227908] : [leq(succ(_227908), _227906), -(gt(_227906, _227908))], (780 ^ _196559) ^ [_228120, _228122] : [leq(minus(_228122, _228120), _228122), -(leq(n0, _228120))], (786 ^ _196559) ^ [_228349, _228351, _228353, _228355] : [-(a_select3(tptp_update3(_228355, _228353, _228351, _228349), _228353, _228351) = _228349)], (788 ^ _196559) ^ [_228541, _228543, _228545, _228547, _228549, _228551, _228553] : [-(a_select3(tptp_update3(_228545, _228553, _228551, _228541), _228549, _228547) = _228543), -(_228553 = _228549), _228551 = _228547, a_select3(_228545, _228549, _228547) = _228543], (802 ^ _196559) ^ [_229084, _229086, _229088, _229090, _229092, _229094] : [-(a_select3(tptp_update3(_229086, _229090, _229088, _229084), _229094, _229092) = _229084), 807 ^ _196559 : [(808 ^ _196559) ^ [] : [-(leq(n0, 805 ^ [_229084, _229086, _229088, _229090, _229092, _229094]))], (810 ^ _196559) ^ [] : [-(leq(n0, 806 ^ [_229084, _229086, _229088, _229090, _229092, _229094]))], (812 ^ _196559) ^ [] : [-(leq(805 ^ [_229084, _229086, _229088, _229090, _229092, _229094], _229090))], (814 ^ _196559) ^ [] : [-(leq(806 ^ [_229084, _229086, _229088, _229090, _229092, _229094], _229088))], (816 ^ _196559) ^ [] : [a_select3(_229086, 805 ^ [_229084, _229086, _229088, _229090, _229092, _229094], 806 ^ [_229084, _229086, _229088, _229090, _229092, _229094]) = _229084]], leq(n0, _229094), leq(_229094, _229090), leq(n0, _229092), leq(_229092, _229088)], (834 ^ _196559) ^ [_230426, _230428, _230430] : [-(a_select2(tptp_update2(_230430, _230428, _230426), _230428) = _230426)], (836 ^ _196559) ^ [_230586, _230588, _230590, _230592, _230594] : [-(a_select2(tptp_update2(_230590, _230594, _230586), _230592) = _230588), -(_230594 = _230592), a_select2(_230590, _230592) = _230588], (865 ^ _196559) ^ [] : [-(true)], (867 ^ _196559) ^ [] : [def = use], (846 ^ _196559) ^ [_230966, _230968, _230970, _230972] : [-(a_select2(tptp_update2(_230968, _230970, _230966), _230972) = _230966), 850 ^ _196559 : [(851 ^ _196559) ^ [] : [-(leq(n0, 849 ^ [_230966, _230968, _230970, _230972]))], (853 ^ _196559) ^ [] : [-(leq(849 ^ [_230966, _230968, _230970, _230972], _230970))], (855 ^ _196559) ^ [] : [a_select2(_230968, 849 ^ [_230966, _230968, _230970, _230972]) = _230966]], leq(n0, _230972), leq(_230972, _230970)]], input).
% 17.93/18.01 ncf('1',plain,[gt(n0, n0)],start(284 ^ 0,bind([[_206625], [n0]]))).
% 17.93/18.01 ncf('1.1',plain,[-(gt(n0, n0)), leq(n0, pred(n0))],extension(338 ^ 1,bind([[_208480, _208482], [n0, n0]]))).
% 17.93/18.01 ncf('1.1.1',plain,[-(leq(n0, pred(n0))), leq(n0, 1040 ^ []), leq(1040 ^ [], pred(n0))],extension(288 ^ 2,bind([[_206824, _206826, _206828], [pred(n0), 1040 ^ [], n0]]))).
% 17.93/18.01 ncf('1.1.1.1',plain,[-(leq(n0, 1040 ^ []))],extension(1042 ^ 3)).
% 17.93/18.01 ncf('1.1.1.2',plain,[-(leq(1040 ^ [], pred(n0))), leq(1040 ^ [], tptp_minus_1), leq(tptp_minus_1, pred(n0))],extension(288 ^ 3,bind([[_206824, _206826, _206828], [pred(n0), tptp_minus_1, 1040 ^ []]]))).
% 17.93/18.01 ncf('1.1.1.2.1',plain,[-(leq(1040 ^ [], tptp_minus_1))],extension(1044 ^ 4)).
% 17.93/18.01 ncf('1.1.1.2.2',plain,[-(leq(tptp_minus_1, pred(n0))), gt(n0, tptp_minus_1)],extension(344 ^ 4,bind([[_208646, _208648], [n0, tptp_minus_1]]))).
% 17.93/18.01 ncf('1.1.1.2.2.1',plain,[-(gt(n0, tptp_minus_1))],extension(875 ^ 5)).
% 17.93/18.01 %-----------------------------------------------------
% 17.93/18.01 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------