%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV193+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n032.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:09 EDT 2023
% Result : Theorem 0.22s 1.31s
% Output : Proof 0.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : SWV193+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.00/0.10 % Command : nanocop.sh %s %d
% 0.08/0.29 % Computer : n032.cluster.edu
% 0.08/0.29 % Model : x86_64 x86_64
% 0.08/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.29 % Memory : 8042.1875MB
% 0.08/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.29 % CPULimit : 300
% 0.08/0.29 % WCLimit : 300
% 0.08/0.29 % DateTime : Fri May 19 02:26:50 EDT 2023
% 0.08/0.29 % CPUTime :
% 0.22/1.31
% 0.22/1.31 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.22/1.31 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.22/1.31 %-----------------------------------------------------
% 0.22/1.31 ncf(matrix, plain, [(1155 ^ _216792) ^ [] : [-(leq(n0, 1152 ^ []))], (1157 ^ _216792) ^ [] : [-(leq(n0, 1153 ^ []))], (1159 ^ _216792) ^ [] : [-(leq(1152 ^ [], n2))], (1161 ^ _216792) ^ [] : [-(leq(1153 ^ [], pred(pv5)))], (1181 ^ _216792) ^ [] : [a_select3(z_defuse, 1152 ^ [], 1153 ^ []) = use], (1163 ^ _216792) ^ [] : [n0 = 1152 ^ [], pv5 = 1153 ^ []], (1169 ^ _216792) ^ [] : [n1 = 1152 ^ [], pv5 = 1153 ^ []], (1175 ^ _216792) ^ [] : [n2 = 1152 ^ [], pv5 = 1153 ^ []], (1055 ^ _216792) ^ [] : [-(a_select2(rho_defuse, n0) = use)], (1057 ^ _216792) ^ [] : [-(a_select2(rho_defuse, n1) = use)], (1059 ^ _216792) ^ [] : [-(a_select2(rho_defuse, n2) = use)], (1061 ^ _216792) ^ [] : [-(a_select2(sigma_defuse, n0) = use)], (1063 ^ _216792) ^ [] : [-(a_select2(sigma_defuse, n1) = use)], (1065 ^ _216792) ^ [] : [-(a_select2(sigma_defuse, n2) = use)], (1067 ^ _216792) ^ [] : [-(a_select2(sigma_defuse, n3) = use)], (1069 ^ _216792) ^ [] : [-(a_select2(sigma_defuse, n4) = use)], (1071 ^ _216792) ^ [] : [-(a_select2(sigma_defuse, n5) = use)], (1073 ^ _216792) ^ [] : [-(a_select3(u_defuse, n0, n0) = use)], (1075 ^ _216792) ^ [] : [-(a_select3(u_defuse, n1, n0) = use)], (1077 ^ _216792) ^ [] : [-(a_select3(u_defuse, n2, n0) = use)], (1079 ^ _216792) ^ [] : [-(a_select2(xinit_defuse, n3) = use)], (1081 ^ _216792) ^ [] : [-(a_select2(xinit_defuse, n4) = use)], (1083 ^ _216792) ^ [] : [-(a_select2(xinit_defuse, n5) = use)], (1085 ^ _216792) ^ [] : [-(a_select2(xinit_mean_defuse, n0) = use)], (1087 ^ _216792) ^ [] : [-(a_select2(xinit_mean_defuse, n1) = use)], (1089 ^ _216792) ^ [] : [-(a_select2(xinit_mean_defuse, n2) = use)], (1091 ^ _216792) ^ [] : [-(a_select2(xinit_mean_defuse, n3) = use)], (1093 ^ _216792) ^ [] : [-(a_select2(xinit_mean_defuse, n4) = use)], (1095 ^ _216792) ^ [] : [-(a_select2(xinit_mean_defuse, n5) = use)], (1097 ^ _216792) ^ [] : [-(a_select2(xinit_noise_defuse, n0) = use)], (1099 ^ _216792) ^ [] : [-(a_select2(xinit_noise_defuse, n1) = use)], (1101 ^ _216792) ^ [] : [-(a_select2(xinit_noise_defuse, n2) = use)], (1103 ^ _216792) ^ [] : [-(a_select2(xinit_noise_defuse, n3) = use)], (1105 ^ _216792) ^ [] : [-(a_select2(xinit_noise_defuse, n4) = use)], (1107 ^ _216792) ^ [] : [-(a_select2(xinit_noise_defuse, n5) = use)], (1109 ^ _216792) ^ [] : [-(leq(n0, pv5))], (1111 ^ _216792) ^ [] : [-(leq(pv5, n0))], (1113 ^ _216792) ^ [] : [-(leq(pv5, n998))], (1115 ^ _216792) ^ [] : [-(gt(pv5, n0))], (1117 ^ _216792) ^ [_258765, _258767] : [-(a_select3(u_defuse, _258767, _258765) = use), leq(n0, _258767), leq(n0, _258765), leq(_258767, n2), leq(_258765, pred(pv5))], (1135 ^ _216792) ^ [_259230, _259232] : [-(a_select3(z_defuse, _259232, _259230) = use), leq(n0, _259232), leq(n0, _259230), leq(_259232, n2), leq(_259230, pred(pv5))], (2 ^ _216792) ^ [_216936] : [-(_216936 = _216936)], (4 ^ _216792) ^ [_217043, _217045] : [_217045 = _217043, -(_217043 = _217045)], (10 ^ _216792) ^ [_217247, _217249, _217251] : [-(_217251 = _217247), _217251 = _217249, _217249 = _217247], (20 ^ _216792) ^ [_217588, _217590, _217592, _217594] : [-(lt(_217592, _217588)), lt(_217594, _217590), _217594 = _217592, _217590 = _217588], (34 ^ _216792) ^ [_218032, _218034, _218036, _218038] : [-(geq(_218036, _218032)), geq(_218038, _218034), _218038 = _218036, _218034 = _218032], (48 ^ _216792) ^ [_218476, _218478, _218480, _218482] : [-(gt(_218480, _218476)), gt(_218482, _218478), _218482 = _218480, _218478 = _218476], (62 ^ _216792) ^ [_218900, _218902, _218904, _218906] : [-(leq(_218904, _218900)), leq(_218906, _218902), _218906 = _218904, _218902 = _218900], (76 ^ _216792) ^ [_219356, _219358, _219360, _219362] : [-(uniform_int_rnd(_219362, _219358) = uniform_int_rnd(_219360, _219356)), _219362 = _219360, _219358 = _219356], (86 ^ _216792) ^ [_219715, _219717, _219719, _219721] : [-(tptp_const_array1(_219721, _219717) = tptp_const_array1(_219719, _219715)), _219721 = _219719, _219717 = _219715], (96 ^ _216792) ^ [_220102, _220104, _220106, _220108, _220110, _220112] : [-(tptp_const_array2(_220112, _220108, _220104) = tptp_const_array2(_220110, _220106, _220102)), _220112 = _220110, _220108 = _220106, _220104 = _220102], (110 ^ _216792) ^ [_220590, _220592, _220594, _220596] : [-(dim(_220596, _220592) = dim(_220594, _220590)), _220596 = _220594, _220592 = _220590], (120 ^ _216792) ^ [_220921, _220923] : [_220923 = _220921, -(inv(_220923) = inv(_220921))], (126 ^ _216792) ^ [_221167, _221169, _221171, _221173] : [-(tptp_msub(_221173, _221169) = tptp_msub(_221171, _221167)), _221173 = _221171, _221169 = _221167], (136 ^ _216792) ^ [_221526, _221528, _221530, _221532] : [-(tptp_madd(_221532, _221528) = tptp_madd(_221530, _221526)), _221532 = _221530, _221528 = _221526], (146 ^ _216792) ^ [_221885, _221887, _221889, _221891] : [-(tptp_mmul(_221891, _221887) = tptp_mmul(_221889, _221885)), _221891 = _221889, _221887 = _221885], (156 ^ _216792) ^ [_222216, _222218] : [_222218 = _222216, -(trans(_222218) = trans(_222216))], (162 ^ _216792) ^ [_222490, _222492, _222494, _222496, _222498, _222500] : [-(sum(_222500, _222496, _222492) = sum(_222498, _222494, _222490)), _222500 = _222498, _222496 = _222494, _222492 = _222490], (176 ^ _216792) ^ [_222978, _222980, _222982, _222984] : [-(plus(_222984, _222980) = plus(_222982, _222978)), _222984 = _222982, _222980 = _222978], (186 ^ _216792) ^ [_223337, _223339, _223341, _223343] : [-(minus(_223343, _223339) = minus(_223341, _223337)), _223343 = _223341, _223339 = _223337], (196 ^ _216792) ^ [_223752, _223754, _223756, _223758, _223760, _223762, _223764, _223766] : [-(tptp_update3(_223766, _223762, _223758, _223754) = tptp_update3(_223764, _223760, _223756, _223752)), _223766 = _223764, _223762 = _223760, _223758 = _223756, _223754 = _223752], (214 ^ _216792) ^ [_224413, _224415, _224417, _224419, _224421, _224423] : [-(tptp_update2(_224423, _224419, _224415) = tptp_update2(_224421, _224417, _224413)), _224423 = _224421, _224419 = _224417, _224415 = _224413], (228 ^ _216792) ^ [_224873, _224875] : [_224875 = _224873, -(succ(_224875) = succ(_224873))], (234 ^ _216792) ^ [_225119, _225121, _225123, _225125] : [-(a_select2(_225125, _225121) = a_select2(_225123, _225119)), _225125 = _225123, _225121 = _225119], (244 ^ _216792) ^ [_225450, _225452] : [_225452 = _225450, -(pred(_225452) = pred(_225450))], (250 ^ _216792) ^ [_225704, _225706, _225708, _225710, _225712, _225714] : [-(a_select3(_225714, _225710, _225706) = a_select3(_225712, _225708, _225704)), _225714 = _225712, _225710 = _225708, _225706 = _225704], (869 ^ _216792) ^ [] : [-(gt(n5, n4))], (871 ^ _216792) ^ [] : [-(gt(n998, n4))], (873 ^ _216792) ^ [] : [-(gt(n998, n5))], (875 ^ _216792) ^ [] : [-(gt(n4, tptp_minus_1))], (877 ^ _216792) ^ [] : [-(gt(n5, tptp_minus_1))], (879 ^ _216792) ^ [] : [-(gt(n998, tptp_minus_1))], (881 ^ _216792) ^ [] : [-(gt(n0, tptp_minus_1))], (883 ^ _216792) ^ [] : [-(gt(n1, tptp_minus_1))], (885 ^ _216792) ^ [] : [-(gt(n2, tptp_minus_1))], (887 ^ _216792) ^ [] : [-(gt(n3, tptp_minus_1))], (889 ^ _216792) ^ [] : [-(gt(n4, n0))], (891 ^ _216792) ^ [] : [-(gt(n5, n0))], (893 ^ _216792) ^ [] : [-(gt(n998, n0))], (895 ^ _216792) ^ [] : [-(gt(n1, n0))], (897 ^ _216792) ^ [] : [-(gt(n2, n0))], (899 ^ _216792) ^ [] : [-(gt(n3, n0))], (901 ^ _216792) ^ [] : [-(gt(n4, n1))], (903 ^ _216792) ^ [] : [-(gt(n5, n1))], (905 ^ _216792) ^ [] : [-(gt(n998, n1))], (907 ^ _216792) ^ [] : [-(gt(n2, n1))], (909 ^ _216792) ^ [] : [-(gt(n3, n1))], (911 ^ _216792) ^ [] : [-(gt(n4, n2))], (913 ^ _216792) ^ [] : [-(gt(n5, n2))], (915 ^ _216792) ^ [] : [-(gt(n998, n2))], (917 ^ _216792) ^ [] : [-(gt(n3, n2))], (919 ^ _216792) ^ [] : [-(gt(n4, n3))], (921 ^ _216792) ^ [] : [-(gt(n5, n3))], (923 ^ _216792) ^ [] : [-(gt(n998, n3))], (925 ^ _216792) ^ [_253673] : [leq(n0, _253673), leq(_253673, n4), -(_253673 = n0), -(_253673 = n1), -(_253673 = n2), -(_253673 = n3), -(_253673 = n4)], (951 ^ _216792) ^ [_254294] : [leq(n0, _254294), leq(_254294, n5), -(_254294 = n0), -(_254294 = n1), -(_254294 = n2), -(_254294 = n3), -(_254294 = n4), -(_254294 = n5)], (981 ^ _216792) ^ [_255001] : [-(_255001 = n0), leq(n0, _255001), leq(_255001, n0)], (991 ^ _216792) ^ [_255276] : [leq(n0, _255276), leq(_255276, n1), -(_255276 = n0), -(_255276 = n1)], (1005 ^ _216792) ^ [_255639] : [leq(n0, _255639), leq(_255639, n2), -(_255639 = n0), -(_255639 = n1), -(_255639 = n2)], (1045 ^ _216792) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (1047 ^ _216792) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (1049 ^ _216792) ^ [] : [-(succ(n0) = n1)], (1051 ^ _216792) ^ [] : [-(succ(succ(n0)) = n2)], (1053 ^ _216792) ^ [] : [-(succ(succ(succ(n0))) = n3)], (1023 ^ _216792) ^ [_256088] : [leq(n0, _256088), leq(_256088, n3), -(_256088 = n0), -(_256088 = n1), -(_256088 = n2), -(_256088 = n3)], (264 ^ _216792) ^ [_226264, _226266] : [-(gt(_226266, _226264)), -(gt(_226264, _226266)), -(_226266 = _226264)], (274 ^ _216792) ^ [_226579, _226581, _226583] : [-(gt(_226583, _226579)), gt(_226583, _226581), gt(_226581, _226579)], (284 ^ _216792) ^ [_226858] : [gt(_226858, _226858)], (286 ^ _216792) ^ [_226936] : [-(leq(_226936, _226936))], (288 ^ _216792) ^ [_227057, _227059, _227061] : [-(leq(_227061, _227057)), leq(_227061, _227059), leq(_227059, _227057)], (298 ^ _216792) ^ [_227395, _227397] : [lt(_227397, _227395), -(gt(_227395, _227397))], (304 ^ _216792) ^ [_227557, _227559] : [gt(_227557, _227559), -(lt(_227559, _227557))], (310 ^ _216792) ^ [_227798, _227800] : [geq(_227800, _227798), -(leq(_227798, _227800))], (316 ^ _216792) ^ [_227960, _227962] : [leq(_227960, _227962), -(geq(_227962, _227960))], (322 ^ _216792) ^ [_228172, _228174] : [gt(_228172, _228174), -(leq(_228174, _228172))], (328 ^ _216792) ^ [_228382, _228384] : [-(gt(_228382, _228384)), leq(_228384, _228382), -(_228384 = _228382)], (338 ^ _216792) ^ [_228713, _228715] : [leq(_228715, pred(_228713)), -(gt(_228713, _228715))], (344 ^ _216792) ^ [_228879, _228881] : [gt(_228879, _228881), -(leq(_228881, pred(_228879)))], (350 ^ _216792) ^ [_229066] : [-(gt(succ(_229066), _229066))], (352 ^ _216792) ^ [_229175, _229177] : [leq(_229177, _229175), -(leq(_229177, succ(_229175)))], (358 ^ _216792) ^ [_229418, _229420] : [leq(_229420, _229418), -(gt(succ(_229418), _229420))], (364 ^ _216792) ^ [_229584, _229586] : [gt(succ(_229584), _229586), -(leq(_229586, _229584))], (370 ^ _216792) ^ [_229800, _229802] : [leq(n0, _229802), -(leq(uniform_int_rnd(_229800, _229802), _229802))], (376 ^ _216792) ^ [_230016, _230018] : [leq(n0, _230018), -(leq(n0, uniform_int_rnd(_230016, _230018)))], (382 ^ _216792) ^ [_230260, _230262, _230264, _230266] : [-(a_select2(tptp_const_array1(dim(_230264, _230262), _230260), _230266) = _230260), leq(_230264, _230266), leq(_230266, _230262)], (392 ^ _216792) ^ [_230667, _230669, _230671, _230673, _230675, _230677, _230679] : [-(a_select3(tptp_const_array2(dim(_230677, _230675), dim(_230671, _230669), _230667), _230679, _230673) = _230667), leq(_230677, _230679), leq(_230679, _230675), leq(_230671, _230673), leq(_230673, _230669)], (410 ^ _216792) ^ [_231262, _231264] : [413 ^ _216792 : [(414 ^ _216792) ^ [] : [-(leq(n0, 411 ^ [_231262, _231264]))], (416 ^ _216792) ^ [] : [-(leq(411 ^ [_231262, _231264], _231262))], (418 ^ _216792) ^ [] : [-(leq(n0, 412 ^ [_231262, _231264]))], (420 ^ _216792) ^ [] : [-(leq(412 ^ [_231262, _231264], _231262))], (422 ^ _216792) ^ [] : [a_select3(_231264, 411 ^ [_231262, _231264], 412 ^ [_231262, _231264]) = a_select3(_231264, 412 ^ [_231262, _231264], 411 ^ [_231262, _231264])]], 423 ^ _216792 : [(424 ^ _216792) ^ [_232019, _232021] : [-(a_select3(trans(_231264), _232021, _232019) = a_select3(trans(_231264), _232019, _232021)), leq(n0, _232021), leq(_232021, _231262), leq(n0, _232019), leq(_232019, _231262)]]], (442 ^ _216792) ^ [_232566, _232568] : [445 ^ _216792 : [(446 ^ _216792) ^ [] : [-(leq(n0, 443 ^ [_232566, _232568]))], (448 ^ _216792) ^ [] : [-(leq(443 ^ [_232566, _232568], _232566))], (450 ^ _216792) ^ [] : [-(leq(n0, 444 ^ [_232566, _232568]))], (452 ^ _216792) ^ [] : [-(leq(444 ^ [_232566, _232568], _232566))], (454 ^ _216792) ^ [] : [a_select3(_232568, 443 ^ [_232566, _232568], 444 ^ [_232566, _232568]) = a_select3(_232568, 444 ^ [_232566, _232568], 443 ^ [_232566, _232568])]], 455 ^ _216792 : [(456 ^ _216792) ^ [_233323, _233325] : [-(a_select3(inv(_232568), _233325, _233323) = a_select3(inv(_232568), _233323, _233325)), leq(n0, _233325), leq(_233325, _232566), leq(n0, _233323), leq(_233323, _232566)]]], (474 ^ _216792) ^ [_233870, _233872] : [477 ^ _216792 : [(478 ^ _216792) ^ [] : [-(leq(n0, 475 ^ [_233870, _233872]))], (480 ^ _216792) ^ [] : [-(leq(475 ^ [_233870, _233872], _233870))], (482 ^ _216792) ^ [] : [-(leq(n0, 476 ^ [_233870, _233872]))], (484 ^ _216792) ^ [] : [-(leq(476 ^ [_233870, _233872], _233870))], (486 ^ _216792) ^ [] : [a_select3(_233872, 475 ^ [_233870, _233872], 476 ^ [_233870, _233872]) = a_select3(_233872, 476 ^ [_233870, _233872], 475 ^ [_233870, _233872])]], 487 ^ _216792 : [(488 ^ _216792) ^ [_234683, _234685, _234687, _234689] : [-(a_select3(tptp_update3(_233872, _234685, _234685, _234683), _234689, _234687) = a_select3(tptp_update3(_233872, _234685, _234685, _234683), _234687, _234689)), leq(n0, _234689), leq(_234689, _233870), leq(n0, _234687), leq(_234687, _233870), leq(n0, _234685), leq(_234685, _233870)]]], (514 ^ _216792) ^ [_235502, _235504, _235506] : [519 ^ _216792 : [(520 ^ _216792) ^ [] : [-(leq(n0, 517 ^ [_235502, _235504, _235506]))], (522 ^ _216792) ^ [] : [-(leq(517 ^ [_235502, _235504, _235506], _235502))], (524 ^ _216792) ^ [] : [-(leq(n0, 518 ^ [_235502, _235504, _235506]))], (526 ^ _216792) ^ [] : [-(leq(518 ^ [_235502, _235504, _235506], _235502))], (528 ^ _216792) ^ [] : [a_select3(_235506, 517 ^ [_235502, _235504, _235506], 518 ^ [_235502, _235504, _235506]) = a_select3(_235506, 518 ^ [_235502, _235504, _235506], 517 ^ [_235502, _235504, _235506])]], 531 ^ _216792 : [(532 ^ _216792) ^ [] : [-(leq(n0, 529 ^ [_235502, _235504, _235506]))], (534 ^ _216792) ^ [] : [-(leq(529 ^ [_235502, _235504, _235506], _235502))], (536 ^ _216792) ^ [] : [-(leq(n0, 530 ^ [_235502, _235504, _235506]))], (538 ^ _216792) ^ [] : [-(leq(530 ^ [_235502, _235504, _235506], _235502))], (540 ^ _216792) ^ [] : [a_select3(_235504, 529 ^ [_235502, _235504, _235506], 530 ^ [_235502, _235504, _235506]) = a_select3(_235504, 530 ^ [_235502, _235504, _235506], 529 ^ [_235502, _235504, _235506])]], 541 ^ _216792 : [(542 ^ _216792) ^ [_237011, _237013] : [-(a_select3(tptp_madd(_235506, _235504), _237013, _237011) = a_select3(tptp_madd(_235506, _235504), _237011, _237013)), leq(n0, _237013), leq(_237013, _235502), leq(n0, _237011), leq(_237011, _235502)]]], (560 ^ _216792) ^ [_237597, _237599, _237601] : [565 ^ _216792 : [(566 ^ _216792) ^ [] : [-(leq(n0, 563 ^ [_237597, _237599, _237601]))], (568 ^ _216792) ^ [] : [-(leq(563 ^ [_237597, _237599, _237601], _237597))], (570 ^ _216792) ^ [] : [-(leq(n0, 564 ^ [_237597, _237599, _237601]))], (572 ^ _216792) ^ [] : [-(leq(564 ^ [_237597, _237599, _237601], _237597))], (574 ^ _216792) ^ [] : [a_select3(_237601, 563 ^ [_237597, _237599, _237601], 564 ^ [_237597, _237599, _237601]) = a_select3(_237601, 564 ^ [_237597, _237599, _237601], 563 ^ [_237597, _237599, _237601])]], 577 ^ _216792 : [(578 ^ _216792) ^ [] : [-(leq(n0, 575 ^ [_237597, _237599, _237601]))], (580 ^ _216792) ^ [] : [-(leq(575 ^ [_237597, _237599, _237601], _237597))], (582 ^ _216792) ^ [] : [-(leq(n0, 576 ^ [_237597, _237599, _237601]))], (584 ^ _216792) ^ [] : [-(leq(576 ^ [_237597, _237599, _237601], _237597))], (586 ^ _216792) ^ [] : [a_select3(_237599, 575 ^ [_237597, _237599, _237601], 576 ^ [_237597, _237599, _237601]) = a_select3(_237599, 576 ^ [_237597, _237599, _237601], 575 ^ [_237597, _237599, _237601])]], 587 ^ _216792 : [(588 ^ _216792) ^ [_239106, _239108] : [-(a_select3(tptp_msub(_237601, _237599), _239108, _239106) = a_select3(tptp_msub(_237601, _237599), _239106, _239108)), leq(n0, _239108), leq(_239108, _237597), leq(n0, _239106), leq(_239106, _237597)]]], (606 ^ _216792) ^ [_239692, _239694, _239696] : [609 ^ _216792 : [(610 ^ _216792) ^ [] : [-(leq(n0, 607 ^ [_239692, _239694, _239696]))], (612 ^ _216792) ^ [] : [-(leq(607 ^ [_239692, _239694, _239696], _239692))], (614 ^ _216792) ^ [] : [-(leq(n0, 608 ^ [_239692, _239694, _239696]))], (616 ^ _216792) ^ [] : [-(leq(608 ^ [_239692, _239694, _239696], _239692))], (618 ^ _216792) ^ [] : [a_select3(_239694, 607 ^ [_239692, _239694, _239696], 608 ^ [_239692, _239694, _239696]) = a_select3(_239694, 608 ^ [_239692, _239694, _239696], 607 ^ [_239692, _239694, _239696])]], 619 ^ _216792 : [(620 ^ _216792) ^ [_240505, _240507] : [-(a_select3(tptp_mmul(_239696, tptp_mmul(_239694, trans(_239696))), _240507, _240505) = a_select3(tptp_mmul(_239696, tptp_mmul(_239694, trans(_239696))), _240505, _240507)), leq(n0, _240507), leq(_240507, _239692), leq(n0, _240505), leq(_240505, _239692)]]], (638 ^ _216792) ^ [_241124, _241126, _241128, _241130] : [641 ^ _216792 : [(642 ^ _216792) ^ [] : [-(leq(n0, 639 ^ [_241124, _241126, _241128, _241130]))], (644 ^ _216792) ^ [] : [-(leq(639 ^ [_241124, _241126, _241128, _241130], _241124))], (646 ^ _216792) ^ [] : [-(leq(n0, 640 ^ [_241124, _241126, _241128, _241130]))], (648 ^ _216792) ^ [] : [-(leq(640 ^ [_241124, _241126, _241128, _241130], _241124))], (650 ^ _216792) ^ [] : [a_select3(_241128, 639 ^ [_241124, _241126, _241128, _241130], 640 ^ [_241124, _241126, _241128, _241130]) = a_select3(_241128, 640 ^ [_241124, _241126, _241128, _241130], 639 ^ [_241124, _241126, _241128, _241130])]], 651 ^ _216792 : [(652 ^ _216792) ^ [_241981, _241983] : [-(a_select3(tptp_mmul(_241130, tptp_mmul(_241128, trans(_241130))), _241983, _241981) = a_select3(tptp_mmul(_241130, tptp_mmul(_241128, trans(_241130))), _241981, _241983)), leq(n0, _241983), leq(_241983, _241126), leq(n0, _241981), leq(_241981, _241126)]]], (670 ^ _216792) ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690] : [675 ^ _216792 : [(676 ^ _216792) ^ [] : [-(leq(n0, 673 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690]))], (678 ^ _216792) ^ [] : [-(leq(673 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690], _242676))], (680 ^ _216792) ^ [] : [-(leq(n0, 674 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690]))], (682 ^ _216792) ^ [] : [-(leq(674 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690], _242676))], (684 ^ _216792) ^ [] : [a_select3(_242684, 673 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690], 674 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690]) = a_select3(_242684, 674 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690], 673 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690])]], 689 ^ _216792 : [(690 ^ _216792) ^ [] : [-(leq(n0, 687 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690]))], (692 ^ _216792) ^ [] : [-(leq(687 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690], _242678))], (694 ^ _216792) ^ [] : [-(leq(n0, 688 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690]))], (696 ^ _216792) ^ [] : [-(leq(688 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690], _242678))], (698 ^ _216792) ^ [] : [a_select3(_242690, 687 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690], 688 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690]) = a_select3(_242690, 688 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690], 687 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690])]], 701 ^ _216792 : [(702 ^ _216792) ^ [] : [-(leq(n0, 699 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690]))], (704 ^ _216792) ^ [] : [-(leq(699 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690], _242678))], (706 ^ _216792) ^ [] : [-(leq(n0, 700 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690]))], (708 ^ _216792) ^ [] : [-(leq(700 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690], _242678))], (710 ^ _216792) ^ [] : [a_select3(_242680, 699 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690], 700 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690]) = a_select3(_242680, 700 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690], 699 ^ [_242676, _242678, _242680, _242682, _242684, _242686, _242688, _242690])]], 711 ^ _216792 : [(712 ^ _216792) ^ [_245604, _245606] : [-(a_select3(tptp_madd(_242690, tptp_mmul(_242688, tptp_mmul(tptp_madd(tptp_mmul(_242686, tptp_mmul(_242684, trans(_242686))), tptp_mmul(_242682, tptp_mmul(_242680, trans(_242682)))), trans(_242688)))), _245606, _245604) = a_select3(tptp_madd(_242690, tptp_mmul(_242688, tptp_mmul(tptp_madd(tptp_mmul(_242686, tptp_mmul(_242684, trans(_242686))), tptp_mmul(_242682, tptp_mmul(_242680, trans(_242682)))), trans(_242688)))), _245604, _245606)), leq(n0, _245606), leq(_245606, _242678), leq(n0, _245604), leq(_245604, _242678)]]], (730 ^ _216792) ^ [_246357] : [-(sum(n0, tptp_minus_1, _246357) = n0)], (732 ^ _216792) ^ [_246439] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _246439))], (734 ^ _216792) ^ [] : [-(succ(tptp_minus_1) = n0)], (736 ^ _216792) ^ [_246574] : [-(plus(_246574, n1) = succ(_246574))], (738 ^ _216792) ^ [_246657] : [-(plus(n1, _246657) = succ(_246657))], (740 ^ _216792) ^ [_246740] : [-(plus(_246740, n2) = succ(succ(_246740)))], (742 ^ _216792) ^ [_246825] : [-(plus(n2, _246825) = succ(succ(_246825)))], (744 ^ _216792) ^ [_246910] : [-(plus(_246910, n3) = succ(succ(succ(_246910))))], (746 ^ _216792) ^ [_246997] : [-(plus(n3, _246997) = succ(succ(succ(_246997))))], (748 ^ _216792) ^ [_247084] : [-(plus(_247084, n4) = succ(succ(succ(succ(_247084)))))], (750 ^ _216792) ^ [_247173] : [-(plus(n4, _247173) = succ(succ(succ(succ(_247173)))))], (752 ^ _216792) ^ [_247262] : [-(plus(_247262, n5) = succ(succ(succ(succ(succ(_247262))))))], (754 ^ _216792) ^ [_247353] : [-(plus(n5, _247353) = succ(succ(succ(succ(succ(_247353))))))], (756 ^ _216792) ^ [_247444] : [-(minus(_247444, n1) = pred(_247444))], (758 ^ _216792) ^ [_247527] : [-(pred(succ(_247527)) = _247527)], (760 ^ _216792) ^ [_247609] : [-(succ(pred(_247609)) = _247609)], (762 ^ _216792) ^ [_247749, _247751] : [leq(succ(_247751), succ(_247749)), -(leq(_247751, _247749))], (768 ^ _216792) ^ [_247919, _247921] : [leq(_247921, _247919), -(leq(succ(_247921), succ(_247919)))], (774 ^ _216792) ^ [_248139, _248141] : [leq(succ(_248141), _248139), -(gt(_248139, _248141))], (780 ^ _216792) ^ [_248353, _248355] : [leq(minus(_248355, _248353), _248355), -(leq(n0, _248353))], (786 ^ _216792) ^ [_248582, _248584, _248586, _248588] : [-(a_select3(tptp_update3(_248588, _248586, _248584, _248582), _248586, _248584) = _248582)], (788 ^ _216792) ^ [_248774, _248776, _248778, _248780, _248782, _248784, _248786] : [-(a_select3(tptp_update3(_248778, _248786, _248784, _248774), _248782, _248780) = _248776), -(_248786 = _248782), _248784 = _248780, a_select3(_248778, _248782, _248780) = _248776], (802 ^ _216792) ^ [_249317, _249319, _249321, _249323, _249325, _249327] : [-(a_select3(tptp_update3(_249319, _249323, _249321, _249317), _249327, _249325) = _249317), 807 ^ _216792 : [(808 ^ _216792) ^ [] : [-(leq(n0, 805 ^ [_249317, _249319, _249321, _249323, _249325, _249327]))], (810 ^ _216792) ^ [] : [-(leq(n0, 806 ^ [_249317, _249319, _249321, _249323, _249325, _249327]))], (812 ^ _216792) ^ [] : [-(leq(805 ^ [_249317, _249319, _249321, _249323, _249325, _249327], _249323))], (814 ^ _216792) ^ [] : [-(leq(806 ^ [_249317, _249319, _249321, _249323, _249325, _249327], _249321))], (816 ^ _216792) ^ [] : [a_select3(_249319, 805 ^ [_249317, _249319, _249321, _249323, _249325, _249327], 806 ^ [_249317, _249319, _249321, _249323, _249325, _249327]) = _249317]], leq(n0, _249327), leq(_249327, _249323), leq(n0, _249325), leq(_249325, _249321)], (834 ^ _216792) ^ [_250659, _250661, _250663] : [-(a_select2(tptp_update2(_250663, _250661, _250659), _250661) = _250659)], (836 ^ _216792) ^ [_250819, _250821, _250823, _250825, _250827] : [-(a_select2(tptp_update2(_250823, _250827, _250819), _250825) = _250821), -(_250827 = _250825), a_select2(_250823, _250825) = _250821], (865 ^ _216792) ^ [] : [-(true)], (867 ^ _216792) ^ [] : [def = use], (846 ^ _216792) ^ [_251199, _251201, _251203, _251205] : [-(a_select2(tptp_update2(_251201, _251203, _251199), _251205) = _251199), 850 ^ _216792 : [(851 ^ _216792) ^ [] : [-(leq(n0, 849 ^ [_251199, _251201, _251203, _251205]))], (853 ^ _216792) ^ [] : [-(leq(849 ^ [_251199, _251201, _251203, _251205], _251203))], (855 ^ _216792) ^ [] : [a_select2(_251201, 849 ^ [_251199, _251201, _251203, _251205]) = _251199]], leq(n0, _251205), leq(_251205, _251203)]], input).
% 0.22/1.31 ncf('1',plain,[a_select3(z_defuse, 1152 ^ [], 1153 ^ []) = use],start(1181 ^ 0)).
% 0.22/1.31 ncf('1.1',plain,[-(a_select3(z_defuse, 1152 ^ [], 1153 ^ []) = use), leq(n0, 1152 ^ []), leq(n0, 1153 ^ []), leq(1152 ^ [], n2), leq(1153 ^ [], pred(pv5))],extension(1135 ^ 1,bind([[_259230, _259232], [1153 ^ [], 1152 ^ []]]))).
% 0.22/1.31 ncf('1.1.1',plain,[-(leq(n0, 1152 ^ []))],extension(1155 ^ 2)).
% 0.22/1.31 ncf('1.1.2',plain,[-(leq(n0, 1153 ^ []))],extension(1157 ^ 2)).
% 0.22/1.31 ncf('1.1.3',plain,[-(leq(1152 ^ [], n2))],extension(1159 ^ 2)).
% 0.22/1.31 ncf('1.1.4',plain,[-(leq(1153 ^ [], pred(pv5)))],extension(1161 ^ 2)).
% 0.22/1.31 %-----------------------------------------------------
% 0.22/1.31 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------