%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV032+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n031.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri May 19 12:19:48 EDT 2023
% Result : Theorem 0.26s 1.37s
% Output : Proof 0.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SWV032+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.04/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n031.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:44:40 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.26/1.37
% 0.26/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.26/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.26/1.37 %-----------------------------------------------------
% 0.26/1.37 ncf(matrix, plain, [(1113 ^ _221752) ^ [] : [init = init, a_select3(simplex7_init, pv1376, n0) = init, a_select3(simplex7_init, pv1376, n1) = init, a_select3(simplex7_init, pv1376, n2) = init, a_select3(tptp_const_array2(dim(n0, minus(n410, n1)), dim(n0, minus(n330, n1)), init), pv19, pv20) = init, leq(n0, pv19), leq(n0, pv1376), leq(pv19, minus(n410, n1)), leq(pv1376, n3), 1151 ^ _221752 : [(1152 ^ _221752) ^ [] : [-(leq(n0, 1150 ^ []))], (1154 ^ _221752) ^ [] : [-(leq(1150 ^ [], n2))], (1157 ^ _221752) ^ [] : [-(leq(n0, 1155 ^ []))], (1159 ^ _221752) ^ [] : [-(leq(1155 ^ [], n3))], (1161 ^ _221752) ^ [] : [a_select3(simplex7_init, 1155 ^ [], 1150 ^ []) = init]], 1163 ^ _221752 : [(1164 ^ _221752) ^ [] : [-(leq(n0, 1162 ^ []))], (1166 ^ _221752) ^ [] : [-(leq(1162 ^ [], minus(pv1376, n1)))], (1168 ^ _221752) ^ [] : [a_select2(s_values7_init, 1162 ^ []) = init]]], (1071 ^ _221752) ^ [] : [-(init = init)], (1073 ^ _221752) ^ [] : [-(leq(n0, pv19))], (1075 ^ _221752) ^ [] : [-(leq(n0, pv20))], (1077 ^ _221752) ^ [] : [-(leq(n0, pv1376))], (1079 ^ _221752) ^ [] : [-(leq(pv19, minus(n410, n1)))], (1081 ^ _221752) ^ [] : [-(leq(pv20, minus(n330, n1)))], (1083 ^ _221752) ^ [] : [-(leq(pv1376, n3))], (1103 ^ _221752) ^ [_263405] : [-(a_select2(s_values7_init, _263405) = init), leq(n0, _263405), leq(_263405, minus(pv1376, n1))], (1085 ^ _221752) ^ [_262895] : [leq(n0, _262895), leq(_262895, n2), 1092 ^ _221752 : [(1093 ^ _221752) ^ [_263123] : [-(a_select3(simplex7_init, _263123, _262895) = init), leq(n0, _263123), leq(_263123, n3)]]], (2 ^ _221752) ^ [_221896] : [-(_221896 = _221896)], (4 ^ _221752) ^ [_222003, _222005] : [_222005 = _222003, -(_222003 = _222005)], (10 ^ _221752) ^ [_222207, _222209, _222211] : [-(_222211 = _222207), _222211 = _222209, _222209 = _222207], (20 ^ _221752) ^ [_222548, _222550, _222552, _222554] : [-(lt(_222552, _222548)), lt(_222554, _222550), _222554 = _222552, _222550 = _222548], (34 ^ _221752) ^ [_222992, _222994, _222996, _222998] : [-(geq(_222996, _222992)), geq(_222998, _222994), _222998 = _222996, _222994 = _222992], (48 ^ _221752) ^ [_223436, _223438, _223440, _223442] : [-(gt(_223440, _223436)), gt(_223442, _223438), _223442 = _223440, _223438 = _223436], (62 ^ _221752) ^ [_223860, _223862, _223864, _223866] : [-(leq(_223864, _223860)), leq(_223866, _223862), _223866 = _223864, _223862 = _223860], (76 ^ _221752) ^ [_224316, _224318, _224320, _224322] : [-(uniform_int_rnd(_224322, _224318) = uniform_int_rnd(_224320, _224316)), _224322 = _224320, _224318 = _224316], (86 ^ _221752) ^ [_224675, _224677, _224679, _224681] : [-(tptp_const_array1(_224681, _224677) = tptp_const_array1(_224679, _224675)), _224681 = _224679, _224677 = _224675], (96 ^ _221752) ^ [_225006, _225008] : [_225008 = _225006, -(inv(_225008) = inv(_225006))], (102 ^ _221752) ^ [_225252, _225254, _225256, _225258] : [-(tptp_msub(_225258, _225254) = tptp_msub(_225256, _225252)), _225258 = _225256, _225254 = _225252], (112 ^ _221752) ^ [_225611, _225613, _225615, _225617] : [-(tptp_madd(_225617, _225613) = tptp_madd(_225615, _225611)), _225617 = _225615, _225613 = _225611], (122 ^ _221752) ^ [_225970, _225972, _225974, _225976] : [-(tptp_mmul(_225976, _225972) = tptp_mmul(_225974, _225970)), _225976 = _225974, _225972 = _225970], (132 ^ _221752) ^ [_226301, _226303] : [_226303 = _226301, -(trans(_226303) = trans(_226301))], (138 ^ _221752) ^ [_226575, _226577, _226579, _226581, _226583, _226585] : [-(sum(_226585, _226581, _226577) = sum(_226583, _226579, _226575)), _226585 = _226583, _226581 = _226579, _226577 = _226575], (152 ^ _221752) ^ [_227063, _227065, _227067, _227069] : [-(plus(_227069, _227065) = plus(_227067, _227063)), _227069 = _227067, _227065 = _227063], (162 ^ _221752) ^ [_227394, _227396] : [_227396 = _227394, -(pred(_227396) = pred(_227394))], (168 ^ _221752) ^ [_227696, _227698, _227700, _227702, _227704, _227706, _227708, _227710] : [-(tptp_update3(_227710, _227706, _227702, _227698) = tptp_update3(_227708, _227704, _227700, _227696)), _227710 = _227708, _227706 = _227704, _227702 = _227700, _227698 = _227696], (186 ^ _221752) ^ [_228357, _228359, _228361, _228363, _228365, _228367] : [-(tptp_update2(_228367, _228363, _228359) = tptp_update2(_228365, _228361, _228357)), _228367 = _228365, _228363 = _228361, _228359 = _228357], (200 ^ _221752) ^ [_228817, _228819] : [_228819 = _228817, -(succ(_228819) = succ(_228817))], (206 ^ _221752) ^ [_229091, _229093, _229095, _229097, _229099, _229101] : [-(tptp_const_array2(_229101, _229097, _229093) = tptp_const_array2(_229099, _229095, _229091)), _229101 = _229099, _229097 = _229095, _229093 = _229091], (220 ^ _221752) ^ [_229579, _229581, _229583, _229585] : [-(dim(_229585, _229581) = dim(_229583, _229579)), _229585 = _229583, _229581 = _229579], (230 ^ _221752) ^ [_229966, _229968, _229970, _229972, _229974, _229976] : [-(a_select3(_229976, _229972, _229968) = a_select3(_229974, _229970, _229966)), _229976 = _229974, _229972 = _229970, _229968 = _229966], (244 ^ _221752) ^ [_230454, _230456, _230458, _230460] : [-(minus(_230460, _230456) = minus(_230458, _230454)), _230460 = _230458, _230456 = _230454], (254 ^ _221752) ^ [_230793, _230795, _230797, _230799] : [-(a_select2(_230799, _230795) = a_select2(_230797, _230793)), _230799 = _230797, _230795 = _230793], (869 ^ _221752) ^ [] : [-(gt(n5, n4))], (871 ^ _221752) ^ [] : [-(gt(n330, n4))], (873 ^ _221752) ^ [] : [-(gt(n410, n4))], (875 ^ _221752) ^ [] : [-(gt(n330, n5))], (877 ^ _221752) ^ [] : [-(gt(n410, n5))], (879 ^ _221752) ^ [] : [-(gt(n410, n330))], (881 ^ _221752) ^ [] : [-(gt(n4, tptp_minus_1))], (883 ^ _221752) ^ [] : [-(gt(n5, tptp_minus_1))], (885 ^ _221752) ^ [] : [-(gt(n330, tptp_minus_1))], (887 ^ _221752) ^ [] : [-(gt(n410, tptp_minus_1))], (889 ^ _221752) ^ [] : [-(gt(n0, tptp_minus_1))], (891 ^ _221752) ^ [] : [-(gt(n1, tptp_minus_1))], (893 ^ _221752) ^ [] : [-(gt(n2, tptp_minus_1))], (895 ^ _221752) ^ [] : [-(gt(n3, tptp_minus_1))], (897 ^ _221752) ^ [] : [-(gt(n4, n0))], (899 ^ _221752) ^ [] : [-(gt(n5, n0))], (901 ^ _221752) ^ [] : [-(gt(n330, n0))], (903 ^ _221752) ^ [] : [-(gt(n410, n0))], (905 ^ _221752) ^ [] : [-(gt(n1, n0))], (907 ^ _221752) ^ [] : [-(gt(n2, n0))], (909 ^ _221752) ^ [] : [-(gt(n3, n0))], (911 ^ _221752) ^ [] : [-(gt(n4, n1))], (913 ^ _221752) ^ [] : [-(gt(n5, n1))], (915 ^ _221752) ^ [] : [-(gt(n330, n1))], (917 ^ _221752) ^ [] : [-(gt(n410, n1))], (919 ^ _221752) ^ [] : [-(gt(n2, n1))], (921 ^ _221752) ^ [] : [-(gt(n3, n1))], (923 ^ _221752) ^ [] : [-(gt(n4, n2))], (925 ^ _221752) ^ [] : [-(gt(n5, n2))], (927 ^ _221752) ^ [] : [-(gt(n330, n2))], (929 ^ _221752) ^ [] : [-(gt(n410, n2))], (931 ^ _221752) ^ [] : [-(gt(n3, n2))], (933 ^ _221752) ^ [] : [-(gt(n4, n3))], (935 ^ _221752) ^ [] : [-(gt(n5, n3))], (937 ^ _221752) ^ [] : [-(gt(n330, n3))], (939 ^ _221752) ^ [] : [-(gt(n410, n3))], (941 ^ _221752) ^ [_259057] : [leq(n0, _259057), leq(_259057, n4), -(_259057 = n0), -(_259057 = n1), -(_259057 = n2), -(_259057 = n3), -(_259057 = n4)], (967 ^ _221752) ^ [_259678] : [leq(n0, _259678), leq(_259678, n5), -(_259678 = n0), -(_259678 = n1), -(_259678 = n2), -(_259678 = n3), -(_259678 = n4), -(_259678 = n5)], (997 ^ _221752) ^ [_260385] : [-(_260385 = n0), leq(n0, _260385), leq(_260385, n0)], (1007 ^ _221752) ^ [_260660] : [leq(n0, _260660), leq(_260660, n1), -(_260660 = n0), -(_260660 = n1)], (1021 ^ _221752) ^ [_261023] : [leq(n0, _261023), leq(_261023, n2), -(_261023 = n0), -(_261023 = n1), -(_261023 = n2)], (1061 ^ _221752) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (1063 ^ _221752) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (1065 ^ _221752) ^ [] : [-(succ(n0) = n1)], (1067 ^ _221752) ^ [] : [-(succ(succ(n0)) = n2)], (1069 ^ _221752) ^ [] : [-(succ(succ(succ(n0))) = n3)], (1039 ^ _221752) ^ [_261472] : [leq(n0, _261472), leq(_261472, n3), -(_261472 = n0), -(_261472 = n1), -(_261472 = n2), -(_261472 = n3)], (264 ^ _221752) ^ [_231224, _231226] : [-(gt(_231226, _231224)), -(gt(_231224, _231226)), -(_231226 = _231224)], (274 ^ _221752) ^ [_231539, _231541, _231543] : [-(gt(_231543, _231539)), gt(_231543, _231541), gt(_231541, _231539)], (284 ^ _221752) ^ [_231818] : [gt(_231818, _231818)], (286 ^ _221752) ^ [_231896] : [-(leq(_231896, _231896))], (288 ^ _221752) ^ [_232017, _232019, _232021] : [-(leq(_232021, _232017)), leq(_232021, _232019), leq(_232019, _232017)], (298 ^ _221752) ^ [_232355, _232357] : [lt(_232357, _232355), -(gt(_232355, _232357))], (304 ^ _221752) ^ [_232517, _232519] : [gt(_232517, _232519), -(lt(_232519, _232517))], (310 ^ _221752) ^ [_232758, _232760] : [geq(_232760, _232758), -(leq(_232758, _232760))], (316 ^ _221752) ^ [_232920, _232922] : [leq(_232920, _232922), -(geq(_232922, _232920))], (322 ^ _221752) ^ [_233132, _233134] : [gt(_233132, _233134), -(leq(_233134, _233132))], (328 ^ _221752) ^ [_233342, _233344] : [-(gt(_233342, _233344)), leq(_233344, _233342), -(_233344 = _233342)], (338 ^ _221752) ^ [_233673, _233675] : [leq(_233675, pred(_233673)), -(gt(_233673, _233675))], (344 ^ _221752) ^ [_233839, _233841] : [gt(_233839, _233841), -(leq(_233841, pred(_233839)))], (350 ^ _221752) ^ [_234026] : [-(gt(succ(_234026), _234026))], (352 ^ _221752) ^ [_234135, _234137] : [leq(_234137, _234135), -(leq(_234137, succ(_234135)))], (358 ^ _221752) ^ [_234378, _234380] : [leq(_234380, _234378), -(gt(succ(_234378), _234380))], (364 ^ _221752) ^ [_234544, _234546] : [gt(succ(_234544), _234546), -(leq(_234546, _234544))], (370 ^ _221752) ^ [_234760, _234762] : [leq(n0, _234762), -(leq(uniform_int_rnd(_234760, _234762), _234762))], (376 ^ _221752) ^ [_234976, _234978] : [leq(n0, _234978), -(leq(n0, uniform_int_rnd(_234976, _234978)))], (382 ^ _221752) ^ [_235220, _235222, _235224, _235226] : [-(a_select2(tptp_const_array1(dim(_235224, _235222), _235220), _235226) = _235220), leq(_235224, _235226), leq(_235226, _235222)], (392 ^ _221752) ^ [_235627, _235629, _235631, _235633, _235635, _235637, _235639] : [-(a_select3(tptp_const_array2(dim(_235637, _235635), dim(_235631, _235629), _235627), _235639, _235633) = _235627), leq(_235637, _235639), leq(_235639, _235635), leq(_235631, _235633), leq(_235633, _235629)], (410 ^ _221752) ^ [_236222, _236224] : [413 ^ _221752 : [(414 ^ _221752) ^ [] : [-(leq(n0, 411 ^ [_236222, _236224]))], (416 ^ _221752) ^ [] : [-(leq(411 ^ [_236222, _236224], _236222))], (418 ^ _221752) ^ [] : [-(leq(n0, 412 ^ [_236222, _236224]))], (420 ^ _221752) ^ [] : [-(leq(412 ^ [_236222, _236224], _236222))], (422 ^ _221752) ^ [] : [a_select3(_236224, 411 ^ [_236222, _236224], 412 ^ [_236222, _236224]) = a_select3(_236224, 412 ^ [_236222, _236224], 411 ^ [_236222, _236224])]], 423 ^ _221752 : [(424 ^ _221752) ^ [_236979, _236981] : [-(a_select3(trans(_236224), _236981, _236979) = a_select3(trans(_236224), _236979, _236981)), leq(n0, _236981), leq(_236981, _236222), leq(n0, _236979), leq(_236979, _236222)]]], (442 ^ _221752) ^ [_237526, _237528] : [445 ^ _221752 : [(446 ^ _221752) ^ [] : [-(leq(n0, 443 ^ [_237526, _237528]))], (448 ^ _221752) ^ [] : [-(leq(443 ^ [_237526, _237528], _237526))], (450 ^ _221752) ^ [] : [-(leq(n0, 444 ^ [_237526, _237528]))], (452 ^ _221752) ^ [] : [-(leq(444 ^ [_237526, _237528], _237526))], (454 ^ _221752) ^ [] : [a_select3(_237528, 443 ^ [_237526, _237528], 444 ^ [_237526, _237528]) = a_select3(_237528, 444 ^ [_237526, _237528], 443 ^ [_237526, _237528])]], 455 ^ _221752 : [(456 ^ _221752) ^ [_238283, _238285] : [-(a_select3(inv(_237528), _238285, _238283) = a_select3(inv(_237528), _238283, _238285)), leq(n0, _238285), leq(_238285, _237526), leq(n0, _238283), leq(_238283, _237526)]]], (474 ^ _221752) ^ [_238830, _238832] : [477 ^ _221752 : [(478 ^ _221752) ^ [] : [-(leq(n0, 475 ^ [_238830, _238832]))], (480 ^ _221752) ^ [] : [-(leq(475 ^ [_238830, _238832], _238830))], (482 ^ _221752) ^ [] : [-(leq(n0, 476 ^ [_238830, _238832]))], (484 ^ _221752) ^ [] : [-(leq(476 ^ [_238830, _238832], _238830))], (486 ^ _221752) ^ [] : [a_select3(_238832, 475 ^ [_238830, _238832], 476 ^ [_238830, _238832]) = a_select3(_238832, 476 ^ [_238830, _238832], 475 ^ [_238830, _238832])]], 487 ^ _221752 : [(488 ^ _221752) ^ [_239643, _239645, _239647, _239649] : [-(a_select3(tptp_update3(_238832, _239645, _239645, _239643), _239649, _239647) = a_select3(tptp_update3(_238832, _239645, _239645, _239643), _239647, _239649)), leq(n0, _239649), leq(_239649, _238830), leq(n0, _239647), leq(_239647, _238830), leq(n0, _239645), leq(_239645, _238830)]]], (514 ^ _221752) ^ [_240462, _240464, _240466] : [519 ^ _221752 : [(520 ^ _221752) ^ [] : [-(leq(n0, 517 ^ [_240462, _240464, _240466]))], (522 ^ _221752) ^ [] : [-(leq(517 ^ [_240462, _240464, _240466], _240462))], (524 ^ _221752) ^ [] : [-(leq(n0, 518 ^ [_240462, _240464, _240466]))], (526 ^ _221752) ^ [] : [-(leq(518 ^ [_240462, _240464, _240466], _240462))], (528 ^ _221752) ^ [] : [a_select3(_240466, 517 ^ [_240462, _240464, _240466], 518 ^ [_240462, _240464, _240466]) = a_select3(_240466, 518 ^ [_240462, _240464, _240466], 517 ^ [_240462, _240464, _240466])]], 531 ^ _221752 : [(532 ^ _221752) ^ [] : [-(leq(n0, 529 ^ [_240462, _240464, _240466]))], (534 ^ _221752) ^ [] : [-(leq(529 ^ [_240462, _240464, _240466], _240462))], (536 ^ _221752) ^ [] : [-(leq(n0, 530 ^ [_240462, _240464, _240466]))], (538 ^ _221752) ^ [] : [-(leq(530 ^ [_240462, _240464, _240466], _240462))], (540 ^ _221752) ^ [] : [a_select3(_240464, 529 ^ [_240462, _240464, _240466], 530 ^ [_240462, _240464, _240466]) = a_select3(_240464, 530 ^ [_240462, _240464, _240466], 529 ^ [_240462, _240464, _240466])]], 541 ^ _221752 : [(542 ^ _221752) ^ [_241971, _241973] : [-(a_select3(tptp_madd(_240466, _240464), _241973, _241971) = a_select3(tptp_madd(_240466, _240464), _241971, _241973)), leq(n0, _241973), leq(_241973, _240462), leq(n0, _241971), leq(_241971, _240462)]]], (560 ^ _221752) ^ [_242557, _242559, _242561] : [565 ^ _221752 : [(566 ^ _221752) ^ [] : [-(leq(n0, 563 ^ [_242557, _242559, _242561]))], (568 ^ _221752) ^ [] : [-(leq(563 ^ [_242557, _242559, _242561], _242557))], (570 ^ _221752) ^ [] : [-(leq(n0, 564 ^ [_242557, _242559, _242561]))], (572 ^ _221752) ^ [] : [-(leq(564 ^ [_242557, _242559, _242561], _242557))], (574 ^ _221752) ^ [] : [a_select3(_242561, 563 ^ [_242557, _242559, _242561], 564 ^ [_242557, _242559, _242561]) = a_select3(_242561, 564 ^ [_242557, _242559, _242561], 563 ^ [_242557, _242559, _242561])]], 577 ^ _221752 : [(578 ^ _221752) ^ [] : [-(leq(n0, 575 ^ [_242557, _242559, _242561]))], (580 ^ _221752) ^ [] : [-(leq(575 ^ [_242557, _242559, _242561], _242557))], (582 ^ _221752) ^ [] : [-(leq(n0, 576 ^ [_242557, _242559, _242561]))], (584 ^ _221752) ^ [] : [-(leq(576 ^ [_242557, _242559, _242561], _242557))], (586 ^ _221752) ^ [] : [a_select3(_242559, 575 ^ [_242557, _242559, _242561], 576 ^ [_242557, _242559, _242561]) = a_select3(_242559, 576 ^ [_242557, _242559, _242561], 575 ^ [_242557, _242559, _242561])]], 587 ^ _221752 : [(588 ^ _221752) ^ [_244066, _244068] : [-(a_select3(tptp_msub(_242561, _242559), _244068, _244066) = a_select3(tptp_msub(_242561, _242559), _244066, _244068)), leq(n0, _244068), leq(_244068, _242557), leq(n0, _244066), leq(_244066, _242557)]]], (606 ^ _221752) ^ [_244652, _244654, _244656] : [609 ^ _221752 : [(610 ^ _221752) ^ [] : [-(leq(n0, 607 ^ [_244652, _244654, _244656]))], (612 ^ _221752) ^ [] : [-(leq(607 ^ [_244652, _244654, _244656], _244652))], (614 ^ _221752) ^ [] : [-(leq(n0, 608 ^ [_244652, _244654, _244656]))], (616 ^ _221752) ^ [] : [-(leq(608 ^ [_244652, _244654, _244656], _244652))], (618 ^ _221752) ^ [] : [a_select3(_244654, 607 ^ [_244652, _244654, _244656], 608 ^ [_244652, _244654, _244656]) = a_select3(_244654, 608 ^ [_244652, _244654, _244656], 607 ^ [_244652, _244654, _244656])]], 619 ^ _221752 : [(620 ^ _221752) ^ [_245465, _245467] : [-(a_select3(tptp_mmul(_244656, tptp_mmul(_244654, trans(_244656))), _245467, _245465) = a_select3(tptp_mmul(_244656, tptp_mmul(_244654, trans(_244656))), _245465, _245467)), leq(n0, _245467), leq(_245467, _244652), leq(n0, _245465), leq(_245465, _244652)]]], (638 ^ _221752) ^ [_246084, _246086, _246088, _246090] : [641 ^ _221752 : [(642 ^ _221752) ^ [] : [-(leq(n0, 639 ^ [_246084, _246086, _246088, _246090]))], (644 ^ _221752) ^ [] : [-(leq(639 ^ [_246084, _246086, _246088, _246090], _246084))], (646 ^ _221752) ^ [] : [-(leq(n0, 640 ^ [_246084, _246086, _246088, _246090]))], (648 ^ _221752) ^ [] : [-(leq(640 ^ [_246084, _246086, _246088, _246090], _246084))], (650 ^ _221752) ^ [] : [a_select3(_246088, 639 ^ [_246084, _246086, _246088, _246090], 640 ^ [_246084, _246086, _246088, _246090]) = a_select3(_246088, 640 ^ [_246084, _246086, _246088, _246090], 639 ^ [_246084, _246086, _246088, _246090])]], 651 ^ _221752 : [(652 ^ _221752) ^ [_246941, _246943] : [-(a_select3(tptp_mmul(_246090, tptp_mmul(_246088, trans(_246090))), _246943, _246941) = a_select3(tptp_mmul(_246090, tptp_mmul(_246088, trans(_246090))), _246941, _246943)), leq(n0, _246943), leq(_246943, _246086), leq(n0, _246941), leq(_246941, _246086)]]], (670 ^ _221752) ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650] : [675 ^ _221752 : [(676 ^ _221752) ^ [] : [-(leq(n0, 673 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650]))], (678 ^ _221752) ^ [] : [-(leq(673 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650], _247636))], (680 ^ _221752) ^ [] : [-(leq(n0, 674 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650]))], (682 ^ _221752) ^ [] : [-(leq(674 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650], _247636))], (684 ^ _221752) ^ [] : [a_select3(_247644, 673 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650], 674 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650]) = a_select3(_247644, 674 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650], 673 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650])]], 689 ^ _221752 : [(690 ^ _221752) ^ [] : [-(leq(n0, 687 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650]))], (692 ^ _221752) ^ [] : [-(leq(687 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650], _247638))], (694 ^ _221752) ^ [] : [-(leq(n0, 688 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650]))], (696 ^ _221752) ^ [] : [-(leq(688 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650], _247638))], (698 ^ _221752) ^ [] : [a_select3(_247650, 687 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650], 688 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650]) = a_select3(_247650, 688 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650], 687 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650])]], 701 ^ _221752 : [(702 ^ _221752) ^ [] : [-(leq(n0, 699 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650]))], (704 ^ _221752) ^ [] : [-(leq(699 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650], _247638))], (706 ^ _221752) ^ [] : [-(leq(n0, 700 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650]))], (708 ^ _221752) ^ [] : [-(leq(700 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650], _247638))], (710 ^ _221752) ^ [] : [a_select3(_247640, 699 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650], 700 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650]) = a_select3(_247640, 700 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650], 699 ^ [_247636, _247638, _247640, _247642, _247644, _247646, _247648, _247650])]], 711 ^ _221752 : [(712 ^ _221752) ^ [_250564, _250566] : [-(a_select3(tptp_madd(_247650, tptp_mmul(_247648, tptp_mmul(tptp_madd(tptp_mmul(_247646, tptp_mmul(_247644, trans(_247646))), tptp_mmul(_247642, tptp_mmul(_247640, trans(_247642)))), trans(_247648)))), _250566, _250564) = a_select3(tptp_madd(_247650, tptp_mmul(_247648, tptp_mmul(tptp_madd(tptp_mmul(_247646, tptp_mmul(_247644, trans(_247646))), tptp_mmul(_247642, tptp_mmul(_247640, trans(_247642)))), trans(_247648)))), _250564, _250566)), leq(n0, _250566), leq(_250566, _247638), leq(n0, _250564), leq(_250564, _247638)]]], (730 ^ _221752) ^ [_251317] : [-(sum(n0, tptp_minus_1, _251317) = n0)], (732 ^ _221752) ^ [_251399] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _251399))], (734 ^ _221752) ^ [] : [-(succ(tptp_minus_1) = n0)], (736 ^ _221752) ^ [_251534] : [-(plus(_251534, n1) = succ(_251534))], (738 ^ _221752) ^ [_251617] : [-(plus(n1, _251617) = succ(_251617))], (740 ^ _221752) ^ [_251700] : [-(plus(_251700, n2) = succ(succ(_251700)))], (742 ^ _221752) ^ [_251785] : [-(plus(n2, _251785) = succ(succ(_251785)))], (744 ^ _221752) ^ [_251870] : [-(plus(_251870, n3) = succ(succ(succ(_251870))))], (746 ^ _221752) ^ [_251957] : [-(plus(n3, _251957) = succ(succ(succ(_251957))))], (748 ^ _221752) ^ [_252044] : [-(plus(_252044, n4) = succ(succ(succ(succ(_252044)))))], (750 ^ _221752) ^ [_252133] : [-(plus(n4, _252133) = succ(succ(succ(succ(_252133)))))], (752 ^ _221752) ^ [_252222] : [-(plus(_252222, n5) = succ(succ(succ(succ(succ(_252222))))))], (754 ^ _221752) ^ [_252313] : [-(plus(n5, _252313) = succ(succ(succ(succ(succ(_252313))))))], (756 ^ _221752) ^ [_252404] : [-(minus(_252404, n1) = pred(_252404))], (758 ^ _221752) ^ [_252487] : [-(pred(succ(_252487)) = _252487)], (760 ^ _221752) ^ [_252569] : [-(succ(pred(_252569)) = _252569)], (762 ^ _221752) ^ [_252709, _252711] : [leq(succ(_252711), succ(_252709)), -(leq(_252711, _252709))], (768 ^ _221752) ^ [_252879, _252881] : [leq(_252881, _252879), -(leq(succ(_252881), succ(_252879)))], (774 ^ _221752) ^ [_253099, _253101] : [leq(succ(_253101), _253099), -(gt(_253099, _253101))], (780 ^ _221752) ^ [_253313, _253315] : [leq(minus(_253315, _253313), _253315), -(leq(n0, _253313))], (786 ^ _221752) ^ [_253542, _253544, _253546, _253548] : [-(a_select3(tptp_update3(_253548, _253546, _253544, _253542), _253546, _253544) = _253542)], (788 ^ _221752) ^ [_253734, _253736, _253738, _253740, _253742, _253744, _253746] : [-(a_select3(tptp_update3(_253738, _253746, _253744, _253734), _253742, _253740) = _253736), -(_253746 = _253742), _253744 = _253740, a_select3(_253738, _253742, _253740) = _253736], (802 ^ _221752) ^ [_254277, _254279, _254281, _254283, _254285, _254287] : [-(a_select3(tptp_update3(_254279, _254283, _254281, _254277), _254287, _254285) = _254277), 807 ^ _221752 : [(808 ^ _221752) ^ [] : [-(leq(n0, 805 ^ [_254277, _254279, _254281, _254283, _254285, _254287]))], (810 ^ _221752) ^ [] : [-(leq(n0, 806 ^ [_254277, _254279, _254281, _254283, _254285, _254287]))], (812 ^ _221752) ^ [] : [-(leq(805 ^ [_254277, _254279, _254281, _254283, _254285, _254287], _254283))], (814 ^ _221752) ^ [] : [-(leq(806 ^ [_254277, _254279, _254281, _254283, _254285, _254287], _254281))], (816 ^ _221752) ^ [] : [a_select3(_254279, 805 ^ [_254277, _254279, _254281, _254283, _254285, _254287], 806 ^ [_254277, _254279, _254281, _254283, _254285, _254287]) = _254277]], leq(n0, _254287), leq(_254287, _254283), leq(n0, _254285), leq(_254285, _254281)], (834 ^ _221752) ^ [_255619, _255621, _255623] : [-(a_select2(tptp_update2(_255623, _255621, _255619), _255621) = _255619)], (836 ^ _221752) ^ [_255779, _255781, _255783, _255785, _255787] : [-(a_select2(tptp_update2(_255783, _255787, _255779), _255785) = _255781), -(_255787 = _255785), a_select2(_255783, _255785) = _255781], (865 ^ _221752) ^ [] : [-(true)], (867 ^ _221752) ^ [] : [def = use], (846 ^ _221752) ^ [_256159, _256161, _256163, _256165] : [-(a_select2(tptp_update2(_256161, _256163, _256159), _256165) = _256159), 850 ^ _221752 : [(851 ^ _221752) ^ [] : [-(leq(n0, 849 ^ [_256159, _256161, _256163, _256165]))], (853 ^ _221752) ^ [] : [-(leq(849 ^ [_256159, _256161, _256163, _256165], _256163))], (855 ^ _221752) ^ [] : [a_select2(_256161, 849 ^ [_256159, _256161, _256163, _256165]) = _256159]], leq(n0, _256165), leq(_256165, _256163)]], input).
% 0.26/1.37 ncf('1',plain,[init = init, a_select3(simplex7_init, pv1376, n0) = init, a_select3(simplex7_init, pv1376, n1) = init, a_select3(simplex7_init, pv1376, n2) = init, a_select3(tptp_const_array2(dim(n0, minus(n410, n1)), dim(n0, minus(n330, n1)), init), pv19, pv20) = init, leq(n0, pv19), leq(n0, pv1376), leq(pv19, minus(n410, n1)), leq(pv1376, n3), 1161 : a_select3(simplex7_init, 1155 ^ [], 1150 ^ []) = init, 1168 : a_select2(s_values7_init, 1162 ^ []) = init],start(1113 ^ 0)).
% 0.26/1.37 ncf('1.1',plain,[-(init = init)],extension(1071 ^ 1)).
% 0.26/1.37 ncf('1.2',plain,[-(a_select3(simplex7_init, pv1376, n0) = init), 1093 : leq(n0, pv1376), 1093 : leq(pv1376, n3), 1093 : leq(n0, n0), 1093 : leq(n0, n2)],extension(1085 ^ 1,bind([[_262895, _263123], [n0, pv1376]]))).
% 0.26/1.37 ncf('1.2.1',plain,[-(leq(n0, pv1376))],extension(1077 ^ 4)).
% 0.26/1.37 ncf('1.2.2',plain,[-(leq(pv1376, n3))],extension(1083 ^ 4)).
% 0.26/1.37 ncf('1.2.3',plain,[-(leq(n0, n0))],extension(286 ^ 2,bind([[_231896], [n0]]))).
% 0.26/1.37 ncf('1.2.4',plain,[-(leq(n0, n2)), gt(n2, n0)],extension(322 ^ 2,bind([[_233132, _233134], [n2, n0]]))).
% 0.26/1.37 ncf('1.2.4.1',plain,[-(gt(n2, n0))],extension(907 ^ 3)).
% 0.26/1.37 ncf('1.3',plain,[-(a_select3(simplex7_init, pv1376, n1) = init), 1093 : leq(n0, pv1376), 1093 : leq(pv1376, n3), 1093 : leq(n0, n1), 1093 : leq(n1, n2)],extension(1085 ^ 1,bind([[_262895, _263123], [n1, pv1376]]))).
% 0.26/1.37 ncf('1.3.1',plain,[-(leq(n0, pv1376))],extension(1077 ^ 4)).
% 0.26/1.37 ncf('1.3.2',plain,[-(leq(pv1376, n3))],extension(1083 ^ 4)).
% 0.26/1.37 ncf('1.3.3',plain,[-(leq(n0, n1)), gt(n1, n0)],extension(322 ^ 2,bind([[_233132, _233134], [n1, n0]]))).
% 0.26/1.37 ncf('1.3.3.1',plain,[-(gt(n1, n0))],extension(905 ^ 3)).
% 0.26/1.37 ncf('1.3.4',plain,[-(leq(n1, n2)), gt(n2, n1)],extension(322 ^ 2,bind([[_233132, _233134], [n2, n1]]))).
% 0.26/1.37 ncf('1.3.4.1',plain,[-(gt(n2, n1))],extension(919 ^ 3)).
% 0.26/1.37 ncf('1.4',plain,[-(a_select3(simplex7_init, pv1376, n2) = init), 1093 : leq(n0, pv1376), 1093 : leq(pv1376, n3), 1093 : leq(n0, n2), 1093 : leq(n2, n2)],extension(1085 ^ 1,bind([[_262895, _263123], [n2, pv1376]]))).
% 0.26/1.37 ncf('1.4.1',plain,[-(leq(n0, pv1376))],extension(1077 ^ 4)).
% 0.26/1.37 ncf('1.4.2',plain,[-(leq(pv1376, n3))],extension(1083 ^ 4)).
% 0.26/1.37 ncf('1.4.3',plain,[-(leq(n0, n2)), gt(n2, n0)],extension(322 ^ 2,bind([[_233132, _233134], [n2, n0]]))).
% 0.26/1.37 ncf('1.4.3.1',plain,[-(gt(n2, n0))],extension(907 ^ 3)).
% 0.26/1.37 ncf('1.4.4',plain,[-(leq(n2, n2))],extension(286 ^ 2,bind([[_231896], [n2]]))).
% 0.26/1.37 ncf('1.5',plain,[-(a_select3(tptp_const_array2(dim(n0, minus(n410, n1)), dim(n0, minus(n330, n1)), init), pv19, pv20) = init), leq(n0, pv19), leq(pv19, minus(n410, n1)), leq(n0, pv20), leq(pv20, minus(n330, n1))],extension(392 ^ 1,bind([[_235627, _235629, _235631, _235633, _235635, _235637, _235639], [init, minus(n330, n1), n0, pv20, minus(n410, n1), n0, pv19]]))).
% 0.26/1.37 ncf('1.5.1',plain,[-(leq(n0, pv19))],extension(1073 ^ 2)).
% 0.26/1.37 ncf('1.5.2',plain,[-(leq(pv19, minus(n410, n1)))],extension(1079 ^ 2)).
% 0.26/1.37 ncf('1.5.3',plain,[-(leq(n0, pv20))],extension(1075 ^ 2)).
% 0.26/1.37 ncf('1.5.4',plain,[-(leq(pv20, minus(n330, n1)))],extension(1081 ^ 2)).
% 0.26/1.37 ncf('1.6',plain,[-(leq(n0, pv19))],extension(1073 ^ 1)).
% 0.26/1.37 ncf('1.7',plain,[-(leq(n0, pv1376))],extension(1077 ^ 1)).
% 0.26/1.37 ncf('1.8',plain,[-(leq(pv19, minus(n410, n1)))],extension(1079 ^ 1)).
% 0.26/1.37 ncf('1.9',plain,[-(leq(pv1376, n3))],extension(1083 ^ 1)).
% 0.26/1.37 ncf('1.10',plain,[-(a_select3(simplex7_init, 1155 ^ [], 1150 ^ []) = init), 1093 : leq(n0, 1155 ^ []), 1093 : leq(1155 ^ [], n3), 1093 : leq(n0, 1150 ^ []), 1093 : leq(1150 ^ [], n2)],extension(1085 ^ 3,bind([[_262895, _263123], [1150 ^ [], 1155 ^ []]]))).
% 0.26/1.37 ncf('1.10.1',plain,[-(leq(n0, 1155 ^ []))],extension(1157 ^ 6)).
% 0.26/1.37 ncf('1.10.2',plain,[-(leq(1155 ^ [], n3))],extension(1159 ^ 6)).
% 0.26/1.37 ncf('1.10.3',plain,[-(leq(n0, 1150 ^ []))],extension(1152 ^ 4)).
% 0.26/1.37 ncf('1.10.4',plain,[-(leq(1150 ^ [], n2))],extension(1154 ^ 4)).
% 0.26/1.37 ncf('1.11',plain,[-(a_select2(s_values7_init, 1162 ^ []) = init), leq(n0, 1162 ^ []), leq(1162 ^ [], minus(pv1376, n1))],extension(1103 ^ 3,bind([[_263405], [1162 ^ []]]))).
% 0.26/1.37 ncf('1.11.1',plain,[-(leq(n0, 1162 ^ []))],extension(1164 ^ 4)).
% 0.26/1.37 ncf('1.11.2',plain,[-(leq(1162 ^ [], minus(pv1376, n1)))],extension(1166 ^ 4)).
% 0.26/1.37 %-----------------------------------------------------
% 0.26/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------