%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV227+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n008.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:12 EDT 2023
% Result : Theorem 0.36s 1.37s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SWV227+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n008.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:19:09 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.36/1.37
% 0.36/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.36/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 ncf(matrix, plain, [(1041 ^ _216280) ^ [_256211, _256213] : [-(a_select3(q_ds1_filter, _256213, _256211) = a_select3(q_ds1_filter, _256211, _256213)), leq(n0, _256213), leq(n0, _256211), leq(_256213, n5), leq(_256211, n5)], (1059 ^ _216280) ^ [_256684, _256686] : [-(a_select3(r_ds1_filter, _256686, _256684) = a_select3(r_ds1_filter, _256684, _256686)), leq(n0, _256686), leq(n0, _256684), leq(_256686, n2), leq(_256684, n2)], (1079 ^ _216280) ^ [] : [-(leq(n0, 1076 ^ []))], (1081 ^ _216280) ^ [] : [-(leq(n0, 1077 ^ []))], (1083 ^ _216280) ^ [] : [-(leq(1076 ^ [], n5))], (1085 ^ _216280) ^ [] : [-(leq(1077 ^ [], n5))], (1221 ^ _216280) ^ [] : [a_select2(xinit_noise, n4) = n0], (1087 ^ _216280) ^ [] : [n0 = 1076 ^ [], n3 = 1077 ^ []], (1093 ^ _216280) ^ [] : [n0 = 1076 ^ [], n4 = 1077 ^ []], (1099 ^ _216280) ^ [] : [n0 = 1076 ^ [], n5 = 1077 ^ []], (1105 ^ _216280) ^ [] : [n0 = 1077 ^ [], n5 = 1076 ^ []], (1111 ^ _216280) ^ [] : [n1 = 1076 ^ [], n3 = 1077 ^ []], (1117 ^ _216280) ^ [] : [n1 = 1076 ^ [], n4 = 1077 ^ []], (1123 ^ _216280) ^ [] : [n1 = 1076 ^ [], n5 = 1077 ^ []], (1129 ^ _216280) ^ [] : [n1 = 1077 ^ [], n5 = 1076 ^ []], (1135 ^ _216280) ^ [] : [n2 = 1076 ^ [], n3 = 1077 ^ []], (1141 ^ _216280) ^ [] : [n2 = 1076 ^ [], n4 = 1077 ^ []], (1147 ^ _216280) ^ [] : [n2 = 1076 ^ [], n5 = 1077 ^ []], (1153 ^ _216280) ^ [] : [n2 = 1077 ^ [], n5 = 1076 ^ []], (1159 ^ _216280) ^ [] : [n3 = 1076 ^ [], n3 = 1077 ^ []], (1165 ^ _216280) ^ [] : [n3 = 1076 ^ [], n4 = 1077 ^ []], (1171 ^ _216280) ^ [] : [n3 = 1076 ^ [], n5 = 1077 ^ []], (1177 ^ _216280) ^ [] : [n3 = 1077 ^ [], n4 = 1076 ^ []], (1183 ^ _216280) ^ [] : [n3 = 1077 ^ [], n5 = 1076 ^ []], (1189 ^ _216280) ^ [] : [n4 = 1076 ^ [], n4 = 1077 ^ []], (1195 ^ _216280) ^ [] : [n4 = 1076 ^ [], n5 = 1077 ^ []], (1201 ^ _216280) ^ [] : [n4 = 1077 ^ [], n5 = 1076 ^ []], (1213 ^ _216280) ^ [] : [-(n2 = 1077 ^ [])], (1215 ^ _216280) ^ [] : [-(n4 = 1076 ^ [])], (1217 ^ _216280) ^ [] : [-(n4 = 1077 ^ [])], (1219 ^ _216280) ^ [] : [-(n5 = 1076 ^ [])], (1207 ^ _216280) ^ [] : [n5 = 1076 ^ [], n5 = 1077 ^ []], (2 ^ _216280) ^ [_216424] : [-(_216424 = _216424)], (4 ^ _216280) ^ [_216531, _216533] : [_216533 = _216531, -(_216531 = _216533)], (10 ^ _216280) ^ [_216735, _216737, _216739] : [-(_216739 = _216735), _216739 = _216737, _216737 = _216735], (20 ^ _216280) ^ [_217076, _217078, _217080, _217082] : [-(lt(_217080, _217076)), lt(_217082, _217078), _217082 = _217080, _217078 = _217076], (34 ^ _216280) ^ [_217520, _217522, _217524, _217526] : [-(geq(_217524, _217520)), geq(_217526, _217522), _217526 = _217524, _217522 = _217520], (48 ^ _216280) ^ [_217964, _217966, _217968, _217970] : [-(gt(_217968, _217964)), gt(_217970, _217966), _217970 = _217968, _217966 = _217964], (62 ^ _216280) ^ [_218388, _218390, _218392, _218394] : [-(leq(_218392, _218388)), leq(_218394, _218390), _218394 = _218392, _218390 = _218388], (76 ^ _216280) ^ [_218844, _218846, _218848, _218850] : [-(uniform_int_rnd(_218850, _218846) = uniform_int_rnd(_218848, _218844)), _218850 = _218848, _218846 = _218844], (86 ^ _216280) ^ [_219203, _219205, _219207, _219209] : [-(tptp_const_array1(_219209, _219205) = tptp_const_array1(_219207, _219203)), _219209 = _219207, _219205 = _219203], (96 ^ _216280) ^ [_219590, _219592, _219594, _219596, _219598, _219600] : [-(tptp_const_array2(_219600, _219596, _219592) = tptp_const_array2(_219598, _219594, _219590)), _219600 = _219598, _219596 = _219594, _219592 = _219590], (110 ^ _216280) ^ [_220078, _220080, _220082, _220084] : [-(dim(_220084, _220080) = dim(_220082, _220078)), _220084 = _220082, _220080 = _220078], (120 ^ _216280) ^ [_220409, _220411] : [_220411 = _220409, -(inv(_220411) = inv(_220409))], (126 ^ _216280) ^ [_220655, _220657, _220659, _220661] : [-(tptp_msub(_220661, _220657) = tptp_msub(_220659, _220655)), _220661 = _220659, _220657 = _220655], (136 ^ _216280) ^ [_221014, _221016, _221018, _221020] : [-(tptp_madd(_221020, _221016) = tptp_madd(_221018, _221014)), _221020 = _221018, _221016 = _221014], (146 ^ _216280) ^ [_221373, _221375, _221377, _221379] : [-(tptp_mmul(_221379, _221375) = tptp_mmul(_221377, _221373)), _221379 = _221377, _221375 = _221373], (156 ^ _216280) ^ [_221704, _221706] : [_221706 = _221704, -(trans(_221706) = trans(_221704))], (162 ^ _216280) ^ [_221978, _221980, _221982, _221984, _221986, _221988] : [-(sum(_221988, _221984, _221980) = sum(_221986, _221982, _221978)), _221988 = _221986, _221984 = _221982, _221980 = _221978], (176 ^ _216280) ^ [_222466, _222468, _222470, _222472] : [-(plus(_222472, _222468) = plus(_222470, _222466)), _222472 = _222470, _222468 = _222466], (186 ^ _216280) ^ [_222797, _222799] : [_222799 = _222797, -(pred(_222799) = pred(_222797))], (192 ^ _216280) ^ [_223043, _223045, _223047, _223049] : [-(minus(_223049, _223045) = minus(_223047, _223043)), _223049 = _223047, _223045 = _223043], (202 ^ _216280) ^ [_223458, _223460, _223462, _223464, _223466, _223468, _223470, _223472] : [-(tptp_update3(_223472, _223468, _223464, _223460) = tptp_update3(_223470, _223466, _223462, _223458)), _223472 = _223470, _223468 = _223466, _223464 = _223462, _223460 = _223458], (220 ^ _216280) ^ [_224119, _224121, _224123, _224125, _224127, _224129] : [-(tptp_update2(_224129, _224125, _224121) = tptp_update2(_224127, _224123, _224119)), _224129 = _224127, _224125 = _224123, _224121 = _224119], (234 ^ _216280) ^ [_224579, _224581] : [_224581 = _224579, -(succ(_224581) = succ(_224579))], (254 ^ _216280) ^ [_225321, _225323, _225325, _225327] : [-(a_select2(_225327, _225323) = a_select2(_225325, _225321)), _225327 = _225325, _225323 = _225321], (240 ^ _216280) ^ [_224853, _224855, _224857, _224859, _224861, _224863] : [-(a_select3(_224863, _224859, _224855) = a_select3(_224861, _224857, _224853)), _224863 = _224861, _224859 = _224857, _224855 = _224853], (869 ^ _216280) ^ [] : [-(gt(n5, n4))], (871 ^ _216280) ^ [] : [-(gt(n4, tptp_minus_1))], (873 ^ _216280) ^ [] : [-(gt(n5, tptp_minus_1))], (875 ^ _216280) ^ [] : [-(gt(n0, tptp_minus_1))], (877 ^ _216280) ^ [] : [-(gt(n1, tptp_minus_1))], (879 ^ _216280) ^ [] : [-(gt(n2, tptp_minus_1))], (881 ^ _216280) ^ [] : [-(gt(n3, tptp_minus_1))], (883 ^ _216280) ^ [] : [-(gt(n4, n0))], (885 ^ _216280) ^ [] : [-(gt(n5, n0))], (887 ^ _216280) ^ [] : [-(gt(n1, n0))], (889 ^ _216280) ^ [] : [-(gt(n2, n0))], (891 ^ _216280) ^ [] : [-(gt(n3, n0))], (893 ^ _216280) ^ [] : [-(gt(n4, n1))], (895 ^ _216280) ^ [] : [-(gt(n5, n1))], (897 ^ _216280) ^ [] : [-(gt(n2, n1))], (899 ^ _216280) ^ [] : [-(gt(n3, n1))], (901 ^ _216280) ^ [] : [-(gt(n4, n2))], (903 ^ _216280) ^ [] : [-(gt(n5, n2))], (905 ^ _216280) ^ [] : [-(gt(n3, n2))], (907 ^ _216280) ^ [] : [-(gt(n4, n3))], (909 ^ _216280) ^ [] : [-(gt(n5, n3))], (911 ^ _216280) ^ [_252790] : [leq(n0, _252790), leq(_252790, n4), -(_252790 = n0), -(_252790 = n1), -(_252790 = n2), -(_252790 = n3), -(_252790 = n4)], (937 ^ _216280) ^ [_253411] : [leq(n0, _253411), leq(_253411, n5), -(_253411 = n0), -(_253411 = n1), -(_253411 = n2), -(_253411 = n3), -(_253411 = n4), -(_253411 = n5)], (967 ^ _216280) ^ [_254118] : [-(_254118 = n0), leq(n0, _254118), leq(_254118, n0)], (977 ^ _216280) ^ [_254393] : [leq(n0, _254393), leq(_254393, n1), -(_254393 = n0), -(_254393 = n1)], (991 ^ _216280) ^ [_254756] : [leq(n0, _254756), leq(_254756, n2), -(_254756 = n0), -(_254756 = n1), -(_254756 = n2)], (1031 ^ _216280) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (1033 ^ _216280) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (1035 ^ _216280) ^ [] : [-(succ(n0) = n1)], (1037 ^ _216280) ^ [] : [-(succ(succ(n0)) = n2)], (1039 ^ _216280) ^ [] : [-(succ(succ(succ(n0))) = n3)], (1009 ^ _216280) ^ [_255205] : [leq(n0, _255205), leq(_255205, n3), -(_255205 = n0), -(_255205 = n1), -(_255205 = n2), -(_255205 = n3)], (264 ^ _216280) ^ [_225752, _225754] : [-(gt(_225754, _225752)), -(gt(_225752, _225754)), -(_225754 = _225752)], (274 ^ _216280) ^ [_226067, _226069, _226071] : [-(gt(_226071, _226067)), gt(_226071, _226069), gt(_226069, _226067)], (284 ^ _216280) ^ [_226346] : [gt(_226346, _226346)], (286 ^ _216280) ^ [_226424] : [-(leq(_226424, _226424))], (288 ^ _216280) ^ [_226545, _226547, _226549] : [-(leq(_226549, _226545)), leq(_226549, _226547), leq(_226547, _226545)], (298 ^ _216280) ^ [_226883, _226885] : [lt(_226885, _226883), -(gt(_226883, _226885))], (304 ^ _216280) ^ [_227045, _227047] : [gt(_227045, _227047), -(lt(_227047, _227045))], (310 ^ _216280) ^ [_227286, _227288] : [geq(_227288, _227286), -(leq(_227286, _227288))], (316 ^ _216280) ^ [_227448, _227450] : [leq(_227448, _227450), -(geq(_227450, _227448))], (322 ^ _216280) ^ [_227660, _227662] : [gt(_227660, _227662), -(leq(_227662, _227660))], (328 ^ _216280) ^ [_227870, _227872] : [-(gt(_227870, _227872)), leq(_227872, _227870), -(_227872 = _227870)], (338 ^ _216280) ^ [_228201, _228203] : [leq(_228203, pred(_228201)), -(gt(_228201, _228203))], (344 ^ _216280) ^ [_228367, _228369] : [gt(_228367, _228369), -(leq(_228369, pred(_228367)))], (350 ^ _216280) ^ [_228554] : [-(gt(succ(_228554), _228554))], (352 ^ _216280) ^ [_228663, _228665] : [leq(_228665, _228663), -(leq(_228665, succ(_228663)))], (358 ^ _216280) ^ [_228906, _228908] : [leq(_228908, _228906), -(gt(succ(_228906), _228908))], (364 ^ _216280) ^ [_229072, _229074] : [gt(succ(_229072), _229074), -(leq(_229074, _229072))], (370 ^ _216280) ^ [_229288, _229290] : [leq(n0, _229290), -(leq(uniform_int_rnd(_229288, _229290), _229290))], (376 ^ _216280) ^ [_229504, _229506] : [leq(n0, _229506), -(leq(n0, uniform_int_rnd(_229504, _229506)))], (382 ^ _216280) ^ [_229748, _229750, _229752, _229754] : [-(a_select2(tptp_const_array1(dim(_229752, _229750), _229748), _229754) = _229748), leq(_229752, _229754), leq(_229754, _229750)], (392 ^ _216280) ^ [_230155, _230157, _230159, _230161, _230163, _230165, _230167] : [-(a_select3(tptp_const_array2(dim(_230165, _230163), dim(_230159, _230157), _230155), _230167, _230161) = _230155), leq(_230165, _230167), leq(_230167, _230163), leq(_230159, _230161), leq(_230161, _230157)], (410 ^ _216280) ^ [_230750, _230752] : [413 ^ _216280 : [(414 ^ _216280) ^ [] : [-(leq(n0, 411 ^ [_230750, _230752]))], (416 ^ _216280) ^ [] : [-(leq(411 ^ [_230750, _230752], _230750))], (418 ^ _216280) ^ [] : [-(leq(n0, 412 ^ [_230750, _230752]))], (420 ^ _216280) ^ [] : [-(leq(412 ^ [_230750, _230752], _230750))], (422 ^ _216280) ^ [] : [a_select3(_230752, 411 ^ [_230750, _230752], 412 ^ [_230750, _230752]) = a_select3(_230752, 412 ^ [_230750, _230752], 411 ^ [_230750, _230752])]], 423 ^ _216280 : [(424 ^ _216280) ^ [_231507, _231509] : [-(a_select3(trans(_230752), _231509, _231507) = a_select3(trans(_230752), _231507, _231509)), leq(n0, _231509), leq(_231509, _230750), leq(n0, _231507), leq(_231507, _230750)]]], (442 ^ _216280) ^ [_232054, _232056] : [445 ^ _216280 : [(446 ^ _216280) ^ [] : [-(leq(n0, 443 ^ [_232054, _232056]))], (448 ^ _216280) ^ [] : [-(leq(443 ^ [_232054, _232056], _232054))], (450 ^ _216280) ^ [] : [-(leq(n0, 444 ^ [_232054, _232056]))], (452 ^ _216280) ^ [] : [-(leq(444 ^ [_232054, _232056], _232054))], (454 ^ _216280) ^ [] : [a_select3(_232056, 443 ^ [_232054, _232056], 444 ^ [_232054, _232056]) = a_select3(_232056, 444 ^ [_232054, _232056], 443 ^ [_232054, _232056])]], 455 ^ _216280 : [(456 ^ _216280) ^ [_232811, _232813] : [-(a_select3(inv(_232056), _232813, _232811) = a_select3(inv(_232056), _232811, _232813)), leq(n0, _232813), leq(_232813, _232054), leq(n0, _232811), leq(_232811, _232054)]]], (474 ^ _216280) ^ [_233358, _233360] : [477 ^ _216280 : [(478 ^ _216280) ^ [] : [-(leq(n0, 475 ^ [_233358, _233360]))], (480 ^ _216280) ^ [] : [-(leq(475 ^ [_233358, _233360], _233358))], (482 ^ _216280) ^ [] : [-(leq(n0, 476 ^ [_233358, _233360]))], (484 ^ _216280) ^ [] : [-(leq(476 ^ [_233358, _233360], _233358))], (486 ^ _216280) ^ [] : [a_select3(_233360, 475 ^ [_233358, _233360], 476 ^ [_233358, _233360]) = a_select3(_233360, 476 ^ [_233358, _233360], 475 ^ [_233358, _233360])]], 487 ^ _216280 : [(488 ^ _216280) ^ [_234171, _234173, _234175, _234177] : [-(a_select3(tptp_update3(_233360, _234173, _234173, _234171), _234177, _234175) = a_select3(tptp_update3(_233360, _234173, _234173, _234171), _234175, _234177)), leq(n0, _234177), leq(_234177, _233358), leq(n0, _234175), leq(_234175, _233358), leq(n0, _234173), leq(_234173, _233358)]]], (514 ^ _216280) ^ [_234990, _234992, _234994] : [519 ^ _216280 : [(520 ^ _216280) ^ [] : [-(leq(n0, 517 ^ [_234990, _234992, _234994]))], (522 ^ _216280) ^ [] : [-(leq(517 ^ [_234990, _234992, _234994], _234990))], (524 ^ _216280) ^ [] : [-(leq(n0, 518 ^ [_234990, _234992, _234994]))], (526 ^ _216280) ^ [] : [-(leq(518 ^ [_234990, _234992, _234994], _234990))], (528 ^ _216280) ^ [] : [a_select3(_234994, 517 ^ [_234990, _234992, _234994], 518 ^ [_234990, _234992, _234994]) = a_select3(_234994, 518 ^ [_234990, _234992, _234994], 517 ^ [_234990, _234992, _234994])]], 531 ^ _216280 : [(532 ^ _216280) ^ [] : [-(leq(n0, 529 ^ [_234990, _234992, _234994]))], (534 ^ _216280) ^ [] : [-(leq(529 ^ [_234990, _234992, _234994], _234990))], (536 ^ _216280) ^ [] : [-(leq(n0, 530 ^ [_234990, _234992, _234994]))], (538 ^ _216280) ^ [] : [-(leq(530 ^ [_234990, _234992, _234994], _234990))], (540 ^ _216280) ^ [] : [a_select3(_234992, 529 ^ [_234990, _234992, _234994], 530 ^ [_234990, _234992, _234994]) = a_select3(_234992, 530 ^ [_234990, _234992, _234994], 529 ^ [_234990, _234992, _234994])]], 541 ^ _216280 : [(542 ^ _216280) ^ [_236499, _236501] : [-(a_select3(tptp_madd(_234994, _234992), _236501, _236499) = a_select3(tptp_madd(_234994, _234992), _236499, _236501)), leq(n0, _236501), leq(_236501, _234990), leq(n0, _236499), leq(_236499, _234990)]]], (560 ^ _216280) ^ [_237085, _237087, _237089] : [565 ^ _216280 : [(566 ^ _216280) ^ [] : [-(leq(n0, 563 ^ [_237085, _237087, _237089]))], (568 ^ _216280) ^ [] : [-(leq(563 ^ [_237085, _237087, _237089], _237085))], (570 ^ _216280) ^ [] : [-(leq(n0, 564 ^ [_237085, _237087, _237089]))], (572 ^ _216280) ^ [] : [-(leq(564 ^ [_237085, _237087, _237089], _237085))], (574 ^ _216280) ^ [] : [a_select3(_237089, 563 ^ [_237085, _237087, _237089], 564 ^ [_237085, _237087, _237089]) = a_select3(_237089, 564 ^ [_237085, _237087, _237089], 563 ^ [_237085, _237087, _237089])]], 577 ^ _216280 : [(578 ^ _216280) ^ [] : [-(leq(n0, 575 ^ [_237085, _237087, _237089]))], (580 ^ _216280) ^ [] : [-(leq(575 ^ [_237085, _237087, _237089], _237085))], (582 ^ _216280) ^ [] : [-(leq(n0, 576 ^ [_237085, _237087, _237089]))], (584 ^ _216280) ^ [] : [-(leq(576 ^ [_237085, _237087, _237089], _237085))], (586 ^ _216280) ^ [] : [a_select3(_237087, 575 ^ [_237085, _237087, _237089], 576 ^ [_237085, _237087, _237089]) = a_select3(_237087, 576 ^ [_237085, _237087, _237089], 575 ^ [_237085, _237087, _237089])]], 587 ^ _216280 : [(588 ^ _216280) ^ [_238594, _238596] : [-(a_select3(tptp_msub(_237089, _237087), _238596, _238594) = a_select3(tptp_msub(_237089, _237087), _238594, _238596)), leq(n0, _238596), leq(_238596, _237085), leq(n0, _238594), leq(_238594, _237085)]]], (606 ^ _216280) ^ [_239180, _239182, _239184] : [609 ^ _216280 : [(610 ^ _216280) ^ [] : [-(leq(n0, 607 ^ [_239180, _239182, _239184]))], (612 ^ _216280) ^ [] : [-(leq(607 ^ [_239180, _239182, _239184], _239180))], (614 ^ _216280) ^ [] : [-(leq(n0, 608 ^ [_239180, _239182, _239184]))], (616 ^ _216280) ^ [] : [-(leq(608 ^ [_239180, _239182, _239184], _239180))], (618 ^ _216280) ^ [] : [a_select3(_239182, 607 ^ [_239180, _239182, _239184], 608 ^ [_239180, _239182, _239184]) = a_select3(_239182, 608 ^ [_239180, _239182, _239184], 607 ^ [_239180, _239182, _239184])]], 619 ^ _216280 : [(620 ^ _216280) ^ [_239993, _239995] : [-(a_select3(tptp_mmul(_239184, tptp_mmul(_239182, trans(_239184))), _239995, _239993) = a_select3(tptp_mmul(_239184, tptp_mmul(_239182, trans(_239184))), _239993, _239995)), leq(n0, _239995), leq(_239995, _239180), leq(n0, _239993), leq(_239993, _239180)]]], (638 ^ _216280) ^ [_240612, _240614, _240616, _240618] : [641 ^ _216280 : [(642 ^ _216280) ^ [] : [-(leq(n0, 639 ^ [_240612, _240614, _240616, _240618]))], (644 ^ _216280) ^ [] : [-(leq(639 ^ [_240612, _240614, _240616, _240618], _240612))], (646 ^ _216280) ^ [] : [-(leq(n0, 640 ^ [_240612, _240614, _240616, _240618]))], (648 ^ _216280) ^ [] : [-(leq(640 ^ [_240612, _240614, _240616, _240618], _240612))], (650 ^ _216280) ^ [] : [a_select3(_240616, 639 ^ [_240612, _240614, _240616, _240618], 640 ^ [_240612, _240614, _240616, _240618]) = a_select3(_240616, 640 ^ [_240612, _240614, _240616, _240618], 639 ^ [_240612, _240614, _240616, _240618])]], 651 ^ _216280 : [(652 ^ _216280) ^ [_241469, _241471] : [-(a_select3(tptp_mmul(_240618, tptp_mmul(_240616, trans(_240618))), _241471, _241469) = a_select3(tptp_mmul(_240618, tptp_mmul(_240616, trans(_240618))), _241469, _241471)), leq(n0, _241471), leq(_241471, _240614), leq(n0, _241469), leq(_241469, _240614)]]], (670 ^ _216280) ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178] : [675 ^ _216280 : [(676 ^ _216280) ^ [] : [-(leq(n0, 673 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178]))], (678 ^ _216280) ^ [] : [-(leq(673 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178], _242164))], (680 ^ _216280) ^ [] : [-(leq(n0, 674 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178]))], (682 ^ _216280) ^ [] : [-(leq(674 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178], _242164))], (684 ^ _216280) ^ [] : [a_select3(_242172, 673 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178], 674 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178]) = a_select3(_242172, 674 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178], 673 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178])]], 689 ^ _216280 : [(690 ^ _216280) ^ [] : [-(leq(n0, 687 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178]))], (692 ^ _216280) ^ [] : [-(leq(687 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178], _242166))], (694 ^ _216280) ^ [] : [-(leq(n0, 688 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178]))], (696 ^ _216280) ^ [] : [-(leq(688 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178], _242166))], (698 ^ _216280) ^ [] : [a_select3(_242178, 687 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178], 688 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178]) = a_select3(_242178, 688 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178], 687 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178])]], 701 ^ _216280 : [(702 ^ _216280) ^ [] : [-(leq(n0, 699 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178]))], (704 ^ _216280) ^ [] : [-(leq(699 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178], _242166))], (706 ^ _216280) ^ [] : [-(leq(n0, 700 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178]))], (708 ^ _216280) ^ [] : [-(leq(700 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178], _242166))], (710 ^ _216280) ^ [] : [a_select3(_242168, 699 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178], 700 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178]) = a_select3(_242168, 700 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178], 699 ^ [_242164, _242166, _242168, _242170, _242172, _242174, _242176, _242178])]], 711 ^ _216280 : [(712 ^ _216280) ^ [_245092, _245094] : [-(a_select3(tptp_madd(_242178, tptp_mmul(_242176, tptp_mmul(tptp_madd(tptp_mmul(_242174, tptp_mmul(_242172, trans(_242174))), tptp_mmul(_242170, tptp_mmul(_242168, trans(_242170)))), trans(_242176)))), _245094, _245092) = a_select3(tptp_madd(_242178, tptp_mmul(_242176, tptp_mmul(tptp_madd(tptp_mmul(_242174, tptp_mmul(_242172, trans(_242174))), tptp_mmul(_242170, tptp_mmul(_242168, trans(_242170)))), trans(_242176)))), _245092, _245094)), leq(n0, _245094), leq(_245094, _242166), leq(n0, _245092), leq(_245092, _242166)]]], (730 ^ _216280) ^ [_245845] : [-(sum(n0, tptp_minus_1, _245845) = n0)], (732 ^ _216280) ^ [_245927] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _245927))], (734 ^ _216280) ^ [] : [-(succ(tptp_minus_1) = n0)], (736 ^ _216280) ^ [_246062] : [-(plus(_246062, n1) = succ(_246062))], (738 ^ _216280) ^ [_246145] : [-(plus(n1, _246145) = succ(_246145))], (740 ^ _216280) ^ [_246228] : [-(plus(_246228, n2) = succ(succ(_246228)))], (742 ^ _216280) ^ [_246313] : [-(plus(n2, _246313) = succ(succ(_246313)))], (744 ^ _216280) ^ [_246398] : [-(plus(_246398, n3) = succ(succ(succ(_246398))))], (746 ^ _216280) ^ [_246485] : [-(plus(n3, _246485) = succ(succ(succ(_246485))))], (748 ^ _216280) ^ [_246572] : [-(plus(_246572, n4) = succ(succ(succ(succ(_246572)))))], (750 ^ _216280) ^ [_246661] : [-(plus(n4, _246661) = succ(succ(succ(succ(_246661)))))], (752 ^ _216280) ^ [_246750] : [-(plus(_246750, n5) = succ(succ(succ(succ(succ(_246750))))))], (754 ^ _216280) ^ [_246841] : [-(plus(n5, _246841) = succ(succ(succ(succ(succ(_246841))))))], (756 ^ _216280) ^ [_246932] : [-(minus(_246932, n1) = pred(_246932))], (758 ^ _216280) ^ [_247015] : [-(pred(succ(_247015)) = _247015)], (760 ^ _216280) ^ [_247097] : [-(succ(pred(_247097)) = _247097)], (762 ^ _216280) ^ [_247237, _247239] : [leq(succ(_247239), succ(_247237)), -(leq(_247239, _247237))], (768 ^ _216280) ^ [_247407, _247409] : [leq(_247409, _247407), -(leq(succ(_247409), succ(_247407)))], (774 ^ _216280) ^ [_247627, _247629] : [leq(succ(_247629), _247627), -(gt(_247627, _247629))], (780 ^ _216280) ^ [_247841, _247843] : [leq(minus(_247843, _247841), _247843), -(leq(n0, _247841))], (786 ^ _216280) ^ [_248070, _248072, _248074, _248076] : [-(a_select3(tptp_update3(_248076, _248074, _248072, _248070), _248074, _248072) = _248070)], (788 ^ _216280) ^ [_248262, _248264, _248266, _248268, _248270, _248272, _248274] : [-(a_select3(tptp_update3(_248266, _248274, _248272, _248262), _248270, _248268) = _248264), -(_248274 = _248270), _248272 = _248268, a_select3(_248266, _248270, _248268) = _248264], (802 ^ _216280) ^ [_248805, _248807, _248809, _248811, _248813, _248815] : [-(a_select3(tptp_update3(_248807, _248811, _248809, _248805), _248815, _248813) = _248805), 807 ^ _216280 : [(808 ^ _216280) ^ [] : [-(leq(n0, 805 ^ [_248805, _248807, _248809, _248811, _248813, _248815]))], (810 ^ _216280) ^ [] : [-(leq(n0, 806 ^ [_248805, _248807, _248809, _248811, _248813, _248815]))], (812 ^ _216280) ^ [] : [-(leq(805 ^ [_248805, _248807, _248809, _248811, _248813, _248815], _248811))], (814 ^ _216280) ^ [] : [-(leq(806 ^ [_248805, _248807, _248809, _248811, _248813, _248815], _248809))], (816 ^ _216280) ^ [] : [a_select3(_248807, 805 ^ [_248805, _248807, _248809, _248811, _248813, _248815], 806 ^ [_248805, _248807, _248809, _248811, _248813, _248815]) = _248805]], leq(n0, _248815), leq(_248815, _248811), leq(n0, _248813), leq(_248813, _248809)], (834 ^ _216280) ^ [_250147, _250149, _250151] : [-(a_select2(tptp_update2(_250151, _250149, _250147), _250149) = _250147)], (836 ^ _216280) ^ [_250307, _250309, _250311, _250313, _250315] : [-(a_select2(tptp_update2(_250311, _250315, _250307), _250313) = _250309), -(_250315 = _250313), a_select2(_250311, _250313) = _250309], (865 ^ _216280) ^ [] : [-(true)], (867 ^ _216280) ^ [] : [def = use], (846 ^ _216280) ^ [_250687, _250689, _250691, _250693] : [-(a_select2(tptp_update2(_250689, _250691, _250687), _250693) = _250687), 850 ^ _216280 : [(851 ^ _216280) ^ [] : [-(leq(n0, 849 ^ [_250687, _250689, _250691, _250693]))], (853 ^ _216280) ^ [] : [-(leq(849 ^ [_250687, _250689, _250691, _250693], _250691))], (855 ^ _216280) ^ [] : [a_select2(_250689, 849 ^ [_250687, _250689, _250691, _250693]) = _250687]], leq(n0, _250693), leq(_250693, _250691)]], input).
% 0.36/1.37 ncf('1',plain,[n2 = 1077 ^ [], n5 = 1076 ^ []],start(1153 ^ 0)).
% 0.36/1.37 ncf('1.1',plain,[-(n2 = 1077 ^ [])],extension(1213 ^ 1)).
% 0.36/1.37 ncf('1.2',plain,[-(n5 = 1076 ^ [])],extension(1219 ^ 1)).
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------