%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV160+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n032.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri May 19 12:20:05 EDT 2023
% Result : Theorem 8.91s 9.59s
% Output : Proof 8.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.09 % Problem : SWV160+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.05/0.10 % Command : nanocop.sh %s %d
% 0.08/0.28 % Computer : n032.cluster.edu
% 0.08/0.28 % Model : x86_64 x86_64
% 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.28 % Memory : 8042.1875MB
% 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.28 % CPULimit : 300
% 0.08/0.28 % WCLimit : 300
% 0.08/0.28 % DateTime : Fri May 19 02:31:35 EDT 2023
% 0.08/0.28 % CPUTime :
% 8.91/9.59
% 8.91/9.59 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 8.91/9.59 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.91/9.59 %-----------------------------------------------------
% 8.91/9.59 ncf(matrix, plain, [(1158 ^ _224715) ^ [] : [-(leq(n0, 1156 ^ []))], (1160 ^ _224715) ^ [] : [-(leq(1156 ^ [], pred(pv10)))], (1162 ^ _224715) ^ [] : [-(pv10 = 1156 ^ [])], (1164 ^ _224715) ^ [] : [sum(n0, n4, cond(tptp_term_equals(pv47, tptp_sum_index), divide(divide(times(exp(divide(divide(times(minus(a_select2(x, pv10), a_select2(mu, pv47)), minus(a_select2(x, pv10), a_select2(mu, pv47))), tptp_minus_2), times(a_select2(sigma, pv47), a_select2(sigma, pv47)))), a_select2(rho, pv47)), times(sqrt(times(n2, tptp_pi)), a_select2(sigma, pv47))), pv84), a_select3(q, 1156 ^ [], tptp_sum_index))) = n1], (1127 ^ _224715) ^ [] : [-(pv84 = sum(n0, n4, divide(times(exp(divide(divide(times(minus(a_select2(x, pv10), a_select2(mu, tptp_sum_index)), minus(a_select2(x, pv10), a_select2(mu, tptp_sum_index))), tptp_minus_2), times(a_select2(sigma, tptp_sum_index), a_select2(sigma, tptp_sum_index)))), a_select2(rho, tptp_sum_index)), times(sqrt(times(n2, tptp_pi)), a_select2(sigma, tptp_sum_index)))))], (1129 ^ _224715) ^ [] : [-(leq(n0, pv10))], (1131 ^ _224715) ^ [] : [-(leq(n0, pv47))], (1133 ^ _224715) ^ [] : [-(leq(pv10, n135299))], (1135 ^ _224715) ^ [] : [-(leq(pv47, n4))], (1137 ^ _224715) ^ [_267821] : [-(a_select3(q, pv10, _267821) = divide(divide(times(exp(divide(divide(times(minus(a_select2(x, pv10), a_select2(mu, _267821)), minus(a_select2(x, pv10), a_select2(mu, _267821))), tptp_minus_2), times(a_select2(sigma, _267821), a_select2(sigma, _267821)))), a_select2(rho, _267821)), times(sqrt(times(n2, tptp_pi)), a_select2(sigma, _267821))), sum(n0, n4, divide(times(exp(divide(divide(times(minus(a_select2(x, pv10), a_select2(mu, tptp_sum_index)), minus(a_select2(x, pv10), a_select2(mu, tptp_sum_index))), tptp_minus_2), times(a_select2(sigma, tptp_sum_index), a_select2(sigma, tptp_sum_index)))), a_select2(rho, tptp_sum_index)), times(sqrt(times(n2, tptp_pi)), a_select2(sigma, tptp_sum_index)))))), leq(n0, _267821), leq(_267821, pred(pv47))], (1147 ^ _224715) ^ [_268184] : [-(sum(n0, n4, a_select3(q, _268184, tptp_sum_index)) = n1), leq(n0, _268184), leq(_268184, pred(pv10))], (2 ^ _224715) ^ [_224859] : [-(_224859 = _224859)], (4 ^ _224715) ^ [_224966, _224968] : [_224968 = _224966, -(_224966 = _224968)], (10 ^ _224715) ^ [_225170, _225172, _225174] : [-(_225174 = _225170), _225174 = _225172, _225172 = _225170], (20 ^ _224715) ^ [_225511, _225513, _225515, _225517] : [-(lt(_225515, _225511)), lt(_225517, _225513), _225517 = _225515, _225513 = _225511], (34 ^ _224715) ^ [_225955, _225957, _225959, _225961] : [-(geq(_225959, _225955)), geq(_225961, _225957), _225961 = _225959, _225957 = _225955], (48 ^ _224715) ^ [_226399, _226401, _226403, _226405] : [-(gt(_226403, _226399)), gt(_226405, _226401), _226405 = _226403, _226401 = _226399], (62 ^ _224715) ^ [_226823, _226825, _226827, _226829] : [-(leq(_226827, _226823)), leq(_226829, _226825), _226829 = _226827, _226825 = _226823], (76 ^ _224715) ^ [_227279, _227281, _227283, _227285] : [-(uniform_int_rnd(_227285, _227281) = uniform_int_rnd(_227283, _227279)), _227285 = _227283, _227281 = _227279], (86 ^ _224715) ^ [_227638, _227640, _227642, _227644] : [-(tptp_const_array1(_227644, _227640) = tptp_const_array1(_227642, _227638)), _227644 = _227642, _227640 = _227638], (96 ^ _224715) ^ [_228025, _228027, _228029, _228031, _228033, _228035] : [-(tptp_const_array2(_228035, _228031, _228027) = tptp_const_array2(_228033, _228029, _228025)), _228035 = _228033, _228031 = _228029, _228027 = _228025], (110 ^ _224715) ^ [_228513, _228515, _228517, _228519] : [-(dim(_228519, _228515) = dim(_228517, _228513)), _228519 = _228517, _228515 = _228513], (120 ^ _224715) ^ [_228844, _228846] : [_228846 = _228844, -(inv(_228846) = inv(_228844))], (126 ^ _224715) ^ [_229090, _229092, _229094, _229096] : [-(tptp_msub(_229096, _229092) = tptp_msub(_229094, _229090)), _229096 = _229094, _229092 = _229090], (136 ^ _224715) ^ [_229449, _229451, _229453, _229455] : [-(tptp_madd(_229455, _229451) = tptp_madd(_229453, _229449)), _229455 = _229453, _229451 = _229449], (146 ^ _224715) ^ [_229808, _229810, _229812, _229814] : [-(tptp_mmul(_229814, _229810) = tptp_mmul(_229812, _229808)), _229814 = _229812, _229810 = _229808], (156 ^ _224715) ^ [_230139, _230141] : [_230141 = _230139, -(trans(_230141) = trans(_230139))], (162 ^ _224715) ^ [_230385, _230387, _230389, _230391] : [-(plus(_230391, _230387) = plus(_230389, _230385)), _230391 = _230389, _230387 = _230385], (172 ^ _224715) ^ [_230800, _230802, _230804, _230806, _230808, _230810, _230812, _230814] : [-(tptp_update3(_230814, _230810, _230806, _230802) = tptp_update3(_230812, _230808, _230804, _230800)), _230814 = _230812, _230810 = _230808, _230806 = _230804, _230802 = _230800], (190 ^ _224715) ^ [_231461, _231463, _231465, _231467, _231469, _231471] : [-(tptp_update2(_231471, _231467, _231463) = tptp_update2(_231469, _231465, _231461)), _231471 = _231469, _231467 = _231465, _231463 = _231461], (204 ^ _224715) ^ [_231921, _231923] : [_231923 = _231921, -(succ(_231923) = succ(_231921))], (210 ^ _224715) ^ [_232139, _232141] : [_232141 = _232139, -(pred(_232141) = pred(_232139))], (216 ^ _224715) ^ [_232413, _232415, _232417, _232419, _232421, _232423] : [-(sum(_232423, _232419, _232415) = sum(_232421, _232417, _232413)), _232423 = _232421, _232419 = _232417, _232415 = _232413], (230 ^ _224715) ^ [_232929, _232931, _232933, _232935, _232937, _232939] : [-(cond(_232939, _232935, _232931) = cond(_232937, _232933, _232929)), _232939 = _232937, _232935 = _232933, _232931 = _232929], (244 ^ _224715) ^ [_233417, _233419, _233421, _233423] : [-(tptp_term_equals(_233423, _233419) = tptp_term_equals(_233421, _233417)), _233423 = _233421, _233419 = _233417], (254 ^ _224715) ^ [_233748, _233750] : [_233750 = _233748, -(exp(_233750) = exp(_233748))], (260 ^ _224715) ^ [_233994, _233996, _233998, _234000] : [-(divide(_234000, _233996) = divide(_233998, _233994)), _234000 = _233998, _233996 = _233994], (270 ^ _224715) ^ [_234353, _234355, _234357, _234359] : [-(minus(_234359, _234355) = minus(_234357, _234353)), _234359 = _234357, _234355 = _234353], (280 ^ _224715) ^ [_234684, _234686] : [_234686 = _234684, -(sqrt(_234686) = sqrt(_234684))], (286 ^ _224715) ^ [_234930, _234932, _234934, _234936] : [-(times(_234936, _234932) = times(_234934, _234930)), _234936 = _234934, _234932 = _234930], (296 ^ _224715) ^ [_235289, _235291, _235293, _235295] : [-(a_select2(_235295, _235291) = a_select2(_235293, _235289)), _235295 = _235293, _235291 = _235289], (306 ^ _224715) ^ [_235656, _235658, _235660, _235662, _235664, _235666] : [-(a_select3(_235666, _235662, _235658) = a_select3(_235664, _235660, _235656)), _235666 = _235664, _235662 = _235660, _235658 = _235656], (925 ^ _224715) ^ [] : [-(gt(n5, n4))], (927 ^ _224715) ^ [] : [-(gt(n135299, n4))], (929 ^ _224715) ^ [] : [-(gt(n135299, n5))], (931 ^ _224715) ^ [] : [-(gt(n4, tptp_minus_1))], (933 ^ _224715) ^ [] : [-(gt(n5, tptp_minus_1))], (935 ^ _224715) ^ [] : [-(gt(n135299, tptp_minus_1))], (937 ^ _224715) ^ [] : [-(gt(n0, tptp_minus_1))], (939 ^ _224715) ^ [] : [-(gt(n1, tptp_minus_1))], (941 ^ _224715) ^ [] : [-(gt(n2, tptp_minus_1))], (943 ^ _224715) ^ [] : [-(gt(n3, tptp_minus_1))], (945 ^ _224715) ^ [] : [-(gt(n4, tptp_minus_2))], (947 ^ _224715) ^ [] : [-(gt(n5, tptp_minus_2))], (949 ^ _224715) ^ [] : [-(gt(tptp_minus_1, tptp_minus_2))], (951 ^ _224715) ^ [] : [-(gt(n135299, tptp_minus_2))], (953 ^ _224715) ^ [] : [-(gt(n0, tptp_minus_2))], (955 ^ _224715) ^ [] : [-(gt(n1, tptp_minus_2))], (957 ^ _224715) ^ [] : [-(gt(n2, tptp_minus_2))], (959 ^ _224715) ^ [] : [-(gt(n3, tptp_minus_2))], (961 ^ _224715) ^ [] : [-(gt(n4, n0))], (963 ^ _224715) ^ [] : [-(gt(n5, n0))], (965 ^ _224715) ^ [] : [-(gt(n135299, n0))], (967 ^ _224715) ^ [] : [-(gt(n1, n0))], (969 ^ _224715) ^ [] : [-(gt(n2, n0))], (971 ^ _224715) ^ [] : [-(gt(n3, n0))], (973 ^ _224715) ^ [] : [-(gt(n4, n1))], (975 ^ _224715) ^ [] : [-(gt(n5, n1))], (977 ^ _224715) ^ [] : [-(gt(n135299, n1))], (979 ^ _224715) ^ [] : [-(gt(n2, n1))], (981 ^ _224715) ^ [] : [-(gt(n3, n1))], (983 ^ _224715) ^ [] : [-(gt(n4, n2))], (985 ^ _224715) ^ [] : [-(gt(n5, n2))], (987 ^ _224715) ^ [] : [-(gt(n135299, n2))], (989 ^ _224715) ^ [] : [-(gt(n3, n2))], (991 ^ _224715) ^ [] : [-(gt(n4, n3))], (993 ^ _224715) ^ [] : [-(gt(n5, n3))], (995 ^ _224715) ^ [] : [-(gt(n135299, n3))], (997 ^ _224715) ^ [_264077] : [leq(n0, _264077), leq(_264077, n4), -(_264077 = n0), -(_264077 = n1), -(_264077 = n2), -(_264077 = n3), -(_264077 = n4)], (1023 ^ _224715) ^ [_264698] : [leq(n0, _264698), leq(_264698, n5), -(_264698 = n0), -(_264698 = n1), -(_264698 = n2), -(_264698 = n3), -(_264698 = n4), -(_264698 = n5)], (1053 ^ _224715) ^ [_265405] : [-(_265405 = n0), leq(n0, _265405), leq(_265405, n0)], (1063 ^ _224715) ^ [_265680] : [leq(n0, _265680), leq(_265680, n1), -(_265680 = n0), -(_265680 = n1)], (1077 ^ _224715) ^ [_266043] : [leq(n0, _266043), leq(_266043, n2), -(_266043 = n0), -(_266043 = n1), -(_266043 = n2)], (1117 ^ _224715) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (1119 ^ _224715) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (1121 ^ _224715) ^ [] : [-(succ(n0) = n1)], (1123 ^ _224715) ^ [] : [-(succ(succ(n0)) = n2)], (1125 ^ _224715) ^ [] : [-(succ(succ(succ(n0))) = n3)], (1095 ^ _224715) ^ [_266492] : [leq(n0, _266492), leq(_266492, n3), -(_266492 = n0), -(_266492 = n1), -(_266492 = n2), -(_266492 = n3)], (320 ^ _224715) ^ [_236244, _236246] : [-(gt(_236246, _236244)), -(gt(_236244, _236246)), -(_236246 = _236244)], (330 ^ _224715) ^ [_236559, _236561, _236563] : [-(gt(_236563, _236559)), gt(_236563, _236561), gt(_236561, _236559)], (340 ^ _224715) ^ [_236838] : [gt(_236838, _236838)], (342 ^ _224715) ^ [_236916] : [-(leq(_236916, _236916))], (344 ^ _224715) ^ [_237037, _237039, _237041] : [-(leq(_237041, _237037)), leq(_237041, _237039), leq(_237039, _237037)], (354 ^ _224715) ^ [_237375, _237377] : [lt(_237377, _237375), -(gt(_237375, _237377))], (360 ^ _224715) ^ [_237537, _237539] : [gt(_237537, _237539), -(lt(_237539, _237537))], (366 ^ _224715) ^ [_237778, _237780] : [geq(_237780, _237778), -(leq(_237778, _237780))], (372 ^ _224715) ^ [_237940, _237942] : [leq(_237940, _237942), -(geq(_237942, _237940))], (378 ^ _224715) ^ [_238152, _238154] : [gt(_238152, _238154), -(leq(_238154, _238152))], (384 ^ _224715) ^ [_238362, _238364] : [-(gt(_238362, _238364)), leq(_238364, _238362), -(_238364 = _238362)], (394 ^ _224715) ^ [_238693, _238695] : [leq(_238695, pred(_238693)), -(gt(_238693, _238695))], (400 ^ _224715) ^ [_238859, _238861] : [gt(_238859, _238861), -(leq(_238861, pred(_238859)))], (406 ^ _224715) ^ [_239046] : [-(gt(succ(_239046), _239046))], (408 ^ _224715) ^ [_239155, _239157] : [leq(_239157, _239155), -(leq(_239157, succ(_239155)))], (414 ^ _224715) ^ [_239398, _239400] : [leq(_239400, _239398), -(gt(succ(_239398), _239400))], (420 ^ _224715) ^ [_239564, _239566] : [gt(succ(_239564), _239566), -(leq(_239566, _239564))], (426 ^ _224715) ^ [_239780, _239782] : [leq(n0, _239782), -(leq(uniform_int_rnd(_239780, _239782), _239782))], (432 ^ _224715) ^ [_239996, _239998] : [leq(n0, _239998), -(leq(n0, uniform_int_rnd(_239996, _239998)))], (438 ^ _224715) ^ [_240240, _240242, _240244, _240246] : [-(a_select2(tptp_const_array1(dim(_240244, _240242), _240240), _240246) = _240240), leq(_240244, _240246), leq(_240246, _240242)], (448 ^ _224715) ^ [_240647, _240649, _240651, _240653, _240655, _240657, _240659] : [-(a_select3(tptp_const_array2(dim(_240657, _240655), dim(_240651, _240649), _240647), _240659, _240653) = _240647), leq(_240657, _240659), leq(_240659, _240655), leq(_240651, _240653), leq(_240653, _240649)], (466 ^ _224715) ^ [_241242, _241244] : [469 ^ _224715 : [(470 ^ _224715) ^ [] : [-(leq(n0, 467 ^ [_241242, _241244]))], (472 ^ _224715) ^ [] : [-(leq(467 ^ [_241242, _241244], _241242))], (474 ^ _224715) ^ [] : [-(leq(n0, 468 ^ [_241242, _241244]))], (476 ^ _224715) ^ [] : [-(leq(468 ^ [_241242, _241244], _241242))], (478 ^ _224715) ^ [] : [a_select3(_241244, 467 ^ [_241242, _241244], 468 ^ [_241242, _241244]) = a_select3(_241244, 468 ^ [_241242, _241244], 467 ^ [_241242, _241244])]], 479 ^ _224715 : [(480 ^ _224715) ^ [_241999, _242001] : [-(a_select3(trans(_241244), _242001, _241999) = a_select3(trans(_241244), _241999, _242001)), leq(n0, _242001), leq(_242001, _241242), leq(n0, _241999), leq(_241999, _241242)]]], (498 ^ _224715) ^ [_242546, _242548] : [501 ^ _224715 : [(502 ^ _224715) ^ [] : [-(leq(n0, 499 ^ [_242546, _242548]))], (504 ^ _224715) ^ [] : [-(leq(499 ^ [_242546, _242548], _242546))], (506 ^ _224715) ^ [] : [-(leq(n0, 500 ^ [_242546, _242548]))], (508 ^ _224715) ^ [] : [-(leq(500 ^ [_242546, _242548], _242546))], (510 ^ _224715) ^ [] : [a_select3(_242548, 499 ^ [_242546, _242548], 500 ^ [_242546, _242548]) = a_select3(_242548, 500 ^ [_242546, _242548], 499 ^ [_242546, _242548])]], 511 ^ _224715 : [(512 ^ _224715) ^ [_243303, _243305] : [-(a_select3(inv(_242548), _243305, _243303) = a_select3(inv(_242548), _243303, _243305)), leq(n0, _243305), leq(_243305, _242546), leq(n0, _243303), leq(_243303, _242546)]]], (530 ^ _224715) ^ [_243850, _243852] : [533 ^ _224715 : [(534 ^ _224715) ^ [] : [-(leq(n0, 531 ^ [_243850, _243852]))], (536 ^ _224715) ^ [] : [-(leq(531 ^ [_243850, _243852], _243850))], (538 ^ _224715) ^ [] : [-(leq(n0, 532 ^ [_243850, _243852]))], (540 ^ _224715) ^ [] : [-(leq(532 ^ [_243850, _243852], _243850))], (542 ^ _224715) ^ [] : [a_select3(_243852, 531 ^ [_243850, _243852], 532 ^ [_243850, _243852]) = a_select3(_243852, 532 ^ [_243850, _243852], 531 ^ [_243850, _243852])]], 543 ^ _224715 : [(544 ^ _224715) ^ [_244663, _244665, _244667, _244669] : [-(a_select3(tptp_update3(_243852, _244665, _244665, _244663), _244669, _244667) = a_select3(tptp_update3(_243852, _244665, _244665, _244663), _244667, _244669)), leq(n0, _244669), leq(_244669, _243850), leq(n0, _244667), leq(_244667, _243850), leq(n0, _244665), leq(_244665, _243850)]]], (570 ^ _224715) ^ [_245482, _245484, _245486] : [575 ^ _224715 : [(576 ^ _224715) ^ [] : [-(leq(n0, 573 ^ [_245482, _245484, _245486]))], (578 ^ _224715) ^ [] : [-(leq(573 ^ [_245482, _245484, _245486], _245482))], (580 ^ _224715) ^ [] : [-(leq(n0, 574 ^ [_245482, _245484, _245486]))], (582 ^ _224715) ^ [] : [-(leq(574 ^ [_245482, _245484, _245486], _245482))], (584 ^ _224715) ^ [] : [a_select3(_245486, 573 ^ [_245482, _245484, _245486], 574 ^ [_245482, _245484, _245486]) = a_select3(_245486, 574 ^ [_245482, _245484, _245486], 573 ^ [_245482, _245484, _245486])]], 587 ^ _224715 : [(588 ^ _224715) ^ [] : [-(leq(n0, 585 ^ [_245482, _245484, _245486]))], (590 ^ _224715) ^ [] : [-(leq(585 ^ [_245482, _245484, _245486], _245482))], (592 ^ _224715) ^ [] : [-(leq(n0, 586 ^ [_245482, _245484, _245486]))], (594 ^ _224715) ^ [] : [-(leq(586 ^ [_245482, _245484, _245486], _245482))], (596 ^ _224715) ^ [] : [a_select3(_245484, 585 ^ [_245482, _245484, _245486], 586 ^ [_245482, _245484, _245486]) = a_select3(_245484, 586 ^ [_245482, _245484, _245486], 585 ^ [_245482, _245484, _245486])]], 597 ^ _224715 : [(598 ^ _224715) ^ [_246991, _246993] : [-(a_select3(tptp_madd(_245486, _245484), _246993, _246991) = a_select3(tptp_madd(_245486, _245484), _246991, _246993)), leq(n0, _246993), leq(_246993, _245482), leq(n0, _246991), leq(_246991, _245482)]]], (616 ^ _224715) ^ [_247577, _247579, _247581] : [621 ^ _224715 : [(622 ^ _224715) ^ [] : [-(leq(n0, 619 ^ [_247577, _247579, _247581]))], (624 ^ _224715) ^ [] : [-(leq(619 ^ [_247577, _247579, _247581], _247577))], (626 ^ _224715) ^ [] : [-(leq(n0, 620 ^ [_247577, _247579, _247581]))], (628 ^ _224715) ^ [] : [-(leq(620 ^ [_247577, _247579, _247581], _247577))], (630 ^ _224715) ^ [] : [a_select3(_247581, 619 ^ [_247577, _247579, _247581], 620 ^ [_247577, _247579, _247581]) = a_select3(_247581, 620 ^ [_247577, _247579, _247581], 619 ^ [_247577, _247579, _247581])]], 633 ^ _224715 : [(634 ^ _224715) ^ [] : [-(leq(n0, 631 ^ [_247577, _247579, _247581]))], (636 ^ _224715) ^ [] : [-(leq(631 ^ [_247577, _247579, _247581], _247577))], (638 ^ _224715) ^ [] : [-(leq(n0, 632 ^ [_247577, _247579, _247581]))], (640 ^ _224715) ^ [] : [-(leq(632 ^ [_247577, _247579, _247581], _247577))], (642 ^ _224715) ^ [] : [a_select3(_247579, 631 ^ [_247577, _247579, _247581], 632 ^ [_247577, _247579, _247581]) = a_select3(_247579, 632 ^ [_247577, _247579, _247581], 631 ^ [_247577, _247579, _247581])]], 643 ^ _224715 : [(644 ^ _224715) ^ [_249086, _249088] : [-(a_select3(tptp_msub(_247581, _247579), _249088, _249086) = a_select3(tptp_msub(_247581, _247579), _249086, _249088)), leq(n0, _249088), leq(_249088, _247577), leq(n0, _249086), leq(_249086, _247577)]]], (662 ^ _224715) ^ [_249672, _249674, _249676] : [665 ^ _224715 : [(666 ^ _224715) ^ [] : [-(leq(n0, 663 ^ [_249672, _249674, _249676]))], (668 ^ _224715) ^ [] : [-(leq(663 ^ [_249672, _249674, _249676], _249672))], (670 ^ _224715) ^ [] : [-(leq(n0, 664 ^ [_249672, _249674, _249676]))], (672 ^ _224715) ^ [] : [-(leq(664 ^ [_249672, _249674, _249676], _249672))], (674 ^ _224715) ^ [] : [a_select3(_249674, 663 ^ [_249672, _249674, _249676], 664 ^ [_249672, _249674, _249676]) = a_select3(_249674, 664 ^ [_249672, _249674, _249676], 663 ^ [_249672, _249674, _249676])]], 675 ^ _224715 : [(676 ^ _224715) ^ [_250485, _250487] : [-(a_select3(tptp_mmul(_249676, tptp_mmul(_249674, trans(_249676))), _250487, _250485) = a_select3(tptp_mmul(_249676, tptp_mmul(_249674, trans(_249676))), _250485, _250487)), leq(n0, _250487), leq(_250487, _249672), leq(n0, _250485), leq(_250485, _249672)]]], (694 ^ _224715) ^ [_251104, _251106, _251108, _251110] : [697 ^ _224715 : [(698 ^ _224715) ^ [] : [-(leq(n0, 695 ^ [_251104, _251106, _251108, _251110]))], (700 ^ _224715) ^ [] : [-(leq(695 ^ [_251104, _251106, _251108, _251110], _251104))], (702 ^ _224715) ^ [] : [-(leq(n0, 696 ^ [_251104, _251106, _251108, _251110]))], (704 ^ _224715) ^ [] : [-(leq(696 ^ [_251104, _251106, _251108, _251110], _251104))], (706 ^ _224715) ^ [] : [a_select3(_251108, 695 ^ [_251104, _251106, _251108, _251110], 696 ^ [_251104, _251106, _251108, _251110]) = a_select3(_251108, 696 ^ [_251104, _251106, _251108, _251110], 695 ^ [_251104, _251106, _251108, _251110])]], 707 ^ _224715 : [(708 ^ _224715) ^ [_251961, _251963] : [-(a_select3(tptp_mmul(_251110, tptp_mmul(_251108, trans(_251110))), _251963, _251961) = a_select3(tptp_mmul(_251110, tptp_mmul(_251108, trans(_251110))), _251961, _251963)), leq(n0, _251963), leq(_251963, _251106), leq(n0, _251961), leq(_251961, _251106)]]], (726 ^ _224715) ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670] : [731 ^ _224715 : [(732 ^ _224715) ^ [] : [-(leq(n0, 729 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670]))], (734 ^ _224715) ^ [] : [-(leq(729 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670], _252656))], (736 ^ _224715) ^ [] : [-(leq(n0, 730 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670]))], (738 ^ _224715) ^ [] : [-(leq(730 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670], _252656))], (740 ^ _224715) ^ [] : [a_select3(_252664, 729 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670], 730 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670]) = a_select3(_252664, 730 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670], 729 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670])]], 745 ^ _224715 : [(746 ^ _224715) ^ [] : [-(leq(n0, 743 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670]))], (748 ^ _224715) ^ [] : [-(leq(743 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670], _252658))], (750 ^ _224715) ^ [] : [-(leq(n0, 744 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670]))], (752 ^ _224715) ^ [] : [-(leq(744 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670], _252658))], (754 ^ _224715) ^ [] : [a_select3(_252670, 743 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670], 744 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670]) = a_select3(_252670, 744 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670], 743 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670])]], 757 ^ _224715 : [(758 ^ _224715) ^ [] : [-(leq(n0, 755 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670]))], (760 ^ _224715) ^ [] : [-(leq(755 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670], _252658))], (762 ^ _224715) ^ [] : [-(leq(n0, 756 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670]))], (764 ^ _224715) ^ [] : [-(leq(756 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670], _252658))], (766 ^ _224715) ^ [] : [a_select3(_252660, 755 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670], 756 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670]) = a_select3(_252660, 756 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670], 755 ^ [_252656, _252658, _252660, _252662, _252664, _252666, _252668, _252670])]], 767 ^ _224715 : [(768 ^ _224715) ^ [_255584, _255586] : [-(a_select3(tptp_madd(_252670, tptp_mmul(_252668, tptp_mmul(tptp_madd(tptp_mmul(_252666, tptp_mmul(_252664, trans(_252666))), tptp_mmul(_252662, tptp_mmul(_252660, trans(_252662)))), trans(_252668)))), _255586, _255584) = a_select3(tptp_madd(_252670, tptp_mmul(_252668, tptp_mmul(tptp_madd(tptp_mmul(_252666, tptp_mmul(_252664, trans(_252666))), tptp_mmul(_252662, tptp_mmul(_252660, trans(_252662)))), trans(_252668)))), _255584, _255586)), leq(n0, _255586), leq(_255586, _252658), leq(n0, _255584), leq(_255584, _252658)]]], (786 ^ _224715) ^ [_256337] : [-(sum(n0, tptp_minus_1, _256337) = n0)], (788 ^ _224715) ^ [_256419] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _256419))], (790 ^ _224715) ^ [] : [-(succ(tptp_minus_1) = n0)], (792 ^ _224715) ^ [_256554] : [-(plus(_256554, n1) = succ(_256554))], (794 ^ _224715) ^ [_256637] : [-(plus(n1, _256637) = succ(_256637))], (796 ^ _224715) ^ [_256720] : [-(plus(_256720, n2) = succ(succ(_256720)))], (798 ^ _224715) ^ [_256805] : [-(plus(n2, _256805) = succ(succ(_256805)))], (800 ^ _224715) ^ [_256890] : [-(plus(_256890, n3) = succ(succ(succ(_256890))))], (802 ^ _224715) ^ [_256977] : [-(plus(n3, _256977) = succ(succ(succ(_256977))))], (804 ^ _224715) ^ [_257064] : [-(plus(_257064, n4) = succ(succ(succ(succ(_257064)))))], (806 ^ _224715) ^ [_257153] : [-(plus(n4, _257153) = succ(succ(succ(succ(_257153)))))], (808 ^ _224715) ^ [_257242] : [-(plus(_257242, n5) = succ(succ(succ(succ(succ(_257242))))))], (810 ^ _224715) ^ [_257333] : [-(plus(n5, _257333) = succ(succ(succ(succ(succ(_257333))))))], (812 ^ _224715) ^ [_257424] : [-(minus(_257424, n1) = pred(_257424))], (814 ^ _224715) ^ [_257507] : [-(pred(succ(_257507)) = _257507)], (816 ^ _224715) ^ [_257589] : [-(succ(pred(_257589)) = _257589)], (818 ^ _224715) ^ [_257729, _257731] : [leq(succ(_257731), succ(_257729)), -(leq(_257731, _257729))], (824 ^ _224715) ^ [_257899, _257901] : [leq(_257901, _257899), -(leq(succ(_257901), succ(_257899)))], (830 ^ _224715) ^ [_258119, _258121] : [leq(succ(_258121), _258119), -(gt(_258119, _258121))], (836 ^ _224715) ^ [_258333, _258335] : [leq(minus(_258335, _258333), _258335), -(leq(n0, _258333))], (842 ^ _224715) ^ [_258562, _258564, _258566, _258568] : [-(a_select3(tptp_update3(_258568, _258566, _258564, _258562), _258566, _258564) = _258562)], (844 ^ _224715) ^ [_258754, _258756, _258758, _258760, _258762, _258764, _258766] : [-(a_select3(tptp_update3(_258758, _258766, _258764, _258754), _258762, _258760) = _258756), -(_258766 = _258762), _258764 = _258760, a_select3(_258758, _258762, _258760) = _258756], (858 ^ _224715) ^ [_259297, _259299, _259301, _259303, _259305, _259307] : [-(a_select3(tptp_update3(_259299, _259303, _259301, _259297), _259307, _259305) = _259297), 863 ^ _224715 : [(864 ^ _224715) ^ [] : [-(leq(n0, 861 ^ [_259297, _259299, _259301, _259303, _259305, _259307]))], (866 ^ _224715) ^ [] : [-(leq(n0, 862 ^ [_259297, _259299, _259301, _259303, _259305, _259307]))], (868 ^ _224715) ^ [] : [-(leq(861 ^ [_259297, _259299, _259301, _259303, _259305, _259307], _259303))], (870 ^ _224715) ^ [] : [-(leq(862 ^ [_259297, _259299, _259301, _259303, _259305, _259307], _259301))], (872 ^ _224715) ^ [] : [a_select3(_259299, 861 ^ [_259297, _259299, _259301, _259303, _259305, _259307], 862 ^ [_259297, _259299, _259301, _259303, _259305, _259307]) = _259297]], leq(n0, _259307), leq(_259307, _259303), leq(n0, _259305), leq(_259305, _259301)], (890 ^ _224715) ^ [_260639, _260641, _260643] : [-(a_select2(tptp_update2(_260643, _260641, _260639), _260641) = _260639)], (892 ^ _224715) ^ [_260799, _260801, _260803, _260805, _260807] : [-(a_select2(tptp_update2(_260803, _260807, _260799), _260805) = _260801), -(_260807 = _260805), a_select2(_260803, _260805) = _260801], (921 ^ _224715) ^ [] : [-(true)], (923 ^ _224715) ^ [] : [def = use], (902 ^ _224715) ^ [_261179, _261181, _261183, _261185] : [-(a_select2(tptp_update2(_261181, _261183, _261179), _261185) = _261179), 906 ^ _224715 : [(907 ^ _224715) ^ [] : [-(leq(n0, 905 ^ [_261179, _261181, _261183, _261185]))], (909 ^ _224715) ^ [] : [-(leq(905 ^ [_261179, _261181, _261183, _261185], _261183))], (911 ^ _224715) ^ [] : [a_select2(_261181, 905 ^ [_261179, _261181, _261183, _261185]) = _261179]], leq(n0, _261185), leq(_261185, _261183)]], input).
% 8.91/9.59 ncf('1',plain,[gt(pv10, pv10)],start(340 ^ 0,bind([[_236838], [pv10]]))).
% 8.91/9.59 ncf('1.1',plain,[-(gt(pv10, pv10)), -(gt(pv10, pv10)), -(pv10 = pv10)],extension(320 ^ 1,bind([[_236244, _236246], [pv10, pv10]]))).
% 8.91/9.59 ncf('1.1.1',plain,[gt(pv10, pv10)],reduction('1')).
% 8.91/9.59 ncf('1.1.2',plain,[pv10 = pv10, -(pred(pv10) = pred(pv10))],extension(210 ^ 2,bind([[_232139, _232141], [pv10, pv10]]))).
% 8.91/9.59 ncf('1.1.2.1',plain,[pred(pv10) = pred(pv10), -(leq(pv10, pred(pv10))), leq(1156 ^ [], pred(pv10)), 1156 ^ [] = pv10],extension(62 ^ 3,bind([[_226823, _226825, _226827, _226829], [pred(pv10), pred(pv10), pv10, 1156 ^ []]]))).
% 8.91/9.59 ncf('1.1.2.1.1',plain,[leq(pv10, pred(pv10)), -(gt(pv10, pv10))],extension(394 ^ 4,bind([[_238693, _238695], [pv10, pv10]]))).
% 8.91/9.59 ncf('1.1.2.1.1.1',plain,[gt(pv10, pv10)],reduction('1')).
% 8.91/9.59 ncf('1.1.2.1.2',plain,[-(leq(1156 ^ [], pred(pv10)))],extension(1160 ^ 4)).
% 8.91/9.59 ncf('1.1.2.1.3',plain,[-(1156 ^ [] = pv10), pv10 = 1156 ^ []],extension(4 ^ 4,bind([[_224966, _224968], [1156 ^ [], pv10]]))).
% 8.91/9.59 ncf('1.1.2.1.3.1',plain,[-(pv10 = 1156 ^ [])],extension(1162 ^ 5)).
% 8.91/9.59 %-----------------------------------------------------
% 8.91/9.59 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------