%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV156+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n004.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:04 EDT 2023
% Result : Theorem 8.96s 9.70s
% Output : Proof 8.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWV156+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n004.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:23:39 EDT 2023
% 0.13/0.35 % CPUTime :
% 8.96/9.70
% 8.96/9.70 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 8.96/9.70 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.96/9.70 %-----------------------------------------------------
% 8.96/9.70 ncf(matrix, plain, [(1136 ^ _217006) ^ [] : [-(leq(n0, 1134 ^ []))], (1138 ^ _217006) ^ [] : [-(leq(1134 ^ [], pred(pv10)))], (1140 ^ _217006) ^ [] : [-(pv10 = 1134 ^ [])], (1142 ^ _217006) ^ [] : [sum(n0, n4, cond(tptp_term_equals(pv12, tptp_sum_index), divide(sqrt(times(minus(a_select3(center, pv12, n0), a_select2(x, pv10)), minus(a_select3(center, pv12, n0), a_select2(x, pv10)))), pv70), a_select3(q, 1134 ^ [], tptp_sum_index))) = n1], (1105 ^ _217006) ^ [] : [-(pv70 = sum(n0, n4, sqrt(times(minus(a_select3(center, tptp_sum_index, n0), a_select2(x, pv10)), minus(a_select3(center, tptp_sum_index, n0), a_select2(x, pv10))))))], (1107 ^ _217006) ^ [] : [-(leq(n0, pv10))], (1109 ^ _217006) ^ [] : [-(leq(n0, pv12))], (1111 ^ _217006) ^ [] : [-(leq(pv10, n135299))], (1113 ^ _217006) ^ [] : [-(leq(pv12, n4))], (1115 ^ _217006) ^ [_259434] : [-(a_select3(q, pv10, _259434) = divide(sqrt(times(minus(a_select3(center, _259434, n0), a_select2(x, pv10)), minus(a_select3(center, _259434, n0), a_select2(x, pv10)))), sum(n0, n4, sqrt(times(minus(a_select3(center, tptp_sum_index, n0), a_select2(x, pv10)), minus(a_select3(center, tptp_sum_index, n0), a_select2(x, pv10))))))), leq(n0, _259434), leq(_259434, pred(pv12))], (1125 ^ _217006) ^ [_259741] : [-(sum(n0, n4, a_select3(q, _259741, tptp_sum_index)) = n1), leq(n0, _259741), leq(_259741, pred(pv10))], (2 ^ _217006) ^ [_217150] : [-(_217150 = _217150)], (4 ^ _217006) ^ [_217257, _217259] : [_217259 = _217257, -(_217257 = _217259)], (10 ^ _217006) ^ [_217461, _217463, _217465] : [-(_217465 = _217461), _217465 = _217463, _217463 = _217461], (20 ^ _217006) ^ [_217802, _217804, _217806, _217808] : [-(lt(_217806, _217802)), lt(_217808, _217804), _217808 = _217806, _217804 = _217802], (34 ^ _217006) ^ [_218246, _218248, _218250, _218252] : [-(geq(_218250, _218246)), geq(_218252, _218248), _218252 = _218250, _218248 = _218246], (48 ^ _217006) ^ [_218690, _218692, _218694, _218696] : [-(gt(_218694, _218690)), gt(_218696, _218692), _218696 = _218694, _218692 = _218690], (62 ^ _217006) ^ [_219114, _219116, _219118, _219120] : [-(leq(_219118, _219114)), leq(_219120, _219116), _219120 = _219118, _219116 = _219114], (76 ^ _217006) ^ [_219570, _219572, _219574, _219576] : [-(uniform_int_rnd(_219576, _219572) = uniform_int_rnd(_219574, _219570)), _219576 = _219574, _219572 = _219570], (86 ^ _217006) ^ [_219929, _219931, _219933, _219935] : [-(tptp_const_array1(_219935, _219931) = tptp_const_array1(_219933, _219929)), _219935 = _219933, _219931 = _219929], (96 ^ _217006) ^ [_220316, _220318, _220320, _220322, _220324, _220326] : [-(tptp_const_array2(_220326, _220322, _220318) = tptp_const_array2(_220324, _220320, _220316)), _220326 = _220324, _220322 = _220320, _220318 = _220316], (110 ^ _217006) ^ [_220804, _220806, _220808, _220810] : [-(dim(_220810, _220806) = dim(_220808, _220804)), _220810 = _220808, _220806 = _220804], (120 ^ _217006) ^ [_221135, _221137] : [_221137 = _221135, -(inv(_221137) = inv(_221135))], (126 ^ _217006) ^ [_221381, _221383, _221385, _221387] : [-(tptp_msub(_221387, _221383) = tptp_msub(_221385, _221381)), _221387 = _221385, _221383 = _221381], (136 ^ _217006) ^ [_221740, _221742, _221744, _221746] : [-(tptp_madd(_221746, _221742) = tptp_madd(_221744, _221740)), _221746 = _221744, _221742 = _221740], (146 ^ _217006) ^ [_222099, _222101, _222103, _222105] : [-(tptp_mmul(_222105, _222101) = tptp_mmul(_222103, _222099)), _222105 = _222103, _222101 = _222099], (156 ^ _217006) ^ [_222430, _222432] : [_222432 = _222430, -(trans(_222432) = trans(_222430))], (162 ^ _217006) ^ [_222676, _222678, _222680, _222682] : [-(plus(_222682, _222678) = plus(_222680, _222676)), _222682 = _222680, _222678 = _222676], (172 ^ _217006) ^ [_223091, _223093, _223095, _223097, _223099, _223101, _223103, _223105] : [-(tptp_update3(_223105, _223101, _223097, _223093) = tptp_update3(_223103, _223099, _223095, _223091)), _223105 = _223103, _223101 = _223099, _223097 = _223095, _223093 = _223091], (190 ^ _217006) ^ [_223752, _223754, _223756, _223758, _223760, _223762] : [-(tptp_update2(_223762, _223758, _223754) = tptp_update2(_223760, _223756, _223752)), _223762 = _223760, _223758 = _223756, _223754 = _223752], (204 ^ _217006) ^ [_224212, _224214] : [_224214 = _224212, -(succ(_224214) = succ(_224212))], (210 ^ _217006) ^ [_224430, _224432] : [_224432 = _224430, -(pred(_224432) = pred(_224430))], (216 ^ _217006) ^ [_224704, _224706, _224708, _224710, _224712, _224714] : [-(sum(_224714, _224710, _224706) = sum(_224712, _224708, _224704)), _224714 = _224712, _224710 = _224708, _224706 = _224704], (230 ^ _217006) ^ [_225220, _225222, _225224, _225226, _225228, _225230] : [-(cond(_225230, _225226, _225222) = cond(_225228, _225224, _225220)), _225230 = _225228, _225226 = _225224, _225222 = _225220], (244 ^ _217006) ^ [_225708, _225710, _225712, _225714] : [-(tptp_term_equals(_225714, _225710) = tptp_term_equals(_225712, _225708)), _225714 = _225712, _225710 = _225708], (254 ^ _217006) ^ [_226067, _226069, _226071, _226073] : [-(divide(_226073, _226069) = divide(_226071, _226067)), _226073 = _226071, _226069 = _226067], (264 ^ _217006) ^ [_226398, _226400] : [_226400 = _226398, -(sqrt(_226400) = sqrt(_226398))], (270 ^ _217006) ^ [_226644, _226646, _226648, _226650] : [-(times(_226650, _226646) = times(_226648, _226644)), _226650 = _226648, _226646 = _226644], (280 ^ _217006) ^ [_227003, _227005, _227007, _227009] : [-(minus(_227009, _227005) = minus(_227007, _227003)), _227009 = _227007, _227005 = _227003], (290 ^ _217006) ^ [_227362, _227364, _227366, _227368] : [-(a_select2(_227368, _227364) = a_select2(_227366, _227362)), _227368 = _227366, _227364 = _227362], (300 ^ _217006) ^ [_227729, _227731, _227733, _227735, _227737, _227739] : [-(a_select3(_227739, _227735, _227731) = a_select3(_227737, _227733, _227729)), _227739 = _227737, _227735 = _227733, _227731 = _227729], (919 ^ _217006) ^ [] : [-(gt(n5, n4))], (921 ^ _217006) ^ [] : [-(gt(n135299, n4))], (923 ^ _217006) ^ [] : [-(gt(n135299, n5))], (925 ^ _217006) ^ [] : [-(gt(n4, tptp_minus_1))], (927 ^ _217006) ^ [] : [-(gt(n5, tptp_minus_1))], (929 ^ _217006) ^ [] : [-(gt(n135299, tptp_minus_1))], (931 ^ _217006) ^ [] : [-(gt(n0, tptp_minus_1))], (933 ^ _217006) ^ [] : [-(gt(n1, tptp_minus_1))], (935 ^ _217006) ^ [] : [-(gt(n2, tptp_minus_1))], (937 ^ _217006) ^ [] : [-(gt(n3, tptp_minus_1))], (939 ^ _217006) ^ [] : [-(gt(n4, n0))], (941 ^ _217006) ^ [] : [-(gt(n5, n0))], (943 ^ _217006) ^ [] : [-(gt(n135299, n0))], (945 ^ _217006) ^ [] : [-(gt(n1, n0))], (947 ^ _217006) ^ [] : [-(gt(n2, n0))], (949 ^ _217006) ^ [] : [-(gt(n3, n0))], (951 ^ _217006) ^ [] : [-(gt(n4, n1))], (953 ^ _217006) ^ [] : [-(gt(n5, n1))], (955 ^ _217006) ^ [] : [-(gt(n135299, n1))], (957 ^ _217006) ^ [] : [-(gt(n2, n1))], (959 ^ _217006) ^ [] : [-(gt(n3, n1))], (961 ^ _217006) ^ [] : [-(gt(n4, n2))], (963 ^ _217006) ^ [] : [-(gt(n5, n2))], (965 ^ _217006) ^ [] : [-(gt(n135299, n2))], (967 ^ _217006) ^ [] : [-(gt(n3, n2))], (969 ^ _217006) ^ [] : [-(gt(n4, n3))], (971 ^ _217006) ^ [] : [-(gt(n5, n3))], (973 ^ _217006) ^ [] : [-(gt(n135299, n3))], (975 ^ _217006) ^ [_255724] : [leq(n0, _255724), leq(_255724, n4), -(_255724 = n0), -(_255724 = n1), -(_255724 = n2), -(_255724 = n3), -(_255724 = n4)], (1001 ^ _217006) ^ [_256345] : [leq(n0, _256345), leq(_256345, n5), -(_256345 = n0), -(_256345 = n1), -(_256345 = n2), -(_256345 = n3), -(_256345 = n4), -(_256345 = n5)], (1031 ^ _217006) ^ [_257052] : [-(_257052 = n0), leq(n0, _257052), leq(_257052, n0)], (1041 ^ _217006) ^ [_257327] : [leq(n0, _257327), leq(_257327, n1), -(_257327 = n0), -(_257327 = n1)], (1055 ^ _217006) ^ [_257690] : [leq(n0, _257690), leq(_257690, n2), -(_257690 = n0), -(_257690 = n1), -(_257690 = n2)], (1095 ^ _217006) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (1097 ^ _217006) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (1099 ^ _217006) ^ [] : [-(succ(n0) = n1)], (1101 ^ _217006) ^ [] : [-(succ(succ(n0)) = n2)], (1103 ^ _217006) ^ [] : [-(succ(succ(succ(n0))) = n3)], (1073 ^ _217006) ^ [_258139] : [leq(n0, _258139), leq(_258139, n3), -(_258139 = n0), -(_258139 = n1), -(_258139 = n2), -(_258139 = n3)], (314 ^ _217006) ^ [_228315, _228317] : [-(gt(_228317, _228315)), -(gt(_228315, _228317)), -(_228317 = _228315)], (324 ^ _217006) ^ [_228630, _228632, _228634] : [-(gt(_228634, _228630)), gt(_228634, _228632), gt(_228632, _228630)], (334 ^ _217006) ^ [_228909] : [gt(_228909, _228909)], (336 ^ _217006) ^ [_228987] : [-(leq(_228987, _228987))], (338 ^ _217006) ^ [_229108, _229110, _229112] : [-(leq(_229112, _229108)), leq(_229112, _229110), leq(_229110, _229108)], (348 ^ _217006) ^ [_229446, _229448] : [lt(_229448, _229446), -(gt(_229446, _229448))], (354 ^ _217006) ^ [_229608, _229610] : [gt(_229608, _229610), -(lt(_229610, _229608))], (360 ^ _217006) ^ [_229849, _229851] : [geq(_229851, _229849), -(leq(_229849, _229851))], (366 ^ _217006) ^ [_230011, _230013] : [leq(_230011, _230013), -(geq(_230013, _230011))], (372 ^ _217006) ^ [_230223, _230225] : [gt(_230223, _230225), -(leq(_230225, _230223))], (378 ^ _217006) ^ [_230433, _230435] : [-(gt(_230433, _230435)), leq(_230435, _230433), -(_230435 = _230433)], (388 ^ _217006) ^ [_230764, _230766] : [leq(_230766, pred(_230764)), -(gt(_230764, _230766))], (394 ^ _217006) ^ [_230930, _230932] : [gt(_230930, _230932), -(leq(_230932, pred(_230930)))], (400 ^ _217006) ^ [_231117] : [-(gt(succ(_231117), _231117))], (402 ^ _217006) ^ [_231226, _231228] : [leq(_231228, _231226), -(leq(_231228, succ(_231226)))], (408 ^ _217006) ^ [_231469, _231471] : [leq(_231471, _231469), -(gt(succ(_231469), _231471))], (414 ^ _217006) ^ [_231635, _231637] : [gt(succ(_231635), _231637), -(leq(_231637, _231635))], (420 ^ _217006) ^ [_231851, _231853] : [leq(n0, _231853), -(leq(uniform_int_rnd(_231851, _231853), _231853))], (426 ^ _217006) ^ [_232067, _232069] : [leq(n0, _232069), -(leq(n0, uniform_int_rnd(_232067, _232069)))], (432 ^ _217006) ^ [_232311, _232313, _232315, _232317] : [-(a_select2(tptp_const_array1(dim(_232315, _232313), _232311), _232317) = _232311), leq(_232315, _232317), leq(_232317, _232313)], (442 ^ _217006) ^ [_232718, _232720, _232722, _232724, _232726, _232728, _232730] : [-(a_select3(tptp_const_array2(dim(_232728, _232726), dim(_232722, _232720), _232718), _232730, _232724) = _232718), leq(_232728, _232730), leq(_232730, _232726), leq(_232722, _232724), leq(_232724, _232720)], (460 ^ _217006) ^ [_233313, _233315] : [463 ^ _217006 : [(464 ^ _217006) ^ [] : [-(leq(n0, 461 ^ [_233313, _233315]))], (466 ^ _217006) ^ [] : [-(leq(461 ^ [_233313, _233315], _233313))], (468 ^ _217006) ^ [] : [-(leq(n0, 462 ^ [_233313, _233315]))], (470 ^ _217006) ^ [] : [-(leq(462 ^ [_233313, _233315], _233313))], (472 ^ _217006) ^ [] : [a_select3(_233315, 461 ^ [_233313, _233315], 462 ^ [_233313, _233315]) = a_select3(_233315, 462 ^ [_233313, _233315], 461 ^ [_233313, _233315])]], 473 ^ _217006 : [(474 ^ _217006) ^ [_234070, _234072] : [-(a_select3(trans(_233315), _234072, _234070) = a_select3(trans(_233315), _234070, _234072)), leq(n0, _234072), leq(_234072, _233313), leq(n0, _234070), leq(_234070, _233313)]]], (492 ^ _217006) ^ [_234617, _234619] : [495 ^ _217006 : [(496 ^ _217006) ^ [] : [-(leq(n0, 493 ^ [_234617, _234619]))], (498 ^ _217006) ^ [] : [-(leq(493 ^ [_234617, _234619], _234617))], (500 ^ _217006) ^ [] : [-(leq(n0, 494 ^ [_234617, _234619]))], (502 ^ _217006) ^ [] : [-(leq(494 ^ [_234617, _234619], _234617))], (504 ^ _217006) ^ [] : [a_select3(_234619, 493 ^ [_234617, _234619], 494 ^ [_234617, _234619]) = a_select3(_234619, 494 ^ [_234617, _234619], 493 ^ [_234617, _234619])]], 505 ^ _217006 : [(506 ^ _217006) ^ [_235374, _235376] : [-(a_select3(inv(_234619), _235376, _235374) = a_select3(inv(_234619), _235374, _235376)), leq(n0, _235376), leq(_235376, _234617), leq(n0, _235374), leq(_235374, _234617)]]], (524 ^ _217006) ^ [_235921, _235923] : [527 ^ _217006 : [(528 ^ _217006) ^ [] : [-(leq(n0, 525 ^ [_235921, _235923]))], (530 ^ _217006) ^ [] : [-(leq(525 ^ [_235921, _235923], _235921))], (532 ^ _217006) ^ [] : [-(leq(n0, 526 ^ [_235921, _235923]))], (534 ^ _217006) ^ [] : [-(leq(526 ^ [_235921, _235923], _235921))], (536 ^ _217006) ^ [] : [a_select3(_235923, 525 ^ [_235921, _235923], 526 ^ [_235921, _235923]) = a_select3(_235923, 526 ^ [_235921, _235923], 525 ^ [_235921, _235923])]], 537 ^ _217006 : [(538 ^ _217006) ^ [_236734, _236736, _236738, _236740] : [-(a_select3(tptp_update3(_235923, _236736, _236736, _236734), _236740, _236738) = a_select3(tptp_update3(_235923, _236736, _236736, _236734), _236738, _236740)), leq(n0, _236740), leq(_236740, _235921), leq(n0, _236738), leq(_236738, _235921), leq(n0, _236736), leq(_236736, _235921)]]], (564 ^ _217006) ^ [_237553, _237555, _237557] : [569 ^ _217006 : [(570 ^ _217006) ^ [] : [-(leq(n0, 567 ^ [_237553, _237555, _237557]))], (572 ^ _217006) ^ [] : [-(leq(567 ^ [_237553, _237555, _237557], _237553))], (574 ^ _217006) ^ [] : [-(leq(n0, 568 ^ [_237553, _237555, _237557]))], (576 ^ _217006) ^ [] : [-(leq(568 ^ [_237553, _237555, _237557], _237553))], (578 ^ _217006) ^ [] : [a_select3(_237557, 567 ^ [_237553, _237555, _237557], 568 ^ [_237553, _237555, _237557]) = a_select3(_237557, 568 ^ [_237553, _237555, _237557], 567 ^ [_237553, _237555, _237557])]], 581 ^ _217006 : [(582 ^ _217006) ^ [] : [-(leq(n0, 579 ^ [_237553, _237555, _237557]))], (584 ^ _217006) ^ [] : [-(leq(579 ^ [_237553, _237555, _237557], _237553))], (586 ^ _217006) ^ [] : [-(leq(n0, 580 ^ [_237553, _237555, _237557]))], (588 ^ _217006) ^ [] : [-(leq(580 ^ [_237553, _237555, _237557], _237553))], (590 ^ _217006) ^ [] : [a_select3(_237555, 579 ^ [_237553, _237555, _237557], 580 ^ [_237553, _237555, _237557]) = a_select3(_237555, 580 ^ [_237553, _237555, _237557], 579 ^ [_237553, _237555, _237557])]], 591 ^ _217006 : [(592 ^ _217006) ^ [_239062, _239064] : [-(a_select3(tptp_madd(_237557, _237555), _239064, _239062) = a_select3(tptp_madd(_237557, _237555), _239062, _239064)), leq(n0, _239064), leq(_239064, _237553), leq(n0, _239062), leq(_239062, _237553)]]], (610 ^ _217006) ^ [_239648, _239650, _239652] : [615 ^ _217006 : [(616 ^ _217006) ^ [] : [-(leq(n0, 613 ^ [_239648, _239650, _239652]))], (618 ^ _217006) ^ [] : [-(leq(613 ^ [_239648, _239650, _239652], _239648))], (620 ^ _217006) ^ [] : [-(leq(n0, 614 ^ [_239648, _239650, _239652]))], (622 ^ _217006) ^ [] : [-(leq(614 ^ [_239648, _239650, _239652], _239648))], (624 ^ _217006) ^ [] : [a_select3(_239652, 613 ^ [_239648, _239650, _239652], 614 ^ [_239648, _239650, _239652]) = a_select3(_239652, 614 ^ [_239648, _239650, _239652], 613 ^ [_239648, _239650, _239652])]], 627 ^ _217006 : [(628 ^ _217006) ^ [] : [-(leq(n0, 625 ^ [_239648, _239650, _239652]))], (630 ^ _217006) ^ [] : [-(leq(625 ^ [_239648, _239650, _239652], _239648))], (632 ^ _217006) ^ [] : [-(leq(n0, 626 ^ [_239648, _239650, _239652]))], (634 ^ _217006) ^ [] : [-(leq(626 ^ [_239648, _239650, _239652], _239648))], (636 ^ _217006) ^ [] : [a_select3(_239650, 625 ^ [_239648, _239650, _239652], 626 ^ [_239648, _239650, _239652]) = a_select3(_239650, 626 ^ [_239648, _239650, _239652], 625 ^ [_239648, _239650, _239652])]], 637 ^ _217006 : [(638 ^ _217006) ^ [_241157, _241159] : [-(a_select3(tptp_msub(_239652, _239650), _241159, _241157) = a_select3(tptp_msub(_239652, _239650), _241157, _241159)), leq(n0, _241159), leq(_241159, _239648), leq(n0, _241157), leq(_241157, _239648)]]], (656 ^ _217006) ^ [_241743, _241745, _241747] : [659 ^ _217006 : [(660 ^ _217006) ^ [] : [-(leq(n0, 657 ^ [_241743, _241745, _241747]))], (662 ^ _217006) ^ [] : [-(leq(657 ^ [_241743, _241745, _241747], _241743))], (664 ^ _217006) ^ [] : [-(leq(n0, 658 ^ [_241743, _241745, _241747]))], (666 ^ _217006) ^ [] : [-(leq(658 ^ [_241743, _241745, _241747], _241743))], (668 ^ _217006) ^ [] : [a_select3(_241745, 657 ^ [_241743, _241745, _241747], 658 ^ [_241743, _241745, _241747]) = a_select3(_241745, 658 ^ [_241743, _241745, _241747], 657 ^ [_241743, _241745, _241747])]], 669 ^ _217006 : [(670 ^ _217006) ^ [_242556, _242558] : [-(a_select3(tptp_mmul(_241747, tptp_mmul(_241745, trans(_241747))), _242558, _242556) = a_select3(tptp_mmul(_241747, tptp_mmul(_241745, trans(_241747))), _242556, _242558)), leq(n0, _242558), leq(_242558, _241743), leq(n0, _242556), leq(_242556, _241743)]]], (688 ^ _217006) ^ [_243175, _243177, _243179, _243181] : [691 ^ _217006 : [(692 ^ _217006) ^ [] : [-(leq(n0, 689 ^ [_243175, _243177, _243179, _243181]))], (694 ^ _217006) ^ [] : [-(leq(689 ^ [_243175, _243177, _243179, _243181], _243175))], (696 ^ _217006) ^ [] : [-(leq(n0, 690 ^ [_243175, _243177, _243179, _243181]))], (698 ^ _217006) ^ [] : [-(leq(690 ^ [_243175, _243177, _243179, _243181], _243175))], (700 ^ _217006) ^ [] : [a_select3(_243179, 689 ^ [_243175, _243177, _243179, _243181], 690 ^ [_243175, _243177, _243179, _243181]) = a_select3(_243179, 690 ^ [_243175, _243177, _243179, _243181], 689 ^ [_243175, _243177, _243179, _243181])]], 701 ^ _217006 : [(702 ^ _217006) ^ [_244032, _244034] : [-(a_select3(tptp_mmul(_243181, tptp_mmul(_243179, trans(_243181))), _244034, _244032) = a_select3(tptp_mmul(_243181, tptp_mmul(_243179, trans(_243181))), _244032, _244034)), leq(n0, _244034), leq(_244034, _243177), leq(n0, _244032), leq(_244032, _243177)]]], (720 ^ _217006) ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741] : [725 ^ _217006 : [(726 ^ _217006) ^ [] : [-(leq(n0, 723 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741]))], (728 ^ _217006) ^ [] : [-(leq(723 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741], _244727))], (730 ^ _217006) ^ [] : [-(leq(n0, 724 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741]))], (732 ^ _217006) ^ [] : [-(leq(724 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741], _244727))], (734 ^ _217006) ^ [] : [a_select3(_244735, 723 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741], 724 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741]) = a_select3(_244735, 724 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741], 723 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741])]], 739 ^ _217006 : [(740 ^ _217006) ^ [] : [-(leq(n0, 737 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741]))], (742 ^ _217006) ^ [] : [-(leq(737 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741], _244729))], (744 ^ _217006) ^ [] : [-(leq(n0, 738 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741]))], (746 ^ _217006) ^ [] : [-(leq(738 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741], _244729))], (748 ^ _217006) ^ [] : [a_select3(_244741, 737 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741], 738 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741]) = a_select3(_244741, 738 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741], 737 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741])]], 751 ^ _217006 : [(752 ^ _217006) ^ [] : [-(leq(n0, 749 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741]))], (754 ^ _217006) ^ [] : [-(leq(749 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741], _244729))], (756 ^ _217006) ^ [] : [-(leq(n0, 750 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741]))], (758 ^ _217006) ^ [] : [-(leq(750 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741], _244729))], (760 ^ _217006) ^ [] : [a_select3(_244731, 749 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741], 750 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741]) = a_select3(_244731, 750 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741], 749 ^ [_244727, _244729, _244731, _244733, _244735, _244737, _244739, _244741])]], 761 ^ _217006 : [(762 ^ _217006) ^ [_247655, _247657] : [-(a_select3(tptp_madd(_244741, tptp_mmul(_244739, tptp_mmul(tptp_madd(tptp_mmul(_244737, tptp_mmul(_244735, trans(_244737))), tptp_mmul(_244733, tptp_mmul(_244731, trans(_244733)))), trans(_244739)))), _247657, _247655) = a_select3(tptp_madd(_244741, tptp_mmul(_244739, tptp_mmul(tptp_madd(tptp_mmul(_244737, tptp_mmul(_244735, trans(_244737))), tptp_mmul(_244733, tptp_mmul(_244731, trans(_244733)))), trans(_244739)))), _247655, _247657)), leq(n0, _247657), leq(_247657, _244729), leq(n0, _247655), leq(_247655, _244729)]]], (780 ^ _217006) ^ [_248408] : [-(sum(n0, tptp_minus_1, _248408) = n0)], (782 ^ _217006) ^ [_248490] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _248490))], (784 ^ _217006) ^ [] : [-(succ(tptp_minus_1) = n0)], (786 ^ _217006) ^ [_248625] : [-(plus(_248625, n1) = succ(_248625))], (788 ^ _217006) ^ [_248708] : [-(plus(n1, _248708) = succ(_248708))], (790 ^ _217006) ^ [_248791] : [-(plus(_248791, n2) = succ(succ(_248791)))], (792 ^ _217006) ^ [_248876] : [-(plus(n2, _248876) = succ(succ(_248876)))], (794 ^ _217006) ^ [_248961] : [-(plus(_248961, n3) = succ(succ(succ(_248961))))], (796 ^ _217006) ^ [_249048] : [-(plus(n3, _249048) = succ(succ(succ(_249048))))], (798 ^ _217006) ^ [_249135] : [-(plus(_249135, n4) = succ(succ(succ(succ(_249135)))))], (800 ^ _217006) ^ [_249224] : [-(plus(n4, _249224) = succ(succ(succ(succ(_249224)))))], (802 ^ _217006) ^ [_249313] : [-(plus(_249313, n5) = succ(succ(succ(succ(succ(_249313))))))], (804 ^ _217006) ^ [_249404] : [-(plus(n5, _249404) = succ(succ(succ(succ(succ(_249404))))))], (806 ^ _217006) ^ [_249495] : [-(minus(_249495, n1) = pred(_249495))], (808 ^ _217006) ^ [_249578] : [-(pred(succ(_249578)) = _249578)], (810 ^ _217006) ^ [_249660] : [-(succ(pred(_249660)) = _249660)], (812 ^ _217006) ^ [_249800, _249802] : [leq(succ(_249802), succ(_249800)), -(leq(_249802, _249800))], (818 ^ _217006) ^ [_249970, _249972] : [leq(_249972, _249970), -(leq(succ(_249972), succ(_249970)))], (824 ^ _217006) ^ [_250190, _250192] : [leq(succ(_250192), _250190), -(gt(_250190, _250192))], (830 ^ _217006) ^ [_250404, _250406] : [leq(minus(_250406, _250404), _250406), -(leq(n0, _250404))], (836 ^ _217006) ^ [_250633, _250635, _250637, _250639] : [-(a_select3(tptp_update3(_250639, _250637, _250635, _250633), _250637, _250635) = _250633)], (838 ^ _217006) ^ [_250825, _250827, _250829, _250831, _250833, _250835, _250837] : [-(a_select3(tptp_update3(_250829, _250837, _250835, _250825), _250833, _250831) = _250827), -(_250837 = _250833), _250835 = _250831, a_select3(_250829, _250833, _250831) = _250827], (852 ^ _217006) ^ [_251368, _251370, _251372, _251374, _251376, _251378] : [-(a_select3(tptp_update3(_251370, _251374, _251372, _251368), _251378, _251376) = _251368), 857 ^ _217006 : [(858 ^ _217006) ^ [] : [-(leq(n0, 855 ^ [_251368, _251370, _251372, _251374, _251376, _251378]))], (860 ^ _217006) ^ [] : [-(leq(n0, 856 ^ [_251368, _251370, _251372, _251374, _251376, _251378]))], (862 ^ _217006) ^ [] : [-(leq(855 ^ [_251368, _251370, _251372, _251374, _251376, _251378], _251374))], (864 ^ _217006) ^ [] : [-(leq(856 ^ [_251368, _251370, _251372, _251374, _251376, _251378], _251372))], (866 ^ _217006) ^ [] : [a_select3(_251370, 855 ^ [_251368, _251370, _251372, _251374, _251376, _251378], 856 ^ [_251368, _251370, _251372, _251374, _251376, _251378]) = _251368]], leq(n0, _251378), leq(_251378, _251374), leq(n0, _251376), leq(_251376, _251372)], (884 ^ _217006) ^ [_252710, _252712, _252714] : [-(a_select2(tptp_update2(_252714, _252712, _252710), _252712) = _252710)], (886 ^ _217006) ^ [_252870, _252872, _252874, _252876, _252878] : [-(a_select2(tptp_update2(_252874, _252878, _252870), _252876) = _252872), -(_252878 = _252876), a_select2(_252874, _252876) = _252872], (915 ^ _217006) ^ [] : [-(true)], (917 ^ _217006) ^ [] : [def = use], (896 ^ _217006) ^ [_253250, _253252, _253254, _253256] : [-(a_select2(tptp_update2(_253252, _253254, _253250), _253256) = _253250), 900 ^ _217006 : [(901 ^ _217006) ^ [] : [-(leq(n0, 899 ^ [_253250, _253252, _253254, _253256]))], (903 ^ _217006) ^ [] : [-(leq(899 ^ [_253250, _253252, _253254, _253256], _253254))], (905 ^ _217006) ^ [] : [a_select2(_253252, 899 ^ [_253250, _253252, _253254, _253256]) = _253250]], leq(n0, _253256), leq(_253256, _253254)]], input).
% 8.96/9.71 ncf('1',plain,[gt(pv10, pv10)],start(334 ^ 0,bind([[_228909], [pv10]]))).
% 8.96/9.71 ncf('1.1',plain,[-(gt(pv10, pv10)), -(gt(pv10, pv10)), -(pv10 = pv10)],extension(314 ^ 1,bind([[_228315, _228317], [pv10, pv10]]))).
% 8.96/9.71 ncf('1.1.1',plain,[gt(pv10, pv10)],reduction('1')).
% 8.96/9.71 ncf('1.1.2',plain,[pv10 = pv10, -(pred(pv10) = pred(pv10))],extension(210 ^ 2,bind([[_224430, _224432], [pv10, pv10]]))).
% 8.96/9.71 ncf('1.1.2.1',plain,[pred(pv10) = pred(pv10), -(leq(pv10, pred(pv10))), leq(1134 ^ [], pred(pv10)), 1134 ^ [] = pv10],extension(62 ^ 3,bind([[_219114, _219116, _219118, _219120], [pred(pv10), pred(pv10), pv10, 1134 ^ []]]))).
% 8.96/9.71 ncf('1.1.2.1.1',plain,[leq(pv10, pred(pv10)), -(gt(pv10, pv10))],extension(388 ^ 4,bind([[_230764, _230766], [pv10, pv10]]))).
% 8.96/9.71 ncf('1.1.2.1.1.1',plain,[gt(pv10, pv10)],reduction('1')).
% 8.96/9.71 ncf('1.1.2.1.2',plain,[-(leq(1134 ^ [], pred(pv10)))],extension(1138 ^ 4)).
% 8.96/9.71 ncf('1.1.2.1.3',plain,[-(1134 ^ [] = pv10), pv10 = 1134 ^ []],extension(4 ^ 4,bind([[_217257, _217259], [1134 ^ [], pv10]]))).
% 8.96/9.71 ncf('1.1.2.1.3.1',plain,[-(pv10 = 1134 ^ [])],extension(1140 ^ 5)).
% 8.96/9.71 %-----------------------------------------------------
% 8.96/9.71 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------