%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV212+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n018.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.36s 1.39s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : SWV212+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.08/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n018.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Fri May 19 02:42:43 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.36/1.39
% 0.36/1.39 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.36/1.39 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/1.39 %-----------------------------------------------------
% 0.36/1.39 ncf(matrix, plain, [(1077 ^ _226311) ^ [] : [-(leq(n0, 1074 ^ []))], (1079 ^ _226311) ^ [] : [-(leq(n0, 1075 ^ []))], (1081 ^ _226311) ^ [] : [-(leq(1074 ^ [], n5))], (1083 ^ _226311) ^ [] : [-(leq(1075 ^ [], n5))], (1301 ^ _226311) ^ [] : [n0 = times(divide(n1, n400), a_select2(sigma, n0))], (1085 ^ _226311) ^ [] : [n0 = 1074 ^ [], n1 = 1075 ^ []], (1091 ^ _226311) ^ [] : [n0 = 1074 ^ [], n2 = 1075 ^ []], (1097 ^ _226311) ^ [] : [n0 = 1074 ^ [], n3 = 1075 ^ []], (1103 ^ _226311) ^ [] : [n0 = 1074 ^ [], n4 = 1075 ^ []], (1109 ^ _226311) ^ [] : [n0 = 1074 ^ [], n5 = 1075 ^ []], (1115 ^ _226311) ^ [] : [n0 = 1075 ^ [], n1 = 1074 ^ []], (1121 ^ _226311) ^ [] : [n0 = 1075 ^ [], n2 = 1074 ^ []], (1127 ^ _226311) ^ [] : [n0 = 1075 ^ [], n3 = 1074 ^ []], (1133 ^ _226311) ^ [] : [n0 = 1075 ^ [], n4 = 1074 ^ []], (1139 ^ _226311) ^ [] : [n0 = 1075 ^ [], n5 = 1074 ^ []], (1145 ^ _226311) ^ [] : [n1 = 1074 ^ [], n1 = 1075 ^ []], (1151 ^ _226311) ^ [] : [n1 = 1074 ^ [], n2 = 1075 ^ []], (1157 ^ _226311) ^ [] : [n1 = 1074 ^ [], n3 = 1075 ^ []], (1163 ^ _226311) ^ [] : [n1 = 1074 ^ [], n4 = 1075 ^ []], (1169 ^ _226311) ^ [] : [n1 = 1074 ^ [], n5 = 1075 ^ []], (1175 ^ _226311) ^ [] : [n1 = 1075 ^ [], n2 = 1074 ^ []], (1181 ^ _226311) ^ [] : [n1 = 1075 ^ [], n3 = 1074 ^ []], (1187 ^ _226311) ^ [] : [n1 = 1075 ^ [], n4 = 1074 ^ []], (1193 ^ _226311) ^ [] : [n1 = 1075 ^ [], n5 = 1074 ^ []], (1199 ^ _226311) ^ [] : [n2 = 1074 ^ [], n2 = 1075 ^ []], (1205 ^ _226311) ^ [] : [n2 = 1074 ^ [], n3 = 1075 ^ []], (1211 ^ _226311) ^ [] : [n2 = 1074 ^ [], n4 = 1075 ^ []], (1217 ^ _226311) ^ [] : [n2 = 1074 ^ [], n5 = 1075 ^ []], (1223 ^ _226311) ^ [] : [n2 = 1075 ^ [], n3 = 1074 ^ []], (1229 ^ _226311) ^ [] : [n2 = 1075 ^ [], n4 = 1074 ^ []], (1235 ^ _226311) ^ [] : [n2 = 1075 ^ [], n5 = 1074 ^ []], (1241 ^ _226311) ^ [] : [n3 = 1074 ^ [], n3 = 1075 ^ []], (1247 ^ _226311) ^ [] : [n3 = 1074 ^ [], n4 = 1075 ^ []], (1253 ^ _226311) ^ [] : [n3 = 1074 ^ [], n5 = 1075 ^ []], (1259 ^ _226311) ^ [] : [n3 = 1075 ^ [], n4 = 1074 ^ []], (1265 ^ _226311) ^ [] : [n3 = 1075 ^ [], n5 = 1074 ^ []], (1271 ^ _226311) ^ [] : [n4 = 1074 ^ [], n4 = 1075 ^ []], (1277 ^ _226311) ^ [] : [n4 = 1074 ^ [], n5 = 1075 ^ []], (1283 ^ _226311) ^ [] : [n4 = 1075 ^ [], n5 = 1074 ^ []], (1295 ^ _226311) ^ [] : [-(n0 = 1074 ^ [])], (1297 ^ _226311) ^ [] : [-(n0 = 1075 ^ [])], (1299 ^ _226311) ^ [] : [-(n3 = 1074 ^ [])], (1289 ^ _226311) ^ [] : [n5 = 1074 ^ [], n5 = 1075 ^ []], (2 ^ _226311) ^ [_226455] : [-(_226455 = _226455)], (4 ^ _226311) ^ [_226562, _226564] : [_226564 = _226562, -(_226562 = _226564)], (10 ^ _226311) ^ [_226766, _226768, _226770] : [-(_226770 = _226766), _226770 = _226768, _226768 = _226766], (20 ^ _226311) ^ [_227107, _227109, _227111, _227113] : [-(lt(_227111, _227107)), lt(_227113, _227109), _227113 = _227111, _227109 = _227107], (34 ^ _226311) ^ [_227551, _227553, _227555, _227557] : [-(geq(_227555, _227551)), geq(_227557, _227553), _227557 = _227555, _227553 = _227551], (48 ^ _226311) ^ [_227995, _227997, _227999, _228001] : [-(gt(_227999, _227995)), gt(_228001, _227997), _228001 = _227999, _227997 = _227995], (62 ^ _226311) ^ [_228419, _228421, _228423, _228425] : [-(leq(_228423, _228419)), leq(_228425, _228421), _228425 = _228423, _228421 = _228419], (76 ^ _226311) ^ [_228875, _228877, _228879, _228881] : [-(uniform_int_rnd(_228881, _228877) = uniform_int_rnd(_228879, _228875)), _228881 = _228879, _228877 = _228875], (86 ^ _226311) ^ [_229234, _229236, _229238, _229240] : [-(tptp_const_array1(_229240, _229236) = tptp_const_array1(_229238, _229234)), _229240 = _229238, _229236 = _229234], (96 ^ _226311) ^ [_229621, _229623, _229625, _229627, _229629, _229631] : [-(tptp_const_array2(_229631, _229627, _229623) = tptp_const_array2(_229629, _229625, _229621)), _229631 = _229629, _229627 = _229625, _229623 = _229621], (110 ^ _226311) ^ [_230109, _230111, _230113, _230115] : [-(dim(_230115, _230111) = dim(_230113, _230109)), _230115 = _230113, _230111 = _230109], (120 ^ _226311) ^ [_230440, _230442] : [_230442 = _230440, -(inv(_230442) = inv(_230440))], (126 ^ _226311) ^ [_230686, _230688, _230690, _230692] : [-(tptp_msub(_230692, _230688) = tptp_msub(_230690, _230686)), _230692 = _230690, _230688 = _230686], (136 ^ _226311) ^ [_231045, _231047, _231049, _231051] : [-(tptp_madd(_231051, _231047) = tptp_madd(_231049, _231045)), _231051 = _231049, _231047 = _231045], (146 ^ _226311) ^ [_231404, _231406, _231408, _231410] : [-(tptp_mmul(_231410, _231406) = tptp_mmul(_231408, _231404)), _231410 = _231408, _231406 = _231404], (156 ^ _226311) ^ [_231735, _231737] : [_231737 = _231735, -(trans(_231737) = trans(_231735))], (162 ^ _226311) ^ [_232009, _232011, _232013, _232015, _232017, _232019] : [-(sum(_232019, _232015, _232011) = sum(_232017, _232013, _232009)), _232019 = _232017, _232015 = _232013, _232011 = _232009], (176 ^ _226311) ^ [_232497, _232499, _232501, _232503] : [-(plus(_232503, _232499) = plus(_232501, _232497)), _232503 = _232501, _232499 = _232497], (186 ^ _226311) ^ [_232828, _232830] : [_232830 = _232828, -(pred(_232830) = pred(_232828))], (192 ^ _226311) ^ [_233074, _233076, _233078, _233080] : [-(minus(_233080, _233076) = minus(_233078, _233074)), _233080 = _233078, _233076 = _233074], (202 ^ _226311) ^ [_233461, _233463, _233465, _233467, _233469, _233471] : [-(a_select3(_233471, _233467, _233463) = a_select3(_233469, _233465, _233461)), _233471 = _233469, _233467 = _233465, _233463 = _233461], (216 ^ _226311) ^ [_234005, _234007, _234009, _234011, _234013, _234015, _234017, _234019] : [-(tptp_update3(_234019, _234015, _234011, _234007) = tptp_update3(_234017, _234013, _234009, _234005)), _234019 = _234017, _234015 = _234013, _234011 = _234009, _234007 = _234005], (234 ^ _226311) ^ [_234666, _234668, _234670, _234672, _234674, _234676] : [-(tptp_update2(_234676, _234672, _234668) = tptp_update2(_234674, _234670, _234666)), _234676 = _234674, _234672 = _234670, _234668 = _234666], (248 ^ _226311) ^ [_235126, _235128] : [_235128 = _235126, -(succ(_235128) = succ(_235126))], (254 ^ _226311) ^ [_235372, _235374, _235376, _235378] : [-(times(_235378, _235374) = times(_235376, _235372)), _235378 = _235376, _235374 = _235372], (264 ^ _226311) ^ [_235731, _235733, _235735, _235737] : [-(divide(_235737, _235733) = divide(_235735, _235731)), _235737 = _235735, _235733 = _235731], (274 ^ _226311) ^ [_236070, _236072, _236074, _236076] : [-(a_select2(_236076, _236072) = a_select2(_236074, _236070)), _236076 = _236074, _236072 = _236070], (889 ^ _226311) ^ [] : [-(gt(n5, n4))], (891 ^ _226311) ^ [] : [-(gt(n400, n4))], (893 ^ _226311) ^ [] : [-(gt(n400, n5))], (895 ^ _226311) ^ [] : [-(gt(n4, tptp_minus_1))], (897 ^ _226311) ^ [] : [-(gt(n5, tptp_minus_1))], (899 ^ _226311) ^ [] : [-(gt(n400, tptp_minus_1))], (901 ^ _226311) ^ [] : [-(gt(n0, tptp_minus_1))], (903 ^ _226311) ^ [] : [-(gt(n1, tptp_minus_1))], (905 ^ _226311) ^ [] : [-(gt(n2, tptp_minus_1))], (907 ^ _226311) ^ [] : [-(gt(n3, tptp_minus_1))], (909 ^ _226311) ^ [] : [-(gt(n4, n0))], (911 ^ _226311) ^ [] : [-(gt(n5, n0))], (913 ^ _226311) ^ [] : [-(gt(n400, n0))], (915 ^ _226311) ^ [] : [-(gt(n1, n0))], (917 ^ _226311) ^ [] : [-(gt(n2, n0))], (919 ^ _226311) ^ [] : [-(gt(n3, n0))], (921 ^ _226311) ^ [] : [-(gt(n4, n1))], (923 ^ _226311) ^ [] : [-(gt(n5, n1))], (925 ^ _226311) ^ [] : [-(gt(n400, n1))], (927 ^ _226311) ^ [] : [-(gt(n2, n1))], (929 ^ _226311) ^ [] : [-(gt(n3, n1))], (931 ^ _226311) ^ [] : [-(gt(n4, n2))], (933 ^ _226311) ^ [] : [-(gt(n5, n2))], (935 ^ _226311) ^ [] : [-(gt(n400, n2))], (937 ^ _226311) ^ [] : [-(gt(n3, n2))], (939 ^ _226311) ^ [] : [-(gt(n4, n3))], (941 ^ _226311) ^ [] : [-(gt(n5, n3))], (943 ^ _226311) ^ [] : [-(gt(n400, n3))], (945 ^ _226311) ^ [_263918] : [leq(n0, _263918), leq(_263918, n4), -(_263918 = n0), -(_263918 = n1), -(_263918 = n2), -(_263918 = n3), -(_263918 = n4)], (971 ^ _226311) ^ [_264539] : [leq(n0, _264539), leq(_264539, n5), -(_264539 = n0), -(_264539 = n1), -(_264539 = n2), -(_264539 = n3), -(_264539 = n4), -(_264539 = n5)], (1001 ^ _226311) ^ [_265246] : [-(_265246 = n0), leq(n0, _265246), leq(_265246, n0)], (1011 ^ _226311) ^ [_265521] : [leq(n0, _265521), leq(_265521, n1), -(_265521 = n0), -(_265521 = n1)], (1025 ^ _226311) ^ [_265884] : [leq(n0, _265884), leq(_265884, n2), -(_265884 = n0), -(_265884 = n1), -(_265884 = n2)], (1065 ^ _226311) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (1067 ^ _226311) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (1069 ^ _226311) ^ [] : [-(succ(n0) = n1)], (1071 ^ _226311) ^ [] : [-(succ(succ(n0)) = n2)], (1073 ^ _226311) ^ [] : [-(succ(succ(succ(n0))) = n3)], (1043 ^ _226311) ^ [_266333] : [leq(n0, _266333), leq(_266333, n3), -(_266333 = n0), -(_266333 = n1), -(_266333 = n2), -(_266333 = n3)], (284 ^ _226311) ^ [_236509, _236511] : [-(gt(_236511, _236509)), -(gt(_236509, _236511)), -(_236511 = _236509)], (294 ^ _226311) ^ [_236824, _236826, _236828] : [-(gt(_236828, _236824)), gt(_236828, _236826), gt(_236826, _236824)], (304 ^ _226311) ^ [_237103] : [gt(_237103, _237103)], (306 ^ _226311) ^ [_237181] : [-(leq(_237181, _237181))], (308 ^ _226311) ^ [_237302, _237304, _237306] : [-(leq(_237306, _237302)), leq(_237306, _237304), leq(_237304, _237302)], (318 ^ _226311) ^ [_237640, _237642] : [lt(_237642, _237640), -(gt(_237640, _237642))], (324 ^ _226311) ^ [_237802, _237804] : [gt(_237802, _237804), -(lt(_237804, _237802))], (330 ^ _226311) ^ [_238043, _238045] : [geq(_238045, _238043), -(leq(_238043, _238045))], (336 ^ _226311) ^ [_238205, _238207] : [leq(_238205, _238207), -(geq(_238207, _238205))], (342 ^ _226311) ^ [_238417, _238419] : [gt(_238417, _238419), -(leq(_238419, _238417))], (348 ^ _226311) ^ [_238627, _238629] : [-(gt(_238627, _238629)), leq(_238629, _238627), -(_238629 = _238627)], (358 ^ _226311) ^ [_238958, _238960] : [leq(_238960, pred(_238958)), -(gt(_238958, _238960))], (364 ^ _226311) ^ [_239124, _239126] : [gt(_239124, _239126), -(leq(_239126, pred(_239124)))], (370 ^ _226311) ^ [_239311] : [-(gt(succ(_239311), _239311))], (372 ^ _226311) ^ [_239420, _239422] : [leq(_239422, _239420), -(leq(_239422, succ(_239420)))], (378 ^ _226311) ^ [_239663, _239665] : [leq(_239665, _239663), -(gt(succ(_239663), _239665))], (384 ^ _226311) ^ [_239829, _239831] : [gt(succ(_239829), _239831), -(leq(_239831, _239829))], (390 ^ _226311) ^ [_240045, _240047] : [leq(n0, _240047), -(leq(uniform_int_rnd(_240045, _240047), _240047))], (396 ^ _226311) ^ [_240261, _240263] : [leq(n0, _240263), -(leq(n0, uniform_int_rnd(_240261, _240263)))], (402 ^ _226311) ^ [_240505, _240507, _240509, _240511] : [-(a_select2(tptp_const_array1(dim(_240509, _240507), _240505), _240511) = _240505), leq(_240509, _240511), leq(_240511, _240507)], (412 ^ _226311) ^ [_240912, _240914, _240916, _240918, _240920, _240922, _240924] : [-(a_select3(tptp_const_array2(dim(_240922, _240920), dim(_240916, _240914), _240912), _240924, _240918) = _240912), leq(_240922, _240924), leq(_240924, _240920), leq(_240916, _240918), leq(_240918, _240914)], (430 ^ _226311) ^ [_241507, _241509] : [433 ^ _226311 : [(434 ^ _226311) ^ [] : [-(leq(n0, 431 ^ [_241507, _241509]))], (436 ^ _226311) ^ [] : [-(leq(431 ^ [_241507, _241509], _241507))], (438 ^ _226311) ^ [] : [-(leq(n0, 432 ^ [_241507, _241509]))], (440 ^ _226311) ^ [] : [-(leq(432 ^ [_241507, _241509], _241507))], (442 ^ _226311) ^ [] : [a_select3(_241509, 431 ^ [_241507, _241509], 432 ^ [_241507, _241509]) = a_select3(_241509, 432 ^ [_241507, _241509], 431 ^ [_241507, _241509])]], 443 ^ _226311 : [(444 ^ _226311) ^ [_242264, _242266] : [-(a_select3(trans(_241509), _242266, _242264) = a_select3(trans(_241509), _242264, _242266)), leq(n0, _242266), leq(_242266, _241507), leq(n0, _242264), leq(_242264, _241507)]]], (462 ^ _226311) ^ [_242811, _242813] : [465 ^ _226311 : [(466 ^ _226311) ^ [] : [-(leq(n0, 463 ^ [_242811, _242813]))], (468 ^ _226311) ^ [] : [-(leq(463 ^ [_242811, _242813], _242811))], (470 ^ _226311) ^ [] : [-(leq(n0, 464 ^ [_242811, _242813]))], (472 ^ _226311) ^ [] : [-(leq(464 ^ [_242811, _242813], _242811))], (474 ^ _226311) ^ [] : [a_select3(_242813, 463 ^ [_242811, _242813], 464 ^ [_242811, _242813]) = a_select3(_242813, 464 ^ [_242811, _242813], 463 ^ [_242811, _242813])]], 475 ^ _226311 : [(476 ^ _226311) ^ [_243568, _243570] : [-(a_select3(inv(_242813), _243570, _243568) = a_select3(inv(_242813), _243568, _243570)), leq(n0, _243570), leq(_243570, _242811), leq(n0, _243568), leq(_243568, _242811)]]], (494 ^ _226311) ^ [_244115, _244117] : [497 ^ _226311 : [(498 ^ _226311) ^ [] : [-(leq(n0, 495 ^ [_244115, _244117]))], (500 ^ _226311) ^ [] : [-(leq(495 ^ [_244115, _244117], _244115))], (502 ^ _226311) ^ [] : [-(leq(n0, 496 ^ [_244115, _244117]))], (504 ^ _226311) ^ [] : [-(leq(496 ^ [_244115, _244117], _244115))], (506 ^ _226311) ^ [] : [a_select3(_244117, 495 ^ [_244115, _244117], 496 ^ [_244115, _244117]) = a_select3(_244117, 496 ^ [_244115, _244117], 495 ^ [_244115, _244117])]], 507 ^ _226311 : [(508 ^ _226311) ^ [_244928, _244930, _244932, _244934] : [-(a_select3(tptp_update3(_244117, _244930, _244930, _244928), _244934, _244932) = a_select3(tptp_update3(_244117, _244930, _244930, _244928), _244932, _244934)), leq(n0, _244934), leq(_244934, _244115), leq(n0, _244932), leq(_244932, _244115), leq(n0, _244930), leq(_244930, _244115)]]], (534 ^ _226311) ^ [_245747, _245749, _245751] : [539 ^ _226311 : [(540 ^ _226311) ^ [] : [-(leq(n0, 537 ^ [_245747, _245749, _245751]))], (542 ^ _226311) ^ [] : [-(leq(537 ^ [_245747, _245749, _245751], _245747))], (544 ^ _226311) ^ [] : [-(leq(n0, 538 ^ [_245747, _245749, _245751]))], (546 ^ _226311) ^ [] : [-(leq(538 ^ [_245747, _245749, _245751], _245747))], (548 ^ _226311) ^ [] : [a_select3(_245751, 537 ^ [_245747, _245749, _245751], 538 ^ [_245747, _245749, _245751]) = a_select3(_245751, 538 ^ [_245747, _245749, _245751], 537 ^ [_245747, _245749, _245751])]], 551 ^ _226311 : [(552 ^ _226311) ^ [] : [-(leq(n0, 549 ^ [_245747, _245749, _245751]))], (554 ^ _226311) ^ [] : [-(leq(549 ^ [_245747, _245749, _245751], _245747))], (556 ^ _226311) ^ [] : [-(leq(n0, 550 ^ [_245747, _245749, _245751]))], (558 ^ _226311) ^ [] : [-(leq(550 ^ [_245747, _245749, _245751], _245747))], (560 ^ _226311) ^ [] : [a_select3(_245749, 549 ^ [_245747, _245749, _245751], 550 ^ [_245747, _245749, _245751]) = a_select3(_245749, 550 ^ [_245747, _245749, _245751], 549 ^ [_245747, _245749, _245751])]], 561 ^ _226311 : [(562 ^ _226311) ^ [_247256, _247258] : [-(a_select3(tptp_madd(_245751, _245749), _247258, _247256) = a_select3(tptp_madd(_245751, _245749), _247256, _247258)), leq(n0, _247258), leq(_247258, _245747), leq(n0, _247256), leq(_247256, _245747)]]], (580 ^ _226311) ^ [_247842, _247844, _247846] : [585 ^ _226311 : [(586 ^ _226311) ^ [] : [-(leq(n0, 583 ^ [_247842, _247844, _247846]))], (588 ^ _226311) ^ [] : [-(leq(583 ^ [_247842, _247844, _247846], _247842))], (590 ^ _226311) ^ [] : [-(leq(n0, 584 ^ [_247842, _247844, _247846]))], (592 ^ _226311) ^ [] : [-(leq(584 ^ [_247842, _247844, _247846], _247842))], (594 ^ _226311) ^ [] : [a_select3(_247846, 583 ^ [_247842, _247844, _247846], 584 ^ [_247842, _247844, _247846]) = a_select3(_247846, 584 ^ [_247842, _247844, _247846], 583 ^ [_247842, _247844, _247846])]], 597 ^ _226311 : [(598 ^ _226311) ^ [] : [-(leq(n0, 595 ^ [_247842, _247844, _247846]))], (600 ^ _226311) ^ [] : [-(leq(595 ^ [_247842, _247844, _247846], _247842))], (602 ^ _226311) ^ [] : [-(leq(n0, 596 ^ [_247842, _247844, _247846]))], (604 ^ _226311) ^ [] : [-(leq(596 ^ [_247842, _247844, _247846], _247842))], (606 ^ _226311) ^ [] : [a_select3(_247844, 595 ^ [_247842, _247844, _247846], 596 ^ [_247842, _247844, _247846]) = a_select3(_247844, 596 ^ [_247842, _247844, _247846], 595 ^ [_247842, _247844, _247846])]], 607 ^ _226311 : [(608 ^ _226311) ^ [_249351, _249353] : [-(a_select3(tptp_msub(_247846, _247844), _249353, _249351) = a_select3(tptp_msub(_247846, _247844), _249351, _249353)), leq(n0, _249353), leq(_249353, _247842), leq(n0, _249351), leq(_249351, _247842)]]], (626 ^ _226311) ^ [_249937, _249939, _249941] : [629 ^ _226311 : [(630 ^ _226311) ^ [] : [-(leq(n0, 627 ^ [_249937, _249939, _249941]))], (632 ^ _226311) ^ [] : [-(leq(627 ^ [_249937, _249939, _249941], _249937))], (634 ^ _226311) ^ [] : [-(leq(n0, 628 ^ [_249937, _249939, _249941]))], (636 ^ _226311) ^ [] : [-(leq(628 ^ [_249937, _249939, _249941], _249937))], (638 ^ _226311) ^ [] : [a_select3(_249939, 627 ^ [_249937, _249939, _249941], 628 ^ [_249937, _249939, _249941]) = a_select3(_249939, 628 ^ [_249937, _249939, _249941], 627 ^ [_249937, _249939, _249941])]], 639 ^ _226311 : [(640 ^ _226311) ^ [_250750, _250752] : [-(a_select3(tptp_mmul(_249941, tptp_mmul(_249939, trans(_249941))), _250752, _250750) = a_select3(tptp_mmul(_249941, tptp_mmul(_249939, trans(_249941))), _250750, _250752)), leq(n0, _250752), leq(_250752, _249937), leq(n0, _250750), leq(_250750, _249937)]]], (658 ^ _226311) ^ [_251369, _251371, _251373, _251375] : [661 ^ _226311 : [(662 ^ _226311) ^ [] : [-(leq(n0, 659 ^ [_251369, _251371, _251373, _251375]))], (664 ^ _226311) ^ [] : [-(leq(659 ^ [_251369, _251371, _251373, _251375], _251369))], (666 ^ _226311) ^ [] : [-(leq(n0, 660 ^ [_251369, _251371, _251373, _251375]))], (668 ^ _226311) ^ [] : [-(leq(660 ^ [_251369, _251371, _251373, _251375], _251369))], (670 ^ _226311) ^ [] : [a_select3(_251373, 659 ^ [_251369, _251371, _251373, _251375], 660 ^ [_251369, _251371, _251373, _251375]) = a_select3(_251373, 660 ^ [_251369, _251371, _251373, _251375], 659 ^ [_251369, _251371, _251373, _251375])]], 671 ^ _226311 : [(672 ^ _226311) ^ [_252226, _252228] : [-(a_select3(tptp_mmul(_251375, tptp_mmul(_251373, trans(_251375))), _252228, _252226) = a_select3(tptp_mmul(_251375, tptp_mmul(_251373, trans(_251375))), _252226, _252228)), leq(n0, _252228), leq(_252228, _251371), leq(n0, _252226), leq(_252226, _251371)]]], (690 ^ _226311) ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935] : [695 ^ _226311 : [(696 ^ _226311) ^ [] : [-(leq(n0, 693 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935]))], (698 ^ _226311) ^ [] : [-(leq(693 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935], _252921))], (700 ^ _226311) ^ [] : [-(leq(n0, 694 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935]))], (702 ^ _226311) ^ [] : [-(leq(694 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935], _252921))], (704 ^ _226311) ^ [] : [a_select3(_252929, 693 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935], 694 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935]) = a_select3(_252929, 694 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935], 693 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935])]], 709 ^ _226311 : [(710 ^ _226311) ^ [] : [-(leq(n0, 707 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935]))], (712 ^ _226311) ^ [] : [-(leq(707 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935], _252923))], (714 ^ _226311) ^ [] : [-(leq(n0, 708 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935]))], (716 ^ _226311) ^ [] : [-(leq(708 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935], _252923))], (718 ^ _226311) ^ [] : [a_select3(_252935, 707 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935], 708 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935]) = a_select3(_252935, 708 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935], 707 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935])]], 721 ^ _226311 : [(722 ^ _226311) ^ [] : [-(leq(n0, 719 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935]))], (724 ^ _226311) ^ [] : [-(leq(719 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935], _252923))], (726 ^ _226311) ^ [] : [-(leq(n0, 720 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935]))], (728 ^ _226311) ^ [] : [-(leq(720 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935], _252923))], (730 ^ _226311) ^ [] : [a_select3(_252925, 719 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935], 720 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935]) = a_select3(_252925, 720 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935], 719 ^ [_252921, _252923, _252925, _252927, _252929, _252931, _252933, _252935])]], 731 ^ _226311 : [(732 ^ _226311) ^ [_255849, _255851] : [-(a_select3(tptp_madd(_252935, tptp_mmul(_252933, tptp_mmul(tptp_madd(tptp_mmul(_252931, tptp_mmul(_252929, trans(_252931))), tptp_mmul(_252927, tptp_mmul(_252925, trans(_252927)))), trans(_252933)))), _255851, _255849) = a_select3(tptp_madd(_252935, tptp_mmul(_252933, tptp_mmul(tptp_madd(tptp_mmul(_252931, tptp_mmul(_252929, trans(_252931))), tptp_mmul(_252927, tptp_mmul(_252925, trans(_252927)))), trans(_252933)))), _255849, _255851)), leq(n0, _255851), leq(_255851, _252923), leq(n0, _255849), leq(_255849, _252923)]]], (750 ^ _226311) ^ [_256602] : [-(sum(n0, tptp_minus_1, _256602) = n0)], (752 ^ _226311) ^ [_256684] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _256684))], (754 ^ _226311) ^ [] : [-(succ(tptp_minus_1) = n0)], (756 ^ _226311) ^ [_256819] : [-(plus(_256819, n1) = succ(_256819))], (758 ^ _226311) ^ [_256902] : [-(plus(n1, _256902) = succ(_256902))], (760 ^ _226311) ^ [_256985] : [-(plus(_256985, n2) = succ(succ(_256985)))], (762 ^ _226311) ^ [_257070] : [-(plus(n2, _257070) = succ(succ(_257070)))], (764 ^ _226311) ^ [_257155] : [-(plus(_257155, n3) = succ(succ(succ(_257155))))], (766 ^ _226311) ^ [_257242] : [-(plus(n3, _257242) = succ(succ(succ(_257242))))], (768 ^ _226311) ^ [_257329] : [-(plus(_257329, n4) = succ(succ(succ(succ(_257329)))))], (770 ^ _226311) ^ [_257418] : [-(plus(n4, _257418) = succ(succ(succ(succ(_257418)))))], (772 ^ _226311) ^ [_257507] : [-(plus(_257507, n5) = succ(succ(succ(succ(succ(_257507))))))], (774 ^ _226311) ^ [_257598] : [-(plus(n5, _257598) = succ(succ(succ(succ(succ(_257598))))))], (776 ^ _226311) ^ [_257689] : [-(minus(_257689, n1) = pred(_257689))], (778 ^ _226311) ^ [_257772] : [-(pred(succ(_257772)) = _257772)], (780 ^ _226311) ^ [_257854] : [-(succ(pred(_257854)) = _257854)], (782 ^ _226311) ^ [_257994, _257996] : [leq(succ(_257996), succ(_257994)), -(leq(_257996, _257994))], (788 ^ _226311) ^ [_258164, _258166] : [leq(_258166, _258164), -(leq(succ(_258166), succ(_258164)))], (794 ^ _226311) ^ [_258384, _258386] : [leq(succ(_258386), _258384), -(gt(_258384, _258386))], (800 ^ _226311) ^ [_258598, _258600] : [leq(minus(_258600, _258598), _258600), -(leq(n0, _258598))], (806 ^ _226311) ^ [_258827, _258829, _258831, _258833] : [-(a_select3(tptp_update3(_258833, _258831, _258829, _258827), _258831, _258829) = _258827)], (808 ^ _226311) ^ [_259019, _259021, _259023, _259025, _259027, _259029, _259031] : [-(a_select3(tptp_update3(_259023, _259031, _259029, _259019), _259027, _259025) = _259021), -(_259031 = _259027), _259029 = _259025, a_select3(_259023, _259027, _259025) = _259021], (822 ^ _226311) ^ [_259562, _259564, _259566, _259568, _259570, _259572] : [-(a_select3(tptp_update3(_259564, _259568, _259566, _259562), _259572, _259570) = _259562), 827 ^ _226311 : [(828 ^ _226311) ^ [] : [-(leq(n0, 825 ^ [_259562, _259564, _259566, _259568, _259570, _259572]))], (830 ^ _226311) ^ [] : [-(leq(n0, 826 ^ [_259562, _259564, _259566, _259568, _259570, _259572]))], (832 ^ _226311) ^ [] : [-(leq(825 ^ [_259562, _259564, _259566, _259568, _259570, _259572], _259568))], (834 ^ _226311) ^ [] : [-(leq(826 ^ [_259562, _259564, _259566, _259568, _259570, _259572], _259566))], (836 ^ _226311) ^ [] : [a_select3(_259564, 825 ^ [_259562, _259564, _259566, _259568, _259570, _259572], 826 ^ [_259562, _259564, _259566, _259568, _259570, _259572]) = _259562]], leq(n0, _259572), leq(_259572, _259568), leq(n0, _259570), leq(_259570, _259566)], (854 ^ _226311) ^ [_260904, _260906, _260908] : [-(a_select2(tptp_update2(_260908, _260906, _260904), _260906) = _260904)], (856 ^ _226311) ^ [_261064, _261066, _261068, _261070, _261072] : [-(a_select2(tptp_update2(_261068, _261072, _261064), _261070) = _261066), -(_261072 = _261070), a_select2(_261068, _261070) = _261066], (885 ^ _226311) ^ [] : [-(true)], (887 ^ _226311) ^ [] : [def = use], (866 ^ _226311) ^ [_261444, _261446, _261448, _261450] : [-(a_select2(tptp_update2(_261446, _261448, _261444), _261450) = _261444), 870 ^ _226311 : [(871 ^ _226311) ^ [] : [-(leq(n0, 869 ^ [_261444, _261446, _261448, _261450]))], (873 ^ _226311) ^ [] : [-(leq(869 ^ [_261444, _261446, _261448, _261450], _261448))], (875 ^ _226311) ^ [] : [a_select2(_261446, 869 ^ [_261444, _261446, _261448, _261450]) = _261444]], leq(n0, _261450), leq(_261450, _261448)]], input).
% 0.36/1.39 ncf('1',plain,[n0 = 1075 ^ [], n3 = 1074 ^ []],start(1127 ^ 0)).
% 0.36/1.39 ncf('1.1',plain,[-(n0 = 1075 ^ [])],extension(1297 ^ 1)).
% 0.36/1.39 ncf('1.2',plain,[-(n3 = 1074 ^ [])],extension(1299 ^ 1)).
% 0.36/1.39 %-----------------------------------------------------
% 0.36/1.39 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------