%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV219+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n009.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:11 EDT 2023
% Result : Theorem 0.35s 1.39s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWV219+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n009.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:48:47 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.35/1.39
% 0.35/1.39 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.35/1.39 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.35/1.39 %-----------------------------------------------------
% 0.35/1.39 ncf(matrix, plain, [(1077 ^ _210409) ^ [] : [-(leq(n0, 1074 ^ []))], (1079 ^ _210409) ^ [] : [-(leq(n0, 1075 ^ []))], (1081 ^ _210409) ^ [] : [-(leq(1074 ^ [], n5))], (1083 ^ _210409) ^ [] : [-(leq(1075 ^ [], n5))], (1163 ^ _210409) ^ [] : [times(divide(n1, n400), a_select2(sigma, n4)) = n0], (1085 ^ _210409) ^ [] : [n0 = 1074 ^ [], n5 = 1075 ^ []], (1091 ^ _210409) ^ [] : [n0 = 1075 ^ [], n5 = 1074 ^ []], (1097 ^ _210409) ^ [] : [n1 = 1074 ^ [], n5 = 1075 ^ []], (1103 ^ _210409) ^ [] : [n1 = 1075 ^ [], n5 = 1074 ^ []], (1109 ^ _210409) ^ [] : [n2 = 1074 ^ [], n5 = 1075 ^ []], (1115 ^ _210409) ^ [] : [n2 = 1075 ^ [], n5 = 1074 ^ []], (1121 ^ _210409) ^ [] : [n3 = 1074 ^ [], n5 = 1075 ^ []], (1127 ^ _210409) ^ [] : [n3 = 1075 ^ [], n5 = 1074 ^ []], (1133 ^ _210409) ^ [] : [n4 = 1074 ^ [], n4 = 1075 ^ []], (1139 ^ _210409) ^ [] : [n4 = 1074 ^ [], n5 = 1075 ^ []], (1145 ^ _210409) ^ [] : [n4 = 1075 ^ [], n5 = 1074 ^ []], (1157 ^ _210409) ^ [] : [-(n3 = 1074 ^ [])], (1159 ^ _210409) ^ [] : [-(n4 = 1074 ^ [])], (1161 ^ _210409) ^ [] : [-(n4 = 1075 ^ [])], (1151 ^ _210409) ^ [] : [n5 = 1074 ^ [], n5 = 1075 ^ []], (2 ^ _210409) ^ [_210553] : [-(_210553 = _210553)], (4 ^ _210409) ^ [_210660, _210662] : [_210662 = _210660, -(_210660 = _210662)], (10 ^ _210409) ^ [_210864, _210866, _210868] : [-(_210868 = _210864), _210868 = _210866, _210866 = _210864], (20 ^ _210409) ^ [_211205, _211207, _211209, _211211] : [-(lt(_211209, _211205)), lt(_211211, _211207), _211211 = _211209, _211207 = _211205], (34 ^ _210409) ^ [_211649, _211651, _211653, _211655] : [-(geq(_211653, _211649)), geq(_211655, _211651), _211655 = _211653, _211651 = _211649], (48 ^ _210409) ^ [_212093, _212095, _212097, _212099] : [-(gt(_212097, _212093)), gt(_212099, _212095), _212099 = _212097, _212095 = _212093], (62 ^ _210409) ^ [_212517, _212519, _212521, _212523] : [-(leq(_212521, _212517)), leq(_212523, _212519), _212523 = _212521, _212519 = _212517], (76 ^ _210409) ^ [_212973, _212975, _212977, _212979] : [-(uniform_int_rnd(_212979, _212975) = uniform_int_rnd(_212977, _212973)), _212979 = _212977, _212975 = _212973], (86 ^ _210409) ^ [_213332, _213334, _213336, _213338] : [-(tptp_const_array1(_213338, _213334) = tptp_const_array1(_213336, _213332)), _213338 = _213336, _213334 = _213332], (96 ^ _210409) ^ [_213719, _213721, _213723, _213725, _213727, _213729] : [-(tptp_const_array2(_213729, _213725, _213721) = tptp_const_array2(_213727, _213723, _213719)), _213729 = _213727, _213725 = _213723, _213721 = _213719], (110 ^ _210409) ^ [_214207, _214209, _214211, _214213] : [-(dim(_214213, _214209) = dim(_214211, _214207)), _214213 = _214211, _214209 = _214207], (120 ^ _210409) ^ [_214538, _214540] : [_214540 = _214538, -(inv(_214540) = inv(_214538))], (126 ^ _210409) ^ [_214784, _214786, _214788, _214790] : [-(tptp_msub(_214790, _214786) = tptp_msub(_214788, _214784)), _214790 = _214788, _214786 = _214784], (136 ^ _210409) ^ [_215143, _215145, _215147, _215149] : [-(tptp_madd(_215149, _215145) = tptp_madd(_215147, _215143)), _215149 = _215147, _215145 = _215143], (146 ^ _210409) ^ [_215502, _215504, _215506, _215508] : [-(tptp_mmul(_215508, _215504) = tptp_mmul(_215506, _215502)), _215508 = _215506, _215504 = _215502], (156 ^ _210409) ^ [_215833, _215835] : [_215835 = _215833, -(trans(_215835) = trans(_215833))], (162 ^ _210409) ^ [_216107, _216109, _216111, _216113, _216115, _216117] : [-(sum(_216117, _216113, _216109) = sum(_216115, _216111, _216107)), _216117 = _216115, _216113 = _216111, _216109 = _216107], (176 ^ _210409) ^ [_216595, _216597, _216599, _216601] : [-(plus(_216601, _216597) = plus(_216599, _216595)), _216601 = _216599, _216597 = _216595], (186 ^ _210409) ^ [_216926, _216928] : [_216928 = _216926, -(pred(_216928) = pred(_216926))], (192 ^ _210409) ^ [_217172, _217174, _217176, _217178] : [-(minus(_217178, _217174) = minus(_217176, _217172)), _217178 = _217176, _217174 = _217172], (202 ^ _210409) ^ [_217559, _217561, _217563, _217565, _217567, _217569] : [-(a_select3(_217569, _217565, _217561) = a_select3(_217567, _217563, _217559)), _217569 = _217567, _217565 = _217563, _217561 = _217559], (216 ^ _210409) ^ [_218103, _218105, _218107, _218109, _218111, _218113, _218115, _218117] : [-(tptp_update3(_218117, _218113, _218109, _218105) = tptp_update3(_218115, _218111, _218107, _218103)), _218117 = _218115, _218113 = _218111, _218109 = _218107, _218105 = _218103], (234 ^ _210409) ^ [_218764, _218766, _218768, _218770, _218772, _218774] : [-(tptp_update2(_218774, _218770, _218766) = tptp_update2(_218772, _218768, _218764)), _218774 = _218772, _218770 = _218768, _218766 = _218764], (248 ^ _210409) ^ [_219224, _219226] : [_219226 = _219224, -(succ(_219226) = succ(_219224))], (254 ^ _210409) ^ [_219470, _219472, _219474, _219476] : [-(times(_219476, _219472) = times(_219474, _219470)), _219476 = _219474, _219472 = _219470], (264 ^ _210409) ^ [_219829, _219831, _219833, _219835] : [-(divide(_219835, _219831) = divide(_219833, _219829)), _219835 = _219833, _219831 = _219829], (274 ^ _210409) ^ [_220168, _220170, _220172, _220174] : [-(a_select2(_220174, _220170) = a_select2(_220172, _220168)), _220174 = _220172, _220170 = _220168], (889 ^ _210409) ^ [] : [-(gt(n5, n4))], (891 ^ _210409) ^ [] : [-(gt(n400, n4))], (893 ^ _210409) ^ [] : [-(gt(n400, n5))], (895 ^ _210409) ^ [] : [-(gt(n4, tptp_minus_1))], (897 ^ _210409) ^ [] : [-(gt(n5, tptp_minus_1))], (899 ^ _210409) ^ [] : [-(gt(n400, tptp_minus_1))], (901 ^ _210409) ^ [] : [-(gt(n0, tptp_minus_1))], (903 ^ _210409) ^ [] : [-(gt(n1, tptp_minus_1))], (905 ^ _210409) ^ [] : [-(gt(n2, tptp_minus_1))], (907 ^ _210409) ^ [] : [-(gt(n3, tptp_minus_1))], (909 ^ _210409) ^ [] : [-(gt(n4, n0))], (911 ^ _210409) ^ [] : [-(gt(n5, n0))], (913 ^ _210409) ^ [] : [-(gt(n400, n0))], (915 ^ _210409) ^ [] : [-(gt(n1, n0))], (917 ^ _210409) ^ [] : [-(gt(n2, n0))], (919 ^ _210409) ^ [] : [-(gt(n3, n0))], (921 ^ _210409) ^ [] : [-(gt(n4, n1))], (923 ^ _210409) ^ [] : [-(gt(n5, n1))], (925 ^ _210409) ^ [] : [-(gt(n400, n1))], (927 ^ _210409) ^ [] : [-(gt(n2, n1))], (929 ^ _210409) ^ [] : [-(gt(n3, n1))], (931 ^ _210409) ^ [] : [-(gt(n4, n2))], (933 ^ _210409) ^ [] : [-(gt(n5, n2))], (935 ^ _210409) ^ [] : [-(gt(n400, n2))], (937 ^ _210409) ^ [] : [-(gt(n3, n2))], (939 ^ _210409) ^ [] : [-(gt(n4, n3))], (941 ^ _210409) ^ [] : [-(gt(n5, n3))], (943 ^ _210409) ^ [] : [-(gt(n400, n3))], (945 ^ _210409) ^ [_248016] : [leq(n0, _248016), leq(_248016, n4), -(_248016 = n0), -(_248016 = n1), -(_248016 = n2), -(_248016 = n3), -(_248016 = n4)], (971 ^ _210409) ^ [_248637] : [leq(n0, _248637), leq(_248637, n5), -(_248637 = n0), -(_248637 = n1), -(_248637 = n2), -(_248637 = n3), -(_248637 = n4), -(_248637 = n5)], (1001 ^ _210409) ^ [_249344] : [-(_249344 = n0), leq(n0, _249344), leq(_249344, n0)], (1011 ^ _210409) ^ [_249619] : [leq(n0, _249619), leq(_249619, n1), -(_249619 = n0), -(_249619 = n1)], (1025 ^ _210409) ^ [_249982] : [leq(n0, _249982), leq(_249982, n2), -(_249982 = n0), -(_249982 = n1), -(_249982 = n2)], (1065 ^ _210409) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (1067 ^ _210409) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (1069 ^ _210409) ^ [] : [-(succ(n0) = n1)], (1071 ^ _210409) ^ [] : [-(succ(succ(n0)) = n2)], (1073 ^ _210409) ^ [] : [-(succ(succ(succ(n0))) = n3)], (1043 ^ _210409) ^ [_250431] : [leq(n0, _250431), leq(_250431, n3), -(_250431 = n0), -(_250431 = n1), -(_250431 = n2), -(_250431 = n3)], (284 ^ _210409) ^ [_220607, _220609] : [-(gt(_220609, _220607)), -(gt(_220607, _220609)), -(_220609 = _220607)], (294 ^ _210409) ^ [_220922, _220924, _220926] : [-(gt(_220926, _220922)), gt(_220926, _220924), gt(_220924, _220922)], (304 ^ _210409) ^ [_221201] : [gt(_221201, _221201)], (306 ^ _210409) ^ [_221279] : [-(leq(_221279, _221279))], (308 ^ _210409) ^ [_221400, _221402, _221404] : [-(leq(_221404, _221400)), leq(_221404, _221402), leq(_221402, _221400)], (318 ^ _210409) ^ [_221738, _221740] : [lt(_221740, _221738), -(gt(_221738, _221740))], (324 ^ _210409) ^ [_221900, _221902] : [gt(_221900, _221902), -(lt(_221902, _221900))], (330 ^ _210409) ^ [_222141, _222143] : [geq(_222143, _222141), -(leq(_222141, _222143))], (336 ^ _210409) ^ [_222303, _222305] : [leq(_222303, _222305), -(geq(_222305, _222303))], (342 ^ _210409) ^ [_222515, _222517] : [gt(_222515, _222517), -(leq(_222517, _222515))], (348 ^ _210409) ^ [_222725, _222727] : [-(gt(_222725, _222727)), leq(_222727, _222725), -(_222727 = _222725)], (358 ^ _210409) ^ [_223056, _223058] : [leq(_223058, pred(_223056)), -(gt(_223056, _223058))], (364 ^ _210409) ^ [_223222, _223224] : [gt(_223222, _223224), -(leq(_223224, pred(_223222)))], (370 ^ _210409) ^ [_223409] : [-(gt(succ(_223409), _223409))], (372 ^ _210409) ^ [_223518, _223520] : [leq(_223520, _223518), -(leq(_223520, succ(_223518)))], (378 ^ _210409) ^ [_223761, _223763] : [leq(_223763, _223761), -(gt(succ(_223761), _223763))], (384 ^ _210409) ^ [_223927, _223929] : [gt(succ(_223927), _223929), -(leq(_223929, _223927))], (390 ^ _210409) ^ [_224143, _224145] : [leq(n0, _224145), -(leq(uniform_int_rnd(_224143, _224145), _224145))], (396 ^ _210409) ^ [_224359, _224361] : [leq(n0, _224361), -(leq(n0, uniform_int_rnd(_224359, _224361)))], (402 ^ _210409) ^ [_224603, _224605, _224607, _224609] : [-(a_select2(tptp_const_array1(dim(_224607, _224605), _224603), _224609) = _224603), leq(_224607, _224609), leq(_224609, _224605)], (412 ^ _210409) ^ [_225010, _225012, _225014, _225016, _225018, _225020, _225022] : [-(a_select3(tptp_const_array2(dim(_225020, _225018), dim(_225014, _225012), _225010), _225022, _225016) = _225010), leq(_225020, _225022), leq(_225022, _225018), leq(_225014, _225016), leq(_225016, _225012)], (430 ^ _210409) ^ [_225605, _225607] : [433 ^ _210409 : [(434 ^ _210409) ^ [] : [-(leq(n0, 431 ^ [_225605, _225607]))], (436 ^ _210409) ^ [] : [-(leq(431 ^ [_225605, _225607], _225605))], (438 ^ _210409) ^ [] : [-(leq(n0, 432 ^ [_225605, _225607]))], (440 ^ _210409) ^ [] : [-(leq(432 ^ [_225605, _225607], _225605))], (442 ^ _210409) ^ [] : [a_select3(_225607, 431 ^ [_225605, _225607], 432 ^ [_225605, _225607]) = a_select3(_225607, 432 ^ [_225605, _225607], 431 ^ [_225605, _225607])]], 443 ^ _210409 : [(444 ^ _210409) ^ [_226362, _226364] : [-(a_select3(trans(_225607), _226364, _226362) = a_select3(trans(_225607), _226362, _226364)), leq(n0, _226364), leq(_226364, _225605), leq(n0, _226362), leq(_226362, _225605)]]], (462 ^ _210409) ^ [_226909, _226911] : [465 ^ _210409 : [(466 ^ _210409) ^ [] : [-(leq(n0, 463 ^ [_226909, _226911]))], (468 ^ _210409) ^ [] : [-(leq(463 ^ [_226909, _226911], _226909))], (470 ^ _210409) ^ [] : [-(leq(n0, 464 ^ [_226909, _226911]))], (472 ^ _210409) ^ [] : [-(leq(464 ^ [_226909, _226911], _226909))], (474 ^ _210409) ^ [] : [a_select3(_226911, 463 ^ [_226909, _226911], 464 ^ [_226909, _226911]) = a_select3(_226911, 464 ^ [_226909, _226911], 463 ^ [_226909, _226911])]], 475 ^ _210409 : [(476 ^ _210409) ^ [_227666, _227668] : [-(a_select3(inv(_226911), _227668, _227666) = a_select3(inv(_226911), _227666, _227668)), leq(n0, _227668), leq(_227668, _226909), leq(n0, _227666), leq(_227666, _226909)]]], (494 ^ _210409) ^ [_228213, _228215] : [497 ^ _210409 : [(498 ^ _210409) ^ [] : [-(leq(n0, 495 ^ [_228213, _228215]))], (500 ^ _210409) ^ [] : [-(leq(495 ^ [_228213, _228215], _228213))], (502 ^ _210409) ^ [] : [-(leq(n0, 496 ^ [_228213, _228215]))], (504 ^ _210409) ^ [] : [-(leq(496 ^ [_228213, _228215], _228213))], (506 ^ _210409) ^ [] : [a_select3(_228215, 495 ^ [_228213, _228215], 496 ^ [_228213, _228215]) = a_select3(_228215, 496 ^ [_228213, _228215], 495 ^ [_228213, _228215])]], 507 ^ _210409 : [(508 ^ _210409) ^ [_229026, _229028, _229030, _229032] : [-(a_select3(tptp_update3(_228215, _229028, _229028, _229026), _229032, _229030) = a_select3(tptp_update3(_228215, _229028, _229028, _229026), _229030, _229032)), leq(n0, _229032), leq(_229032, _228213), leq(n0, _229030), leq(_229030, _228213), leq(n0, _229028), leq(_229028, _228213)]]], (534 ^ _210409) ^ [_229845, _229847, _229849] : [539 ^ _210409 : [(540 ^ _210409) ^ [] : [-(leq(n0, 537 ^ [_229845, _229847, _229849]))], (542 ^ _210409) ^ [] : [-(leq(537 ^ [_229845, _229847, _229849], _229845))], (544 ^ _210409) ^ [] : [-(leq(n0, 538 ^ [_229845, _229847, _229849]))], (546 ^ _210409) ^ [] : [-(leq(538 ^ [_229845, _229847, _229849], _229845))], (548 ^ _210409) ^ [] : [a_select3(_229849, 537 ^ [_229845, _229847, _229849], 538 ^ [_229845, _229847, _229849]) = a_select3(_229849, 538 ^ [_229845, _229847, _229849], 537 ^ [_229845, _229847, _229849])]], 551 ^ _210409 : [(552 ^ _210409) ^ [] : [-(leq(n0, 549 ^ [_229845, _229847, _229849]))], (554 ^ _210409) ^ [] : [-(leq(549 ^ [_229845, _229847, _229849], _229845))], (556 ^ _210409) ^ [] : [-(leq(n0, 550 ^ [_229845, _229847, _229849]))], (558 ^ _210409) ^ [] : [-(leq(550 ^ [_229845, _229847, _229849], _229845))], (560 ^ _210409) ^ [] : [a_select3(_229847, 549 ^ [_229845, _229847, _229849], 550 ^ [_229845, _229847, _229849]) = a_select3(_229847, 550 ^ [_229845, _229847, _229849], 549 ^ [_229845, _229847, _229849])]], 561 ^ _210409 : [(562 ^ _210409) ^ [_231354, _231356] : [-(a_select3(tptp_madd(_229849, _229847), _231356, _231354) = a_select3(tptp_madd(_229849, _229847), _231354, _231356)), leq(n0, _231356), leq(_231356, _229845), leq(n0, _231354), leq(_231354, _229845)]]], (580 ^ _210409) ^ [_231940, _231942, _231944] : [585 ^ _210409 : [(586 ^ _210409) ^ [] : [-(leq(n0, 583 ^ [_231940, _231942, _231944]))], (588 ^ _210409) ^ [] : [-(leq(583 ^ [_231940, _231942, _231944], _231940))], (590 ^ _210409) ^ [] : [-(leq(n0, 584 ^ [_231940, _231942, _231944]))], (592 ^ _210409) ^ [] : [-(leq(584 ^ [_231940, _231942, _231944], _231940))], (594 ^ _210409) ^ [] : [a_select3(_231944, 583 ^ [_231940, _231942, _231944], 584 ^ [_231940, _231942, _231944]) = a_select3(_231944, 584 ^ [_231940, _231942, _231944], 583 ^ [_231940, _231942, _231944])]], 597 ^ _210409 : [(598 ^ _210409) ^ [] : [-(leq(n0, 595 ^ [_231940, _231942, _231944]))], (600 ^ _210409) ^ [] : [-(leq(595 ^ [_231940, _231942, _231944], _231940))], (602 ^ _210409) ^ [] : [-(leq(n0, 596 ^ [_231940, _231942, _231944]))], (604 ^ _210409) ^ [] : [-(leq(596 ^ [_231940, _231942, _231944], _231940))], (606 ^ _210409) ^ [] : [a_select3(_231942, 595 ^ [_231940, _231942, _231944], 596 ^ [_231940, _231942, _231944]) = a_select3(_231942, 596 ^ [_231940, _231942, _231944], 595 ^ [_231940, _231942, _231944])]], 607 ^ _210409 : [(608 ^ _210409) ^ [_233449, _233451] : [-(a_select3(tptp_msub(_231944, _231942), _233451, _233449) = a_select3(tptp_msub(_231944, _231942), _233449, _233451)), leq(n0, _233451), leq(_233451, _231940), leq(n0, _233449), leq(_233449, _231940)]]], (626 ^ _210409) ^ [_234035, _234037, _234039] : [629 ^ _210409 : [(630 ^ _210409) ^ [] : [-(leq(n0, 627 ^ [_234035, _234037, _234039]))], (632 ^ _210409) ^ [] : [-(leq(627 ^ [_234035, _234037, _234039], _234035))], (634 ^ _210409) ^ [] : [-(leq(n0, 628 ^ [_234035, _234037, _234039]))], (636 ^ _210409) ^ [] : [-(leq(628 ^ [_234035, _234037, _234039], _234035))], (638 ^ _210409) ^ [] : [a_select3(_234037, 627 ^ [_234035, _234037, _234039], 628 ^ [_234035, _234037, _234039]) = a_select3(_234037, 628 ^ [_234035, _234037, _234039], 627 ^ [_234035, _234037, _234039])]], 639 ^ _210409 : [(640 ^ _210409) ^ [_234848, _234850] : [-(a_select3(tptp_mmul(_234039, tptp_mmul(_234037, trans(_234039))), _234850, _234848) = a_select3(tptp_mmul(_234039, tptp_mmul(_234037, trans(_234039))), _234848, _234850)), leq(n0, _234850), leq(_234850, _234035), leq(n0, _234848), leq(_234848, _234035)]]], (658 ^ _210409) ^ [_235467, _235469, _235471, _235473] : [661 ^ _210409 : [(662 ^ _210409) ^ [] : [-(leq(n0, 659 ^ [_235467, _235469, _235471, _235473]))], (664 ^ _210409) ^ [] : [-(leq(659 ^ [_235467, _235469, _235471, _235473], _235467))], (666 ^ _210409) ^ [] : [-(leq(n0, 660 ^ [_235467, _235469, _235471, _235473]))], (668 ^ _210409) ^ [] : [-(leq(660 ^ [_235467, _235469, _235471, _235473], _235467))], (670 ^ _210409) ^ [] : [a_select3(_235471, 659 ^ [_235467, _235469, _235471, _235473], 660 ^ [_235467, _235469, _235471, _235473]) = a_select3(_235471, 660 ^ [_235467, _235469, _235471, _235473], 659 ^ [_235467, _235469, _235471, _235473])]], 671 ^ _210409 : [(672 ^ _210409) ^ [_236324, _236326] : [-(a_select3(tptp_mmul(_235473, tptp_mmul(_235471, trans(_235473))), _236326, _236324) = a_select3(tptp_mmul(_235473, tptp_mmul(_235471, trans(_235473))), _236324, _236326)), leq(n0, _236326), leq(_236326, _235469), leq(n0, _236324), leq(_236324, _235469)]]], (690 ^ _210409) ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033] : [695 ^ _210409 : [(696 ^ _210409) ^ [] : [-(leq(n0, 693 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033]))], (698 ^ _210409) ^ [] : [-(leq(693 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033], _237019))], (700 ^ _210409) ^ [] : [-(leq(n0, 694 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033]))], (702 ^ _210409) ^ [] : [-(leq(694 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033], _237019))], (704 ^ _210409) ^ [] : [a_select3(_237027, 693 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033], 694 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033]) = a_select3(_237027, 694 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033], 693 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033])]], 709 ^ _210409 : [(710 ^ _210409) ^ [] : [-(leq(n0, 707 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033]))], (712 ^ _210409) ^ [] : [-(leq(707 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033], _237021))], (714 ^ _210409) ^ [] : [-(leq(n0, 708 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033]))], (716 ^ _210409) ^ [] : [-(leq(708 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033], _237021))], (718 ^ _210409) ^ [] : [a_select3(_237033, 707 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033], 708 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033]) = a_select3(_237033, 708 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033], 707 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033])]], 721 ^ _210409 : [(722 ^ _210409) ^ [] : [-(leq(n0, 719 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033]))], (724 ^ _210409) ^ [] : [-(leq(719 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033], _237021))], (726 ^ _210409) ^ [] : [-(leq(n0, 720 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033]))], (728 ^ _210409) ^ [] : [-(leq(720 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033], _237021))], (730 ^ _210409) ^ [] : [a_select3(_237023, 719 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033], 720 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033]) = a_select3(_237023, 720 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033], 719 ^ [_237019, _237021, _237023, _237025, _237027, _237029, _237031, _237033])]], 731 ^ _210409 : [(732 ^ _210409) ^ [_239947, _239949] : [-(a_select3(tptp_madd(_237033, tptp_mmul(_237031, tptp_mmul(tptp_madd(tptp_mmul(_237029, tptp_mmul(_237027, trans(_237029))), tptp_mmul(_237025, tptp_mmul(_237023, trans(_237025)))), trans(_237031)))), _239949, _239947) = a_select3(tptp_madd(_237033, tptp_mmul(_237031, tptp_mmul(tptp_madd(tptp_mmul(_237029, tptp_mmul(_237027, trans(_237029))), tptp_mmul(_237025, tptp_mmul(_237023, trans(_237025)))), trans(_237031)))), _239947, _239949)), leq(n0, _239949), leq(_239949, _237021), leq(n0, _239947), leq(_239947, _237021)]]], (750 ^ _210409) ^ [_240700] : [-(sum(n0, tptp_minus_1, _240700) = n0)], (752 ^ _210409) ^ [_240782] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _240782))], (754 ^ _210409) ^ [] : [-(succ(tptp_minus_1) = n0)], (756 ^ _210409) ^ [_240917] : [-(plus(_240917, n1) = succ(_240917))], (758 ^ _210409) ^ [_241000] : [-(plus(n1, _241000) = succ(_241000))], (760 ^ _210409) ^ [_241083] : [-(plus(_241083, n2) = succ(succ(_241083)))], (762 ^ _210409) ^ [_241168] : [-(plus(n2, _241168) = succ(succ(_241168)))], (764 ^ _210409) ^ [_241253] : [-(plus(_241253, n3) = succ(succ(succ(_241253))))], (766 ^ _210409) ^ [_241340] : [-(plus(n3, _241340) = succ(succ(succ(_241340))))], (768 ^ _210409) ^ [_241427] : [-(plus(_241427, n4) = succ(succ(succ(succ(_241427)))))], (770 ^ _210409) ^ [_241516] : [-(plus(n4, _241516) = succ(succ(succ(succ(_241516)))))], (772 ^ _210409) ^ [_241605] : [-(plus(_241605, n5) = succ(succ(succ(succ(succ(_241605))))))], (774 ^ _210409) ^ [_241696] : [-(plus(n5, _241696) = succ(succ(succ(succ(succ(_241696))))))], (776 ^ _210409) ^ [_241787] : [-(minus(_241787, n1) = pred(_241787))], (778 ^ _210409) ^ [_241870] : [-(pred(succ(_241870)) = _241870)], (780 ^ _210409) ^ [_241952] : [-(succ(pred(_241952)) = _241952)], (782 ^ _210409) ^ [_242092, _242094] : [leq(succ(_242094), succ(_242092)), -(leq(_242094, _242092))], (788 ^ _210409) ^ [_242262, _242264] : [leq(_242264, _242262), -(leq(succ(_242264), succ(_242262)))], (794 ^ _210409) ^ [_242482, _242484] : [leq(succ(_242484), _242482), -(gt(_242482, _242484))], (800 ^ _210409) ^ [_242696, _242698] : [leq(minus(_242698, _242696), _242698), -(leq(n0, _242696))], (806 ^ _210409) ^ [_242925, _242927, _242929, _242931] : [-(a_select3(tptp_update3(_242931, _242929, _242927, _242925), _242929, _242927) = _242925)], (808 ^ _210409) ^ [_243117, _243119, _243121, _243123, _243125, _243127, _243129] : [-(a_select3(tptp_update3(_243121, _243129, _243127, _243117), _243125, _243123) = _243119), -(_243129 = _243125), _243127 = _243123, a_select3(_243121, _243125, _243123) = _243119], (822 ^ _210409) ^ [_243660, _243662, _243664, _243666, _243668, _243670] : [-(a_select3(tptp_update3(_243662, _243666, _243664, _243660), _243670, _243668) = _243660), 827 ^ _210409 : [(828 ^ _210409) ^ [] : [-(leq(n0, 825 ^ [_243660, _243662, _243664, _243666, _243668, _243670]))], (830 ^ _210409) ^ [] : [-(leq(n0, 826 ^ [_243660, _243662, _243664, _243666, _243668, _243670]))], (832 ^ _210409) ^ [] : [-(leq(825 ^ [_243660, _243662, _243664, _243666, _243668, _243670], _243666))], (834 ^ _210409) ^ [] : [-(leq(826 ^ [_243660, _243662, _243664, _243666, _243668, _243670], _243664))], (836 ^ _210409) ^ [] : [a_select3(_243662, 825 ^ [_243660, _243662, _243664, _243666, _243668, _243670], 826 ^ [_243660, _243662, _243664, _243666, _243668, _243670]) = _243660]], leq(n0, _243670), leq(_243670, _243666), leq(n0, _243668), leq(_243668, _243664)], (854 ^ _210409) ^ [_245002, _245004, _245006] : [-(a_select2(tptp_update2(_245006, _245004, _245002), _245004) = _245002)], (856 ^ _210409) ^ [_245162, _245164, _245166, _245168, _245170] : [-(a_select2(tptp_update2(_245166, _245170, _245162), _245168) = _245164), -(_245170 = _245168), a_select2(_245166, _245168) = _245164], (885 ^ _210409) ^ [] : [-(true)], (887 ^ _210409) ^ [] : [def = use], (866 ^ _210409) ^ [_245542, _245544, _245546, _245548] : [-(a_select2(tptp_update2(_245544, _245546, _245542), _245548) = _245542), 870 ^ _210409 : [(871 ^ _210409) ^ [] : [-(leq(n0, 869 ^ [_245542, _245544, _245546, _245548]))], (873 ^ _210409) ^ [] : [-(leq(869 ^ [_245542, _245544, _245546, _245548], _245546))], (875 ^ _210409) ^ [] : [a_select2(_245544, 869 ^ [_245542, _245544, _245546, _245548]) = _245542]], leq(n0, _245548), leq(_245548, _245546)]], input).
% 0.35/1.39 ncf('1',plain,[n4 = 1074 ^ [], n4 = 1075 ^ []],start(1133 ^ 0)).
% 0.35/1.39 ncf('1.1',plain,[-(n4 = 1074 ^ [])],extension(1159 ^ 1)).
% 0.35/1.39 ncf('1.2',plain,[-(n4 = 1075 ^ [])],extension(1161 ^ 1)).
% 0.35/1.39 %-----------------------------------------------------
% 0.35/1.39 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------