%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV217+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n019.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.33s 1.38s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWV217+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n019.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.18/0.33 % CPULimit : 300
% 0.18/0.33 % WCLimit : 300
% 0.18/0.33 % DateTime : Fri May 19 02:34:42 EDT 2023
% 0.18/0.33 % CPUTime :
% 0.33/1.38
% 0.33/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.33/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 ncf(matrix, plain, [(1077 ^ _219366) ^ [] : [-(leq(n0, 1074 ^ []))], (1079 ^ _219366) ^ [] : [-(leq(n0, 1075 ^ []))], (1081 ^ _219366) ^ [] : [-(leq(1074 ^ [], n5))], (1083 ^ _219366) ^ [] : [-(leq(1075 ^ [], n5))], (1241 ^ _219366) ^ [] : [times(divide(n1, n400), a_select2(sigma, n2)) = n0], (1085 ^ _219366) ^ [] : [n0 = 1074 ^ [], n4 = 1075 ^ []], (1091 ^ _219366) ^ [] : [n0 = 1074 ^ [], n5 = 1075 ^ []], (1097 ^ _219366) ^ [] : [n0 = 1075 ^ [], n3 = 1074 ^ []], (1103 ^ _219366) ^ [] : [n0 = 1075 ^ [], n4 = 1074 ^ []], (1109 ^ _219366) ^ [] : [n0 = 1075 ^ [], n5 = 1074 ^ []], (1115 ^ _219366) ^ [] : [n1 = 1074 ^ [], n4 = 1075 ^ []], (1121 ^ _219366) ^ [] : [n1 = 1074 ^ [], n5 = 1075 ^ []], (1127 ^ _219366) ^ [] : [n1 = 1075 ^ [], n3 = 1074 ^ []], (1133 ^ _219366) ^ [] : [n1 = 1075 ^ [], n4 = 1074 ^ []], (1139 ^ _219366) ^ [] : [n1 = 1075 ^ [], n5 = 1074 ^ []], (1145 ^ _219366) ^ [] : [n2 = 1074 ^ [], n3 = 1075 ^ []], (1151 ^ _219366) ^ [] : [n2 = 1074 ^ [], n4 = 1075 ^ []], (1157 ^ _219366) ^ [] : [n2 = 1074 ^ [], n5 = 1075 ^ []], (1163 ^ _219366) ^ [] : [n2 = 1075 ^ [], n3 = 1074 ^ []], (1169 ^ _219366) ^ [] : [n2 = 1075 ^ [], n4 = 1074 ^ []], (1175 ^ _219366) ^ [] : [n2 = 1075 ^ [], n5 = 1074 ^ []], (1181 ^ _219366) ^ [] : [n3 = 1074 ^ [], n3 = 1075 ^ []], (1187 ^ _219366) ^ [] : [n3 = 1074 ^ [], n4 = 1075 ^ []], (1193 ^ _219366) ^ [] : [n3 = 1074 ^ [], n5 = 1075 ^ []], (1199 ^ _219366) ^ [] : [n3 = 1075 ^ [], n4 = 1074 ^ []], (1205 ^ _219366) ^ [] : [n3 = 1075 ^ [], n5 = 1074 ^ []], (1211 ^ _219366) ^ [] : [n4 = 1074 ^ [], n4 = 1075 ^ []], (1217 ^ _219366) ^ [] : [n4 = 1074 ^ [], n5 = 1075 ^ []], (1223 ^ _219366) ^ [] : [n4 = 1075 ^ [], n5 = 1074 ^ []], (1235 ^ _219366) ^ [] : [-(n2 = 1074 ^ [])], (1237 ^ _219366) ^ [] : [-(n2 = 1075 ^ [])], (1239 ^ _219366) ^ [] : [-(n3 = 1075 ^ [])], (1229 ^ _219366) ^ [] : [n5 = 1074 ^ [], n5 = 1075 ^ []], (2 ^ _219366) ^ [_219510] : [-(_219510 = _219510)], (4 ^ _219366) ^ [_219617, _219619] : [_219619 = _219617, -(_219617 = _219619)], (10 ^ _219366) ^ [_219821, _219823, _219825] : [-(_219825 = _219821), _219825 = _219823, _219823 = _219821], (20 ^ _219366) ^ [_220162, _220164, _220166, _220168] : [-(lt(_220166, _220162)), lt(_220168, _220164), _220168 = _220166, _220164 = _220162], (34 ^ _219366) ^ [_220606, _220608, _220610, _220612] : [-(geq(_220610, _220606)), geq(_220612, _220608), _220612 = _220610, _220608 = _220606], (48 ^ _219366) ^ [_221050, _221052, _221054, _221056] : [-(gt(_221054, _221050)), gt(_221056, _221052), _221056 = _221054, _221052 = _221050], (62 ^ _219366) ^ [_221474, _221476, _221478, _221480] : [-(leq(_221478, _221474)), leq(_221480, _221476), _221480 = _221478, _221476 = _221474], (76 ^ _219366) ^ [_221930, _221932, _221934, _221936] : [-(uniform_int_rnd(_221936, _221932) = uniform_int_rnd(_221934, _221930)), _221936 = _221934, _221932 = _221930], (86 ^ _219366) ^ [_222289, _222291, _222293, _222295] : [-(tptp_const_array1(_222295, _222291) = tptp_const_array1(_222293, _222289)), _222295 = _222293, _222291 = _222289], (96 ^ _219366) ^ [_222676, _222678, _222680, _222682, _222684, _222686] : [-(tptp_const_array2(_222686, _222682, _222678) = tptp_const_array2(_222684, _222680, _222676)), _222686 = _222684, _222682 = _222680, _222678 = _222676], (110 ^ _219366) ^ [_223164, _223166, _223168, _223170] : [-(dim(_223170, _223166) = dim(_223168, _223164)), _223170 = _223168, _223166 = _223164], (120 ^ _219366) ^ [_223495, _223497] : [_223497 = _223495, -(inv(_223497) = inv(_223495))], (126 ^ _219366) ^ [_223741, _223743, _223745, _223747] : [-(tptp_msub(_223747, _223743) = tptp_msub(_223745, _223741)), _223747 = _223745, _223743 = _223741], (136 ^ _219366) ^ [_224100, _224102, _224104, _224106] : [-(tptp_madd(_224106, _224102) = tptp_madd(_224104, _224100)), _224106 = _224104, _224102 = _224100], (146 ^ _219366) ^ [_224459, _224461, _224463, _224465] : [-(tptp_mmul(_224465, _224461) = tptp_mmul(_224463, _224459)), _224465 = _224463, _224461 = _224459], (156 ^ _219366) ^ [_224790, _224792] : [_224792 = _224790, -(trans(_224792) = trans(_224790))], (162 ^ _219366) ^ [_225064, _225066, _225068, _225070, _225072, _225074] : [-(sum(_225074, _225070, _225066) = sum(_225072, _225068, _225064)), _225074 = _225072, _225070 = _225068, _225066 = _225064], (176 ^ _219366) ^ [_225552, _225554, _225556, _225558] : [-(plus(_225558, _225554) = plus(_225556, _225552)), _225558 = _225556, _225554 = _225552], (186 ^ _219366) ^ [_225883, _225885] : [_225885 = _225883, -(pred(_225885) = pred(_225883))], (192 ^ _219366) ^ [_226129, _226131, _226133, _226135] : [-(minus(_226135, _226131) = minus(_226133, _226129)), _226135 = _226133, _226131 = _226129], (202 ^ _219366) ^ [_226516, _226518, _226520, _226522, _226524, _226526] : [-(a_select3(_226526, _226522, _226518) = a_select3(_226524, _226520, _226516)), _226526 = _226524, _226522 = _226520, _226518 = _226516], (216 ^ _219366) ^ [_227060, _227062, _227064, _227066, _227068, _227070, _227072, _227074] : [-(tptp_update3(_227074, _227070, _227066, _227062) = tptp_update3(_227072, _227068, _227064, _227060)), _227074 = _227072, _227070 = _227068, _227066 = _227064, _227062 = _227060], (234 ^ _219366) ^ [_227721, _227723, _227725, _227727, _227729, _227731] : [-(tptp_update2(_227731, _227727, _227723) = tptp_update2(_227729, _227725, _227721)), _227731 = _227729, _227727 = _227725, _227723 = _227721], (248 ^ _219366) ^ [_228181, _228183] : [_228183 = _228181, -(succ(_228183) = succ(_228181))], (254 ^ _219366) ^ [_228427, _228429, _228431, _228433] : [-(times(_228433, _228429) = times(_228431, _228427)), _228433 = _228431, _228429 = _228427], (264 ^ _219366) ^ [_228786, _228788, _228790, _228792] : [-(divide(_228792, _228788) = divide(_228790, _228786)), _228792 = _228790, _228788 = _228786], (274 ^ _219366) ^ [_229125, _229127, _229129, _229131] : [-(a_select2(_229131, _229127) = a_select2(_229129, _229125)), _229131 = _229129, _229127 = _229125], (889 ^ _219366) ^ [] : [-(gt(n5, n4))], (891 ^ _219366) ^ [] : [-(gt(n400, n4))], (893 ^ _219366) ^ [] : [-(gt(n400, n5))], (895 ^ _219366) ^ [] : [-(gt(n4, tptp_minus_1))], (897 ^ _219366) ^ [] : [-(gt(n5, tptp_minus_1))], (899 ^ _219366) ^ [] : [-(gt(n400, tptp_minus_1))], (901 ^ _219366) ^ [] : [-(gt(n0, tptp_minus_1))], (903 ^ _219366) ^ [] : [-(gt(n1, tptp_minus_1))], (905 ^ _219366) ^ [] : [-(gt(n2, tptp_minus_1))], (907 ^ _219366) ^ [] : [-(gt(n3, tptp_minus_1))], (909 ^ _219366) ^ [] : [-(gt(n4, n0))], (911 ^ _219366) ^ [] : [-(gt(n5, n0))], (913 ^ _219366) ^ [] : [-(gt(n400, n0))], (915 ^ _219366) ^ [] : [-(gt(n1, n0))], (917 ^ _219366) ^ [] : [-(gt(n2, n0))], (919 ^ _219366) ^ [] : [-(gt(n3, n0))], (921 ^ _219366) ^ [] : [-(gt(n4, n1))], (923 ^ _219366) ^ [] : [-(gt(n5, n1))], (925 ^ _219366) ^ [] : [-(gt(n400, n1))], (927 ^ _219366) ^ [] : [-(gt(n2, n1))], (929 ^ _219366) ^ [] : [-(gt(n3, n1))], (931 ^ _219366) ^ [] : [-(gt(n4, n2))], (933 ^ _219366) ^ [] : [-(gt(n5, n2))], (935 ^ _219366) ^ [] : [-(gt(n400, n2))], (937 ^ _219366) ^ [] : [-(gt(n3, n2))], (939 ^ _219366) ^ [] : [-(gt(n4, n3))], (941 ^ _219366) ^ [] : [-(gt(n5, n3))], (943 ^ _219366) ^ [] : [-(gt(n400, n3))], (945 ^ _219366) ^ [_256973] : [leq(n0, _256973), leq(_256973, n4), -(_256973 = n0), -(_256973 = n1), -(_256973 = n2), -(_256973 = n3), -(_256973 = n4)], (971 ^ _219366) ^ [_257594] : [leq(n0, _257594), leq(_257594, n5), -(_257594 = n0), -(_257594 = n1), -(_257594 = n2), -(_257594 = n3), -(_257594 = n4), -(_257594 = n5)], (1001 ^ _219366) ^ [_258301] : [-(_258301 = n0), leq(n0, _258301), leq(_258301, n0)], (1011 ^ _219366) ^ [_258576] : [leq(n0, _258576), leq(_258576, n1), -(_258576 = n0), -(_258576 = n1)], (1025 ^ _219366) ^ [_258939] : [leq(n0, _258939), leq(_258939, n2), -(_258939 = n0), -(_258939 = n1), -(_258939 = n2)], (1065 ^ _219366) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (1067 ^ _219366) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (1069 ^ _219366) ^ [] : [-(succ(n0) = n1)], (1071 ^ _219366) ^ [] : [-(succ(succ(n0)) = n2)], (1073 ^ _219366) ^ [] : [-(succ(succ(succ(n0))) = n3)], (1043 ^ _219366) ^ [_259388] : [leq(n0, _259388), leq(_259388, n3), -(_259388 = n0), -(_259388 = n1), -(_259388 = n2), -(_259388 = n3)], (284 ^ _219366) ^ [_229564, _229566] : [-(gt(_229566, _229564)), -(gt(_229564, _229566)), -(_229566 = _229564)], (294 ^ _219366) ^ [_229879, _229881, _229883] : [-(gt(_229883, _229879)), gt(_229883, _229881), gt(_229881, _229879)], (304 ^ _219366) ^ [_230158] : [gt(_230158, _230158)], (306 ^ _219366) ^ [_230236] : [-(leq(_230236, _230236))], (308 ^ _219366) ^ [_230357, _230359, _230361] : [-(leq(_230361, _230357)), leq(_230361, _230359), leq(_230359, _230357)], (318 ^ _219366) ^ [_230695, _230697] : [lt(_230697, _230695), -(gt(_230695, _230697))], (324 ^ _219366) ^ [_230857, _230859] : [gt(_230857, _230859), -(lt(_230859, _230857))], (330 ^ _219366) ^ [_231098, _231100] : [geq(_231100, _231098), -(leq(_231098, _231100))], (336 ^ _219366) ^ [_231260, _231262] : [leq(_231260, _231262), -(geq(_231262, _231260))], (342 ^ _219366) ^ [_231472, _231474] : [gt(_231472, _231474), -(leq(_231474, _231472))], (348 ^ _219366) ^ [_231682, _231684] : [-(gt(_231682, _231684)), leq(_231684, _231682), -(_231684 = _231682)], (358 ^ _219366) ^ [_232013, _232015] : [leq(_232015, pred(_232013)), -(gt(_232013, _232015))], (364 ^ _219366) ^ [_232179, _232181] : [gt(_232179, _232181), -(leq(_232181, pred(_232179)))], (370 ^ _219366) ^ [_232366] : [-(gt(succ(_232366), _232366))], (372 ^ _219366) ^ [_232475, _232477] : [leq(_232477, _232475), -(leq(_232477, succ(_232475)))], (378 ^ _219366) ^ [_232718, _232720] : [leq(_232720, _232718), -(gt(succ(_232718), _232720))], (384 ^ _219366) ^ [_232884, _232886] : [gt(succ(_232884), _232886), -(leq(_232886, _232884))], (390 ^ _219366) ^ [_233100, _233102] : [leq(n0, _233102), -(leq(uniform_int_rnd(_233100, _233102), _233102))], (396 ^ _219366) ^ [_233316, _233318] : [leq(n0, _233318), -(leq(n0, uniform_int_rnd(_233316, _233318)))], (402 ^ _219366) ^ [_233560, _233562, _233564, _233566] : [-(a_select2(tptp_const_array1(dim(_233564, _233562), _233560), _233566) = _233560), leq(_233564, _233566), leq(_233566, _233562)], (412 ^ _219366) ^ [_233967, _233969, _233971, _233973, _233975, _233977, _233979] : [-(a_select3(tptp_const_array2(dim(_233977, _233975), dim(_233971, _233969), _233967), _233979, _233973) = _233967), leq(_233977, _233979), leq(_233979, _233975), leq(_233971, _233973), leq(_233973, _233969)], (430 ^ _219366) ^ [_234562, _234564] : [433 ^ _219366 : [(434 ^ _219366) ^ [] : [-(leq(n0, 431 ^ [_234562, _234564]))], (436 ^ _219366) ^ [] : [-(leq(431 ^ [_234562, _234564], _234562))], (438 ^ _219366) ^ [] : [-(leq(n0, 432 ^ [_234562, _234564]))], (440 ^ _219366) ^ [] : [-(leq(432 ^ [_234562, _234564], _234562))], (442 ^ _219366) ^ [] : [a_select3(_234564, 431 ^ [_234562, _234564], 432 ^ [_234562, _234564]) = a_select3(_234564, 432 ^ [_234562, _234564], 431 ^ [_234562, _234564])]], 443 ^ _219366 : [(444 ^ _219366) ^ [_235319, _235321] : [-(a_select3(trans(_234564), _235321, _235319) = a_select3(trans(_234564), _235319, _235321)), leq(n0, _235321), leq(_235321, _234562), leq(n0, _235319), leq(_235319, _234562)]]], (462 ^ _219366) ^ [_235866, _235868] : [465 ^ _219366 : [(466 ^ _219366) ^ [] : [-(leq(n0, 463 ^ [_235866, _235868]))], (468 ^ _219366) ^ [] : [-(leq(463 ^ [_235866, _235868], _235866))], (470 ^ _219366) ^ [] : [-(leq(n0, 464 ^ [_235866, _235868]))], (472 ^ _219366) ^ [] : [-(leq(464 ^ [_235866, _235868], _235866))], (474 ^ _219366) ^ [] : [a_select3(_235868, 463 ^ [_235866, _235868], 464 ^ [_235866, _235868]) = a_select3(_235868, 464 ^ [_235866, _235868], 463 ^ [_235866, _235868])]], 475 ^ _219366 : [(476 ^ _219366) ^ [_236623, _236625] : [-(a_select3(inv(_235868), _236625, _236623) = a_select3(inv(_235868), _236623, _236625)), leq(n0, _236625), leq(_236625, _235866), leq(n0, _236623), leq(_236623, _235866)]]], (494 ^ _219366) ^ [_237170, _237172] : [497 ^ _219366 : [(498 ^ _219366) ^ [] : [-(leq(n0, 495 ^ [_237170, _237172]))], (500 ^ _219366) ^ [] : [-(leq(495 ^ [_237170, _237172], _237170))], (502 ^ _219366) ^ [] : [-(leq(n0, 496 ^ [_237170, _237172]))], (504 ^ _219366) ^ [] : [-(leq(496 ^ [_237170, _237172], _237170))], (506 ^ _219366) ^ [] : [a_select3(_237172, 495 ^ [_237170, _237172], 496 ^ [_237170, _237172]) = a_select3(_237172, 496 ^ [_237170, _237172], 495 ^ [_237170, _237172])]], 507 ^ _219366 : [(508 ^ _219366) ^ [_237983, _237985, _237987, _237989] : [-(a_select3(tptp_update3(_237172, _237985, _237985, _237983), _237989, _237987) = a_select3(tptp_update3(_237172, _237985, _237985, _237983), _237987, _237989)), leq(n0, _237989), leq(_237989, _237170), leq(n0, _237987), leq(_237987, _237170), leq(n0, _237985), leq(_237985, _237170)]]], (534 ^ _219366) ^ [_238802, _238804, _238806] : [539 ^ _219366 : [(540 ^ _219366) ^ [] : [-(leq(n0, 537 ^ [_238802, _238804, _238806]))], (542 ^ _219366) ^ [] : [-(leq(537 ^ [_238802, _238804, _238806], _238802))], (544 ^ _219366) ^ [] : [-(leq(n0, 538 ^ [_238802, _238804, _238806]))], (546 ^ _219366) ^ [] : [-(leq(538 ^ [_238802, _238804, _238806], _238802))], (548 ^ _219366) ^ [] : [a_select3(_238806, 537 ^ [_238802, _238804, _238806], 538 ^ [_238802, _238804, _238806]) = a_select3(_238806, 538 ^ [_238802, _238804, _238806], 537 ^ [_238802, _238804, _238806])]], 551 ^ _219366 : [(552 ^ _219366) ^ [] : [-(leq(n0, 549 ^ [_238802, _238804, _238806]))], (554 ^ _219366) ^ [] : [-(leq(549 ^ [_238802, _238804, _238806], _238802))], (556 ^ _219366) ^ [] : [-(leq(n0, 550 ^ [_238802, _238804, _238806]))], (558 ^ _219366) ^ [] : [-(leq(550 ^ [_238802, _238804, _238806], _238802))], (560 ^ _219366) ^ [] : [a_select3(_238804, 549 ^ [_238802, _238804, _238806], 550 ^ [_238802, _238804, _238806]) = a_select3(_238804, 550 ^ [_238802, _238804, _238806], 549 ^ [_238802, _238804, _238806])]], 561 ^ _219366 : [(562 ^ _219366) ^ [_240311, _240313] : [-(a_select3(tptp_madd(_238806, _238804), _240313, _240311) = a_select3(tptp_madd(_238806, _238804), _240311, _240313)), leq(n0, _240313), leq(_240313, _238802), leq(n0, _240311), leq(_240311, _238802)]]], (580 ^ _219366) ^ [_240897, _240899, _240901] : [585 ^ _219366 : [(586 ^ _219366) ^ [] : [-(leq(n0, 583 ^ [_240897, _240899, _240901]))], (588 ^ _219366) ^ [] : [-(leq(583 ^ [_240897, _240899, _240901], _240897))], (590 ^ _219366) ^ [] : [-(leq(n0, 584 ^ [_240897, _240899, _240901]))], (592 ^ _219366) ^ [] : [-(leq(584 ^ [_240897, _240899, _240901], _240897))], (594 ^ _219366) ^ [] : [a_select3(_240901, 583 ^ [_240897, _240899, _240901], 584 ^ [_240897, _240899, _240901]) = a_select3(_240901, 584 ^ [_240897, _240899, _240901], 583 ^ [_240897, _240899, _240901])]], 597 ^ _219366 : [(598 ^ _219366) ^ [] : [-(leq(n0, 595 ^ [_240897, _240899, _240901]))], (600 ^ _219366) ^ [] : [-(leq(595 ^ [_240897, _240899, _240901], _240897))], (602 ^ _219366) ^ [] : [-(leq(n0, 596 ^ [_240897, _240899, _240901]))], (604 ^ _219366) ^ [] : [-(leq(596 ^ [_240897, _240899, _240901], _240897))], (606 ^ _219366) ^ [] : [a_select3(_240899, 595 ^ [_240897, _240899, _240901], 596 ^ [_240897, _240899, _240901]) = a_select3(_240899, 596 ^ [_240897, _240899, _240901], 595 ^ [_240897, _240899, _240901])]], 607 ^ _219366 : [(608 ^ _219366) ^ [_242406, _242408] : [-(a_select3(tptp_msub(_240901, _240899), _242408, _242406) = a_select3(tptp_msub(_240901, _240899), _242406, _242408)), leq(n0, _242408), leq(_242408, _240897), leq(n0, _242406), leq(_242406, _240897)]]], (626 ^ _219366) ^ [_242992, _242994, _242996] : [629 ^ _219366 : [(630 ^ _219366) ^ [] : [-(leq(n0, 627 ^ [_242992, _242994, _242996]))], (632 ^ _219366) ^ [] : [-(leq(627 ^ [_242992, _242994, _242996], _242992))], (634 ^ _219366) ^ [] : [-(leq(n0, 628 ^ [_242992, _242994, _242996]))], (636 ^ _219366) ^ [] : [-(leq(628 ^ [_242992, _242994, _242996], _242992))], (638 ^ _219366) ^ [] : [a_select3(_242994, 627 ^ [_242992, _242994, _242996], 628 ^ [_242992, _242994, _242996]) = a_select3(_242994, 628 ^ [_242992, _242994, _242996], 627 ^ [_242992, _242994, _242996])]], 639 ^ _219366 : [(640 ^ _219366) ^ [_243805, _243807] : [-(a_select3(tptp_mmul(_242996, tptp_mmul(_242994, trans(_242996))), _243807, _243805) = a_select3(tptp_mmul(_242996, tptp_mmul(_242994, trans(_242996))), _243805, _243807)), leq(n0, _243807), leq(_243807, _242992), leq(n0, _243805), leq(_243805, _242992)]]], (658 ^ _219366) ^ [_244424, _244426, _244428, _244430] : [661 ^ _219366 : [(662 ^ _219366) ^ [] : [-(leq(n0, 659 ^ [_244424, _244426, _244428, _244430]))], (664 ^ _219366) ^ [] : [-(leq(659 ^ [_244424, _244426, _244428, _244430], _244424))], (666 ^ _219366) ^ [] : [-(leq(n0, 660 ^ [_244424, _244426, _244428, _244430]))], (668 ^ _219366) ^ [] : [-(leq(660 ^ [_244424, _244426, _244428, _244430], _244424))], (670 ^ _219366) ^ [] : [a_select3(_244428, 659 ^ [_244424, _244426, _244428, _244430], 660 ^ [_244424, _244426, _244428, _244430]) = a_select3(_244428, 660 ^ [_244424, _244426, _244428, _244430], 659 ^ [_244424, _244426, _244428, _244430])]], 671 ^ _219366 : [(672 ^ _219366) ^ [_245281, _245283] : [-(a_select3(tptp_mmul(_244430, tptp_mmul(_244428, trans(_244430))), _245283, _245281) = a_select3(tptp_mmul(_244430, tptp_mmul(_244428, trans(_244430))), _245281, _245283)), leq(n0, _245283), leq(_245283, _244426), leq(n0, _245281), leq(_245281, _244426)]]], (690 ^ _219366) ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990] : [695 ^ _219366 : [(696 ^ _219366) ^ [] : [-(leq(n0, 693 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990]))], (698 ^ _219366) ^ [] : [-(leq(693 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990], _245976))], (700 ^ _219366) ^ [] : [-(leq(n0, 694 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990]))], (702 ^ _219366) ^ [] : [-(leq(694 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990], _245976))], (704 ^ _219366) ^ [] : [a_select3(_245984, 693 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990], 694 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990]) = a_select3(_245984, 694 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990], 693 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990])]], 709 ^ _219366 : [(710 ^ _219366) ^ [] : [-(leq(n0, 707 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990]))], (712 ^ _219366) ^ [] : [-(leq(707 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990], _245978))], (714 ^ _219366) ^ [] : [-(leq(n0, 708 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990]))], (716 ^ _219366) ^ [] : [-(leq(708 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990], _245978))], (718 ^ _219366) ^ [] : [a_select3(_245990, 707 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990], 708 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990]) = a_select3(_245990, 708 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990], 707 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990])]], 721 ^ _219366 : [(722 ^ _219366) ^ [] : [-(leq(n0, 719 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990]))], (724 ^ _219366) ^ [] : [-(leq(719 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990], _245978))], (726 ^ _219366) ^ [] : [-(leq(n0, 720 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990]))], (728 ^ _219366) ^ [] : [-(leq(720 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990], _245978))], (730 ^ _219366) ^ [] : [a_select3(_245980, 719 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990], 720 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990]) = a_select3(_245980, 720 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990], 719 ^ [_245976, _245978, _245980, _245982, _245984, _245986, _245988, _245990])]], 731 ^ _219366 : [(732 ^ _219366) ^ [_248904, _248906] : [-(a_select3(tptp_madd(_245990, tptp_mmul(_245988, tptp_mmul(tptp_madd(tptp_mmul(_245986, tptp_mmul(_245984, trans(_245986))), tptp_mmul(_245982, tptp_mmul(_245980, trans(_245982)))), trans(_245988)))), _248906, _248904) = a_select3(tptp_madd(_245990, tptp_mmul(_245988, tptp_mmul(tptp_madd(tptp_mmul(_245986, tptp_mmul(_245984, trans(_245986))), tptp_mmul(_245982, tptp_mmul(_245980, trans(_245982)))), trans(_245988)))), _248904, _248906)), leq(n0, _248906), leq(_248906, _245978), leq(n0, _248904), leq(_248904, _245978)]]], (750 ^ _219366) ^ [_249657] : [-(sum(n0, tptp_minus_1, _249657) = n0)], (752 ^ _219366) ^ [_249739] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _249739))], (754 ^ _219366) ^ [] : [-(succ(tptp_minus_1) = n0)], (756 ^ _219366) ^ [_249874] : [-(plus(_249874, n1) = succ(_249874))], (758 ^ _219366) ^ [_249957] : [-(plus(n1, _249957) = succ(_249957))], (760 ^ _219366) ^ [_250040] : [-(plus(_250040, n2) = succ(succ(_250040)))], (762 ^ _219366) ^ [_250125] : [-(plus(n2, _250125) = succ(succ(_250125)))], (764 ^ _219366) ^ [_250210] : [-(plus(_250210, n3) = succ(succ(succ(_250210))))], (766 ^ _219366) ^ [_250297] : [-(plus(n3, _250297) = succ(succ(succ(_250297))))], (768 ^ _219366) ^ [_250384] : [-(plus(_250384, n4) = succ(succ(succ(succ(_250384)))))], (770 ^ _219366) ^ [_250473] : [-(plus(n4, _250473) = succ(succ(succ(succ(_250473)))))], (772 ^ _219366) ^ [_250562] : [-(plus(_250562, n5) = succ(succ(succ(succ(succ(_250562))))))], (774 ^ _219366) ^ [_250653] : [-(plus(n5, _250653) = succ(succ(succ(succ(succ(_250653))))))], (776 ^ _219366) ^ [_250744] : [-(minus(_250744, n1) = pred(_250744))], (778 ^ _219366) ^ [_250827] : [-(pred(succ(_250827)) = _250827)], (780 ^ _219366) ^ [_250909] : [-(succ(pred(_250909)) = _250909)], (782 ^ _219366) ^ [_251049, _251051] : [leq(succ(_251051), succ(_251049)), -(leq(_251051, _251049))], (788 ^ _219366) ^ [_251219, _251221] : [leq(_251221, _251219), -(leq(succ(_251221), succ(_251219)))], (794 ^ _219366) ^ [_251439, _251441] : [leq(succ(_251441), _251439), -(gt(_251439, _251441))], (800 ^ _219366) ^ [_251653, _251655] : [leq(minus(_251655, _251653), _251655), -(leq(n0, _251653))], (806 ^ _219366) ^ [_251882, _251884, _251886, _251888] : [-(a_select3(tptp_update3(_251888, _251886, _251884, _251882), _251886, _251884) = _251882)], (808 ^ _219366) ^ [_252074, _252076, _252078, _252080, _252082, _252084, _252086] : [-(a_select3(tptp_update3(_252078, _252086, _252084, _252074), _252082, _252080) = _252076), -(_252086 = _252082), _252084 = _252080, a_select3(_252078, _252082, _252080) = _252076], (822 ^ _219366) ^ [_252617, _252619, _252621, _252623, _252625, _252627] : [-(a_select3(tptp_update3(_252619, _252623, _252621, _252617), _252627, _252625) = _252617), 827 ^ _219366 : [(828 ^ _219366) ^ [] : [-(leq(n0, 825 ^ [_252617, _252619, _252621, _252623, _252625, _252627]))], (830 ^ _219366) ^ [] : [-(leq(n0, 826 ^ [_252617, _252619, _252621, _252623, _252625, _252627]))], (832 ^ _219366) ^ [] : [-(leq(825 ^ [_252617, _252619, _252621, _252623, _252625, _252627], _252623))], (834 ^ _219366) ^ [] : [-(leq(826 ^ [_252617, _252619, _252621, _252623, _252625, _252627], _252621))], (836 ^ _219366) ^ [] : [a_select3(_252619, 825 ^ [_252617, _252619, _252621, _252623, _252625, _252627], 826 ^ [_252617, _252619, _252621, _252623, _252625, _252627]) = _252617]], leq(n0, _252627), leq(_252627, _252623), leq(n0, _252625), leq(_252625, _252621)], (854 ^ _219366) ^ [_253959, _253961, _253963] : [-(a_select2(tptp_update2(_253963, _253961, _253959), _253961) = _253959)], (856 ^ _219366) ^ [_254119, _254121, _254123, _254125, _254127] : [-(a_select2(tptp_update2(_254123, _254127, _254119), _254125) = _254121), -(_254127 = _254125), a_select2(_254123, _254125) = _254121], (885 ^ _219366) ^ [] : [-(true)], (887 ^ _219366) ^ [] : [def = use], (866 ^ _219366) ^ [_254499, _254501, _254503, _254505] : [-(a_select2(tptp_update2(_254501, _254503, _254499), _254505) = _254499), 870 ^ _219366 : [(871 ^ _219366) ^ [] : [-(leq(n0, 869 ^ [_254499, _254501, _254503, _254505]))], (873 ^ _219366) ^ [] : [-(leq(869 ^ [_254499, _254501, _254503, _254505], _254503))], (875 ^ _219366) ^ [] : [a_select2(_254501, 869 ^ [_254499, _254501, _254503, _254505]) = _254499]], leq(n0, _254505), leq(_254505, _254503)]], input).
% 0.33/1.38 ncf('1',plain,[n2 = 1074 ^ [], n3 = 1075 ^ []],start(1145 ^ 0)).
% 0.33/1.38 ncf('1.1',plain,[-(n2 = 1074 ^ [])],extension(1235 ^ 1)).
% 0.33/1.38 ncf('1.2',plain,[-(n3 = 1075 ^ [])],extension(1239 ^ 1)).
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------