%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV213+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n021.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.34s 1.40s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWV213+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n021.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:32:27 EDT 2023
% 0.13/0.35 % CPUTime :
% 0.34/1.40
% 0.34/1.40 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.34/1.40 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.34/1.40 %-----------------------------------------------------
% 0.34/1.40 ncf(matrix, plain, [(1077 ^ _225263) ^ [] : [-(leq(n0, 1074 ^ []))], (1079 ^ _225263) ^ [] : [-(leq(n0, 1075 ^ []))], (1081 ^ _225263) ^ [] : [-(leq(1074 ^ [], n5))], (1083 ^ _225263) ^ [] : [-(leq(1075 ^ [], n5))], (1291 ^ _225263) ^ [] : [times(divide(n1, n400), a_select2(sigma, n2)) = n0], (1085 ^ _225263) ^ [] : [n0 = 1074 ^ [], n1 = 1075 ^ []], (1091 ^ _225263) ^ [] : [n0 = 1074 ^ [], n2 = 1075 ^ []], (1097 ^ _225263) ^ [] : [n0 = 1074 ^ [], n3 = 1075 ^ []], (1103 ^ _225263) ^ [] : [n0 = 1074 ^ [], n4 = 1075 ^ []], (1109 ^ _225263) ^ [] : [n0 = 1074 ^ [], n5 = 1075 ^ []], (1115 ^ _225263) ^ [] : [n0 = 1075 ^ [], n3 = 1074 ^ []], (1121 ^ _225263) ^ [] : [n0 = 1075 ^ [], n4 = 1074 ^ []], (1127 ^ _225263) ^ [] : [n0 = 1075 ^ [], n5 = 1074 ^ []], (1133 ^ _225263) ^ [] : [n1 = 1074 ^ [], n1 = 1075 ^ []], (1139 ^ _225263) ^ [] : [n1 = 1074 ^ [], n2 = 1075 ^ []], (1145 ^ _225263) ^ [] : [n1 = 1074 ^ [], n3 = 1075 ^ []], (1151 ^ _225263) ^ [] : [n1 = 1074 ^ [], n4 = 1075 ^ []], (1157 ^ _225263) ^ [] : [n1 = 1074 ^ [], n5 = 1075 ^ []], (1163 ^ _225263) ^ [] : [n1 = 1075 ^ [], n2 = 1074 ^ []], (1169 ^ _225263) ^ [] : [n1 = 1075 ^ [], n3 = 1074 ^ []], (1175 ^ _225263) ^ [] : [n1 = 1075 ^ [], n4 = 1074 ^ []], (1181 ^ _225263) ^ [] : [n1 = 1075 ^ [], n5 = 1074 ^ []], (1187 ^ _225263) ^ [] : [n2 = 1074 ^ [], n2 = 1075 ^ []], (1193 ^ _225263) ^ [] : [n2 = 1074 ^ [], n3 = 1075 ^ []], (1199 ^ _225263) ^ [] : [n2 = 1074 ^ [], n4 = 1075 ^ []], (1205 ^ _225263) ^ [] : [n2 = 1074 ^ [], n5 = 1075 ^ []], (1211 ^ _225263) ^ [] : [n2 = 1075 ^ [], n3 = 1074 ^ []], (1217 ^ _225263) ^ [] : [n2 = 1075 ^ [], n4 = 1074 ^ []], (1223 ^ _225263) ^ [] : [n2 = 1075 ^ [], n5 = 1074 ^ []], (1229 ^ _225263) ^ [] : [n3 = 1074 ^ [], n3 = 1075 ^ []], (1235 ^ _225263) ^ [] : [n3 = 1074 ^ [], n4 = 1075 ^ []], (1241 ^ _225263) ^ [] : [n3 = 1074 ^ [], n5 = 1075 ^ []], (1247 ^ _225263) ^ [] : [n3 = 1075 ^ [], n4 = 1074 ^ []], (1253 ^ _225263) ^ [] : [n3 = 1075 ^ [], n5 = 1074 ^ []], (1259 ^ _225263) ^ [] : [n4 = 1074 ^ [], n4 = 1075 ^ []], (1265 ^ _225263) ^ [] : [n4 = 1074 ^ [], n5 = 1075 ^ []], (1271 ^ _225263) ^ [] : [n4 = 1075 ^ [], n5 = 1074 ^ []], (1283 ^ _225263) ^ [] : [-(n0 = 1075 ^ [])], (1285 ^ _225263) ^ [] : [-(n2 = 1074 ^ [])], (1287 ^ _225263) ^ [] : [-(n2 = 1075 ^ [])], (1289 ^ _225263) ^ [] : [-(n3 = 1074 ^ [])], (1277 ^ _225263) ^ [] : [n5 = 1074 ^ [], n5 = 1075 ^ []], (2 ^ _225263) ^ [_225407] : [-(_225407 = _225407)], (4 ^ _225263) ^ [_225514, _225516] : [_225516 = _225514, -(_225514 = _225516)], (10 ^ _225263) ^ [_225718, _225720, _225722] : [-(_225722 = _225718), _225722 = _225720, _225720 = _225718], (20 ^ _225263) ^ [_226059, _226061, _226063, _226065] : [-(lt(_226063, _226059)), lt(_226065, _226061), _226065 = _226063, _226061 = _226059], (34 ^ _225263) ^ [_226503, _226505, _226507, _226509] : [-(geq(_226507, _226503)), geq(_226509, _226505), _226509 = _226507, _226505 = _226503], (48 ^ _225263) ^ [_226947, _226949, _226951, _226953] : [-(gt(_226951, _226947)), gt(_226953, _226949), _226953 = _226951, _226949 = _226947], (62 ^ _225263) ^ [_227371, _227373, _227375, _227377] : [-(leq(_227375, _227371)), leq(_227377, _227373), _227377 = _227375, _227373 = _227371], (76 ^ _225263) ^ [_227827, _227829, _227831, _227833] : [-(uniform_int_rnd(_227833, _227829) = uniform_int_rnd(_227831, _227827)), _227833 = _227831, _227829 = _227827], (86 ^ _225263) ^ [_228186, _228188, _228190, _228192] : [-(tptp_const_array1(_228192, _228188) = tptp_const_array1(_228190, _228186)), _228192 = _228190, _228188 = _228186], (96 ^ _225263) ^ [_228573, _228575, _228577, _228579, _228581, _228583] : [-(tptp_const_array2(_228583, _228579, _228575) = tptp_const_array2(_228581, _228577, _228573)), _228583 = _228581, _228579 = _228577, _228575 = _228573], (110 ^ _225263) ^ [_229061, _229063, _229065, _229067] : [-(dim(_229067, _229063) = dim(_229065, _229061)), _229067 = _229065, _229063 = _229061], (120 ^ _225263) ^ [_229392, _229394] : [_229394 = _229392, -(inv(_229394) = inv(_229392))], (126 ^ _225263) ^ [_229638, _229640, _229642, _229644] : [-(tptp_msub(_229644, _229640) = tptp_msub(_229642, _229638)), _229644 = _229642, _229640 = _229638], (136 ^ _225263) ^ [_229997, _229999, _230001, _230003] : [-(tptp_madd(_230003, _229999) = tptp_madd(_230001, _229997)), _230003 = _230001, _229999 = _229997], (146 ^ _225263) ^ [_230356, _230358, _230360, _230362] : [-(tptp_mmul(_230362, _230358) = tptp_mmul(_230360, _230356)), _230362 = _230360, _230358 = _230356], (156 ^ _225263) ^ [_230687, _230689] : [_230689 = _230687, -(trans(_230689) = trans(_230687))], (162 ^ _225263) ^ [_230961, _230963, _230965, _230967, _230969, _230971] : [-(sum(_230971, _230967, _230963) = sum(_230969, _230965, _230961)), _230971 = _230969, _230967 = _230965, _230963 = _230961], (176 ^ _225263) ^ [_231449, _231451, _231453, _231455] : [-(plus(_231455, _231451) = plus(_231453, _231449)), _231455 = _231453, _231451 = _231449], (186 ^ _225263) ^ [_231780, _231782] : [_231782 = _231780, -(pred(_231782) = pred(_231780))], (192 ^ _225263) ^ [_232026, _232028, _232030, _232032] : [-(minus(_232032, _232028) = minus(_232030, _232026)), _232032 = _232030, _232028 = _232026], (202 ^ _225263) ^ [_232413, _232415, _232417, _232419, _232421, _232423] : [-(a_select3(_232423, _232419, _232415) = a_select3(_232421, _232417, _232413)), _232423 = _232421, _232419 = _232417, _232415 = _232413], (216 ^ _225263) ^ [_232957, _232959, _232961, _232963, _232965, _232967, _232969, _232971] : [-(tptp_update3(_232971, _232967, _232963, _232959) = tptp_update3(_232969, _232965, _232961, _232957)), _232971 = _232969, _232967 = _232965, _232963 = _232961, _232959 = _232957], (234 ^ _225263) ^ [_233618, _233620, _233622, _233624, _233626, _233628] : [-(tptp_update2(_233628, _233624, _233620) = tptp_update2(_233626, _233622, _233618)), _233628 = _233626, _233624 = _233622, _233620 = _233618], (248 ^ _225263) ^ [_234078, _234080] : [_234080 = _234078, -(succ(_234080) = succ(_234078))], (254 ^ _225263) ^ [_234324, _234326, _234328, _234330] : [-(times(_234330, _234326) = times(_234328, _234324)), _234330 = _234328, _234326 = _234324], (264 ^ _225263) ^ [_234683, _234685, _234687, _234689] : [-(divide(_234689, _234685) = divide(_234687, _234683)), _234689 = _234687, _234685 = _234683], (274 ^ _225263) ^ [_235022, _235024, _235026, _235028] : [-(a_select2(_235028, _235024) = a_select2(_235026, _235022)), _235028 = _235026, _235024 = _235022], (889 ^ _225263) ^ [] : [-(gt(n5, n4))], (891 ^ _225263) ^ [] : [-(gt(n400, n4))], (893 ^ _225263) ^ [] : [-(gt(n400, n5))], (895 ^ _225263) ^ [] : [-(gt(n4, tptp_minus_1))], (897 ^ _225263) ^ [] : [-(gt(n5, tptp_minus_1))], (899 ^ _225263) ^ [] : [-(gt(n400, tptp_minus_1))], (901 ^ _225263) ^ [] : [-(gt(n0, tptp_minus_1))], (903 ^ _225263) ^ [] : [-(gt(n1, tptp_minus_1))], (905 ^ _225263) ^ [] : [-(gt(n2, tptp_minus_1))], (907 ^ _225263) ^ [] : [-(gt(n3, tptp_minus_1))], (909 ^ _225263) ^ [] : [-(gt(n4, n0))], (911 ^ _225263) ^ [] : [-(gt(n5, n0))], (913 ^ _225263) ^ [] : [-(gt(n400, n0))], (915 ^ _225263) ^ [] : [-(gt(n1, n0))], (917 ^ _225263) ^ [] : [-(gt(n2, n0))], (919 ^ _225263) ^ [] : [-(gt(n3, n0))], (921 ^ _225263) ^ [] : [-(gt(n4, n1))], (923 ^ _225263) ^ [] : [-(gt(n5, n1))], (925 ^ _225263) ^ [] : [-(gt(n400, n1))], (927 ^ _225263) ^ [] : [-(gt(n2, n1))], (929 ^ _225263) ^ [] : [-(gt(n3, n1))], (931 ^ _225263) ^ [] : [-(gt(n4, n2))], (933 ^ _225263) ^ [] : [-(gt(n5, n2))], (935 ^ _225263) ^ [] : [-(gt(n400, n2))], (937 ^ _225263) ^ [] : [-(gt(n3, n2))], (939 ^ _225263) ^ [] : [-(gt(n4, n3))], (941 ^ _225263) ^ [] : [-(gt(n5, n3))], (943 ^ _225263) ^ [] : [-(gt(n400, n3))], (945 ^ _225263) ^ [_262870] : [leq(n0, _262870), leq(_262870, n4), -(_262870 = n0), -(_262870 = n1), -(_262870 = n2), -(_262870 = n3), -(_262870 = n4)], (971 ^ _225263) ^ [_263491] : [leq(n0, _263491), leq(_263491, n5), -(_263491 = n0), -(_263491 = n1), -(_263491 = n2), -(_263491 = n3), -(_263491 = n4), -(_263491 = n5)], (1001 ^ _225263) ^ [_264198] : [-(_264198 = n0), leq(n0, _264198), leq(_264198, n0)], (1011 ^ _225263) ^ [_264473] : [leq(n0, _264473), leq(_264473, n1), -(_264473 = n0), -(_264473 = n1)], (1025 ^ _225263) ^ [_264836] : [leq(n0, _264836), leq(_264836, n2), -(_264836 = n0), -(_264836 = n1), -(_264836 = n2)], (1065 ^ _225263) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (1067 ^ _225263) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (1069 ^ _225263) ^ [] : [-(succ(n0) = n1)], (1071 ^ _225263) ^ [] : [-(succ(succ(n0)) = n2)], (1073 ^ _225263) ^ [] : [-(succ(succ(succ(n0))) = n3)], (1043 ^ _225263) ^ [_265285] : [leq(n0, _265285), leq(_265285, n3), -(_265285 = n0), -(_265285 = n1), -(_265285 = n2), -(_265285 = n3)], (284 ^ _225263) ^ [_235461, _235463] : [-(gt(_235463, _235461)), -(gt(_235461, _235463)), -(_235463 = _235461)], (294 ^ _225263) ^ [_235776, _235778, _235780] : [-(gt(_235780, _235776)), gt(_235780, _235778), gt(_235778, _235776)], (304 ^ _225263) ^ [_236055] : [gt(_236055, _236055)], (306 ^ _225263) ^ [_236133] : [-(leq(_236133, _236133))], (308 ^ _225263) ^ [_236254, _236256, _236258] : [-(leq(_236258, _236254)), leq(_236258, _236256), leq(_236256, _236254)], (318 ^ _225263) ^ [_236592, _236594] : [lt(_236594, _236592), -(gt(_236592, _236594))], (324 ^ _225263) ^ [_236754, _236756] : [gt(_236754, _236756), -(lt(_236756, _236754))], (330 ^ _225263) ^ [_236995, _236997] : [geq(_236997, _236995), -(leq(_236995, _236997))], (336 ^ _225263) ^ [_237157, _237159] : [leq(_237157, _237159), -(geq(_237159, _237157))], (342 ^ _225263) ^ [_237369, _237371] : [gt(_237369, _237371), -(leq(_237371, _237369))], (348 ^ _225263) ^ [_237579, _237581] : [-(gt(_237579, _237581)), leq(_237581, _237579), -(_237581 = _237579)], (358 ^ _225263) ^ [_237910, _237912] : [leq(_237912, pred(_237910)), -(gt(_237910, _237912))], (364 ^ _225263) ^ [_238076, _238078] : [gt(_238076, _238078), -(leq(_238078, pred(_238076)))], (370 ^ _225263) ^ [_238263] : [-(gt(succ(_238263), _238263))], (372 ^ _225263) ^ [_238372, _238374] : [leq(_238374, _238372), -(leq(_238374, succ(_238372)))], (378 ^ _225263) ^ [_238615, _238617] : [leq(_238617, _238615), -(gt(succ(_238615), _238617))], (384 ^ _225263) ^ [_238781, _238783] : [gt(succ(_238781), _238783), -(leq(_238783, _238781))], (390 ^ _225263) ^ [_238997, _238999] : [leq(n0, _238999), -(leq(uniform_int_rnd(_238997, _238999), _238999))], (396 ^ _225263) ^ [_239213, _239215] : [leq(n0, _239215), -(leq(n0, uniform_int_rnd(_239213, _239215)))], (402 ^ _225263) ^ [_239457, _239459, _239461, _239463] : [-(a_select2(tptp_const_array1(dim(_239461, _239459), _239457), _239463) = _239457), leq(_239461, _239463), leq(_239463, _239459)], (412 ^ _225263) ^ [_239864, _239866, _239868, _239870, _239872, _239874, _239876] : [-(a_select3(tptp_const_array2(dim(_239874, _239872), dim(_239868, _239866), _239864), _239876, _239870) = _239864), leq(_239874, _239876), leq(_239876, _239872), leq(_239868, _239870), leq(_239870, _239866)], (430 ^ _225263) ^ [_240459, _240461] : [433 ^ _225263 : [(434 ^ _225263) ^ [] : [-(leq(n0, 431 ^ [_240459, _240461]))], (436 ^ _225263) ^ [] : [-(leq(431 ^ [_240459, _240461], _240459))], (438 ^ _225263) ^ [] : [-(leq(n0, 432 ^ [_240459, _240461]))], (440 ^ _225263) ^ [] : [-(leq(432 ^ [_240459, _240461], _240459))], (442 ^ _225263) ^ [] : [a_select3(_240461, 431 ^ [_240459, _240461], 432 ^ [_240459, _240461]) = a_select3(_240461, 432 ^ [_240459, _240461], 431 ^ [_240459, _240461])]], 443 ^ _225263 : [(444 ^ _225263) ^ [_241216, _241218] : [-(a_select3(trans(_240461), _241218, _241216) = a_select3(trans(_240461), _241216, _241218)), leq(n0, _241218), leq(_241218, _240459), leq(n0, _241216), leq(_241216, _240459)]]], (462 ^ _225263) ^ [_241763, _241765] : [465 ^ _225263 : [(466 ^ _225263) ^ [] : [-(leq(n0, 463 ^ [_241763, _241765]))], (468 ^ _225263) ^ [] : [-(leq(463 ^ [_241763, _241765], _241763))], (470 ^ _225263) ^ [] : [-(leq(n0, 464 ^ [_241763, _241765]))], (472 ^ _225263) ^ [] : [-(leq(464 ^ [_241763, _241765], _241763))], (474 ^ _225263) ^ [] : [a_select3(_241765, 463 ^ [_241763, _241765], 464 ^ [_241763, _241765]) = a_select3(_241765, 464 ^ [_241763, _241765], 463 ^ [_241763, _241765])]], 475 ^ _225263 : [(476 ^ _225263) ^ [_242520, _242522] : [-(a_select3(inv(_241765), _242522, _242520) = a_select3(inv(_241765), _242520, _242522)), leq(n0, _242522), leq(_242522, _241763), leq(n0, _242520), leq(_242520, _241763)]]], (494 ^ _225263) ^ [_243067, _243069] : [497 ^ _225263 : [(498 ^ _225263) ^ [] : [-(leq(n0, 495 ^ [_243067, _243069]))], (500 ^ _225263) ^ [] : [-(leq(495 ^ [_243067, _243069], _243067))], (502 ^ _225263) ^ [] : [-(leq(n0, 496 ^ [_243067, _243069]))], (504 ^ _225263) ^ [] : [-(leq(496 ^ [_243067, _243069], _243067))], (506 ^ _225263) ^ [] : [a_select3(_243069, 495 ^ [_243067, _243069], 496 ^ [_243067, _243069]) = a_select3(_243069, 496 ^ [_243067, _243069], 495 ^ [_243067, _243069])]], 507 ^ _225263 : [(508 ^ _225263) ^ [_243880, _243882, _243884, _243886] : [-(a_select3(tptp_update3(_243069, _243882, _243882, _243880), _243886, _243884) = a_select3(tptp_update3(_243069, _243882, _243882, _243880), _243884, _243886)), leq(n0, _243886), leq(_243886, _243067), leq(n0, _243884), leq(_243884, _243067), leq(n0, _243882), leq(_243882, _243067)]]], (534 ^ _225263) ^ [_244699, _244701, _244703] : [539 ^ _225263 : [(540 ^ _225263) ^ [] : [-(leq(n0, 537 ^ [_244699, _244701, _244703]))], (542 ^ _225263) ^ [] : [-(leq(537 ^ [_244699, _244701, _244703], _244699))], (544 ^ _225263) ^ [] : [-(leq(n0, 538 ^ [_244699, _244701, _244703]))], (546 ^ _225263) ^ [] : [-(leq(538 ^ [_244699, _244701, _244703], _244699))], (548 ^ _225263) ^ [] : [a_select3(_244703, 537 ^ [_244699, _244701, _244703], 538 ^ [_244699, _244701, _244703]) = a_select3(_244703, 538 ^ [_244699, _244701, _244703], 537 ^ [_244699, _244701, _244703])]], 551 ^ _225263 : [(552 ^ _225263) ^ [] : [-(leq(n0, 549 ^ [_244699, _244701, _244703]))], (554 ^ _225263) ^ [] : [-(leq(549 ^ [_244699, _244701, _244703], _244699))], (556 ^ _225263) ^ [] : [-(leq(n0, 550 ^ [_244699, _244701, _244703]))], (558 ^ _225263) ^ [] : [-(leq(550 ^ [_244699, _244701, _244703], _244699))], (560 ^ _225263) ^ [] : [a_select3(_244701, 549 ^ [_244699, _244701, _244703], 550 ^ [_244699, _244701, _244703]) = a_select3(_244701, 550 ^ [_244699, _244701, _244703], 549 ^ [_244699, _244701, _244703])]], 561 ^ _225263 : [(562 ^ _225263) ^ [_246208, _246210] : [-(a_select3(tptp_madd(_244703, _244701), _246210, _246208) = a_select3(tptp_madd(_244703, _244701), _246208, _246210)), leq(n0, _246210), leq(_246210, _244699), leq(n0, _246208), leq(_246208, _244699)]]], (580 ^ _225263) ^ [_246794, _246796, _246798] : [585 ^ _225263 : [(586 ^ _225263) ^ [] : [-(leq(n0, 583 ^ [_246794, _246796, _246798]))], (588 ^ _225263) ^ [] : [-(leq(583 ^ [_246794, _246796, _246798], _246794))], (590 ^ _225263) ^ [] : [-(leq(n0, 584 ^ [_246794, _246796, _246798]))], (592 ^ _225263) ^ [] : [-(leq(584 ^ [_246794, _246796, _246798], _246794))], (594 ^ _225263) ^ [] : [a_select3(_246798, 583 ^ [_246794, _246796, _246798], 584 ^ [_246794, _246796, _246798]) = a_select3(_246798, 584 ^ [_246794, _246796, _246798], 583 ^ [_246794, _246796, _246798])]], 597 ^ _225263 : [(598 ^ _225263) ^ [] : [-(leq(n0, 595 ^ [_246794, _246796, _246798]))], (600 ^ _225263) ^ [] : [-(leq(595 ^ [_246794, _246796, _246798], _246794))], (602 ^ _225263) ^ [] : [-(leq(n0, 596 ^ [_246794, _246796, _246798]))], (604 ^ _225263) ^ [] : [-(leq(596 ^ [_246794, _246796, _246798], _246794))], (606 ^ _225263) ^ [] : [a_select3(_246796, 595 ^ [_246794, _246796, _246798], 596 ^ [_246794, _246796, _246798]) = a_select3(_246796, 596 ^ [_246794, _246796, _246798], 595 ^ [_246794, _246796, _246798])]], 607 ^ _225263 : [(608 ^ _225263) ^ [_248303, _248305] : [-(a_select3(tptp_msub(_246798, _246796), _248305, _248303) = a_select3(tptp_msub(_246798, _246796), _248303, _248305)), leq(n0, _248305), leq(_248305, _246794), leq(n0, _248303), leq(_248303, _246794)]]], (626 ^ _225263) ^ [_248889, _248891, _248893] : [629 ^ _225263 : [(630 ^ _225263) ^ [] : [-(leq(n0, 627 ^ [_248889, _248891, _248893]))], (632 ^ _225263) ^ [] : [-(leq(627 ^ [_248889, _248891, _248893], _248889))], (634 ^ _225263) ^ [] : [-(leq(n0, 628 ^ [_248889, _248891, _248893]))], (636 ^ _225263) ^ [] : [-(leq(628 ^ [_248889, _248891, _248893], _248889))], (638 ^ _225263) ^ [] : [a_select3(_248891, 627 ^ [_248889, _248891, _248893], 628 ^ [_248889, _248891, _248893]) = a_select3(_248891, 628 ^ [_248889, _248891, _248893], 627 ^ [_248889, _248891, _248893])]], 639 ^ _225263 : [(640 ^ _225263) ^ [_249702, _249704] : [-(a_select3(tptp_mmul(_248893, tptp_mmul(_248891, trans(_248893))), _249704, _249702) = a_select3(tptp_mmul(_248893, tptp_mmul(_248891, trans(_248893))), _249702, _249704)), leq(n0, _249704), leq(_249704, _248889), leq(n0, _249702), leq(_249702, _248889)]]], (658 ^ _225263) ^ [_250321, _250323, _250325, _250327] : [661 ^ _225263 : [(662 ^ _225263) ^ [] : [-(leq(n0, 659 ^ [_250321, _250323, _250325, _250327]))], (664 ^ _225263) ^ [] : [-(leq(659 ^ [_250321, _250323, _250325, _250327], _250321))], (666 ^ _225263) ^ [] : [-(leq(n0, 660 ^ [_250321, _250323, _250325, _250327]))], (668 ^ _225263) ^ [] : [-(leq(660 ^ [_250321, _250323, _250325, _250327], _250321))], (670 ^ _225263) ^ [] : [a_select3(_250325, 659 ^ [_250321, _250323, _250325, _250327], 660 ^ [_250321, _250323, _250325, _250327]) = a_select3(_250325, 660 ^ [_250321, _250323, _250325, _250327], 659 ^ [_250321, _250323, _250325, _250327])]], 671 ^ _225263 : [(672 ^ _225263) ^ [_251178, _251180] : [-(a_select3(tptp_mmul(_250327, tptp_mmul(_250325, trans(_250327))), _251180, _251178) = a_select3(tptp_mmul(_250327, tptp_mmul(_250325, trans(_250327))), _251178, _251180)), leq(n0, _251180), leq(_251180, _250323), leq(n0, _251178), leq(_251178, _250323)]]], (690 ^ _225263) ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887] : [695 ^ _225263 : [(696 ^ _225263) ^ [] : [-(leq(n0, 693 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887]))], (698 ^ _225263) ^ [] : [-(leq(693 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887], _251873))], (700 ^ _225263) ^ [] : [-(leq(n0, 694 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887]))], (702 ^ _225263) ^ [] : [-(leq(694 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887], _251873))], (704 ^ _225263) ^ [] : [a_select3(_251881, 693 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887], 694 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887]) = a_select3(_251881, 694 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887], 693 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887])]], 709 ^ _225263 : [(710 ^ _225263) ^ [] : [-(leq(n0, 707 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887]))], (712 ^ _225263) ^ [] : [-(leq(707 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887], _251875))], (714 ^ _225263) ^ [] : [-(leq(n0, 708 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887]))], (716 ^ _225263) ^ [] : [-(leq(708 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887], _251875))], (718 ^ _225263) ^ [] : [a_select3(_251887, 707 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887], 708 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887]) = a_select3(_251887, 708 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887], 707 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887])]], 721 ^ _225263 : [(722 ^ _225263) ^ [] : [-(leq(n0, 719 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887]))], (724 ^ _225263) ^ [] : [-(leq(719 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887], _251875))], (726 ^ _225263) ^ [] : [-(leq(n0, 720 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887]))], (728 ^ _225263) ^ [] : [-(leq(720 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887], _251875))], (730 ^ _225263) ^ [] : [a_select3(_251877, 719 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887], 720 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887]) = a_select3(_251877, 720 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887], 719 ^ [_251873, _251875, _251877, _251879, _251881, _251883, _251885, _251887])]], 731 ^ _225263 : [(732 ^ _225263) ^ [_254801, _254803] : [-(a_select3(tptp_madd(_251887, tptp_mmul(_251885, tptp_mmul(tptp_madd(tptp_mmul(_251883, tptp_mmul(_251881, trans(_251883))), tptp_mmul(_251879, tptp_mmul(_251877, trans(_251879)))), trans(_251885)))), _254803, _254801) = a_select3(tptp_madd(_251887, tptp_mmul(_251885, tptp_mmul(tptp_madd(tptp_mmul(_251883, tptp_mmul(_251881, trans(_251883))), tptp_mmul(_251879, tptp_mmul(_251877, trans(_251879)))), trans(_251885)))), _254801, _254803)), leq(n0, _254803), leq(_254803, _251875), leq(n0, _254801), leq(_254801, _251875)]]], (750 ^ _225263) ^ [_255554] : [-(sum(n0, tptp_minus_1, _255554) = n0)], (752 ^ _225263) ^ [_255636] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _255636))], (754 ^ _225263) ^ [] : [-(succ(tptp_minus_1) = n0)], (756 ^ _225263) ^ [_255771] : [-(plus(_255771, n1) = succ(_255771))], (758 ^ _225263) ^ [_255854] : [-(plus(n1, _255854) = succ(_255854))], (760 ^ _225263) ^ [_255937] : [-(plus(_255937, n2) = succ(succ(_255937)))], (762 ^ _225263) ^ [_256022] : [-(plus(n2, _256022) = succ(succ(_256022)))], (764 ^ _225263) ^ [_256107] : [-(plus(_256107, n3) = succ(succ(succ(_256107))))], (766 ^ _225263) ^ [_256194] : [-(plus(n3, _256194) = succ(succ(succ(_256194))))], (768 ^ _225263) ^ [_256281] : [-(plus(_256281, n4) = succ(succ(succ(succ(_256281)))))], (770 ^ _225263) ^ [_256370] : [-(plus(n4, _256370) = succ(succ(succ(succ(_256370)))))], (772 ^ _225263) ^ [_256459] : [-(plus(_256459, n5) = succ(succ(succ(succ(succ(_256459))))))], (774 ^ _225263) ^ [_256550] : [-(plus(n5, _256550) = succ(succ(succ(succ(succ(_256550))))))], (776 ^ _225263) ^ [_256641] : [-(minus(_256641, n1) = pred(_256641))], (778 ^ _225263) ^ [_256724] : [-(pred(succ(_256724)) = _256724)], (780 ^ _225263) ^ [_256806] : [-(succ(pred(_256806)) = _256806)], (782 ^ _225263) ^ [_256946, _256948] : [leq(succ(_256948), succ(_256946)), -(leq(_256948, _256946))], (788 ^ _225263) ^ [_257116, _257118] : [leq(_257118, _257116), -(leq(succ(_257118), succ(_257116)))], (794 ^ _225263) ^ [_257336, _257338] : [leq(succ(_257338), _257336), -(gt(_257336, _257338))], (800 ^ _225263) ^ [_257550, _257552] : [leq(minus(_257552, _257550), _257552), -(leq(n0, _257550))], (806 ^ _225263) ^ [_257779, _257781, _257783, _257785] : [-(a_select3(tptp_update3(_257785, _257783, _257781, _257779), _257783, _257781) = _257779)], (808 ^ _225263) ^ [_257971, _257973, _257975, _257977, _257979, _257981, _257983] : [-(a_select3(tptp_update3(_257975, _257983, _257981, _257971), _257979, _257977) = _257973), -(_257983 = _257979), _257981 = _257977, a_select3(_257975, _257979, _257977) = _257973], (822 ^ _225263) ^ [_258514, _258516, _258518, _258520, _258522, _258524] : [-(a_select3(tptp_update3(_258516, _258520, _258518, _258514), _258524, _258522) = _258514), 827 ^ _225263 : [(828 ^ _225263) ^ [] : [-(leq(n0, 825 ^ [_258514, _258516, _258518, _258520, _258522, _258524]))], (830 ^ _225263) ^ [] : [-(leq(n0, 826 ^ [_258514, _258516, _258518, _258520, _258522, _258524]))], (832 ^ _225263) ^ [] : [-(leq(825 ^ [_258514, _258516, _258518, _258520, _258522, _258524], _258520))], (834 ^ _225263) ^ [] : [-(leq(826 ^ [_258514, _258516, _258518, _258520, _258522, _258524], _258518))], (836 ^ _225263) ^ [] : [a_select3(_258516, 825 ^ [_258514, _258516, _258518, _258520, _258522, _258524], 826 ^ [_258514, _258516, _258518, _258520, _258522, _258524]) = _258514]], leq(n0, _258524), leq(_258524, _258520), leq(n0, _258522), leq(_258522, _258518)], (854 ^ _225263) ^ [_259856, _259858, _259860] : [-(a_select2(tptp_update2(_259860, _259858, _259856), _259858) = _259856)], (856 ^ _225263) ^ [_260016, _260018, _260020, _260022, _260024] : [-(a_select2(tptp_update2(_260020, _260024, _260016), _260022) = _260018), -(_260024 = _260022), a_select2(_260020, _260022) = _260018], (885 ^ _225263) ^ [] : [-(true)], (887 ^ _225263) ^ [] : [def = use], (866 ^ _225263) ^ [_260396, _260398, _260400, _260402] : [-(a_select2(tptp_update2(_260398, _260400, _260396), _260402) = _260396), 870 ^ _225263 : [(871 ^ _225263) ^ [] : [-(leq(n0, 869 ^ [_260396, _260398, _260400, _260402]))], (873 ^ _225263) ^ [] : [-(leq(869 ^ [_260396, _260398, _260400, _260402], _260400))], (875 ^ _225263) ^ [] : [a_select2(_260398, 869 ^ [_260396, _260398, _260400, _260402]) = _260396]], leq(n0, _260402), leq(_260402, _260400)]], input).
% 0.34/1.40 ncf('1',plain,[n0 = 1075 ^ [], n3 = 1074 ^ []],start(1115 ^ 0)).
% 0.34/1.40 ncf('1.1',plain,[-(n0 = 1075 ^ [])],extension(1283 ^ 1)).
% 0.34/1.40 ncf('1.2',plain,[-(n3 = 1074 ^ [])],extension(1289 ^ 1)).
% 0.34/1.40 %-----------------------------------------------------
% 0.34/1.40 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------