%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV171+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n008.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:06 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.03/0.12 % Problem : SWV171+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.35 % Computer : n008.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8042.1875MB
% 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Fri May 19 02:47:39 EDT 2023
% 0.12/0.35 % CPUTime :
% 0.34/1.40
% 0.34/1.40 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.34/1.40 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.34/1.40 %-----------------------------------------------------
% 0.34/1.40 ncf(matrix, plain, [(1167 ^ _209653) ^ [] : [a_select2(sigma_init, pv52) = init], (1055 ^ _209653) ^ [] : [-(leq(n0, pv10))], (1057 ^ _209653) ^ [] : [-(leq(n0, pv52))], (1059 ^ _209653) ^ [] : [-(leq(n0, pv54))], (1061 ^ _209653) ^ [] : [-(leq(pv10, n135299))], (1063 ^ _209653) ^ [] : [-(leq(pv52, n4))], (1065 ^ _209653) ^ [] : [-(leq(pv54, n4))], (1067 ^ _209653) ^ [_250287] : [leq(n0, _250287), leq(_250287, n135299), 1074 ^ _209653 : [(1075 ^ _209653) ^ [_250515] : [-(a_select3(q_init, _250287, _250515) = init), leq(n0, _250515), leq(_250515, n4)]]], (1085 ^ _209653) ^ [_250817] : [-(a_select2(rho_init, _250817) = init), leq(n0, _250817), leq(_250817, n4)], (1095 ^ _209653) ^ [_251098] : [-(a_select2(mu_init, _251098) = init), leq(n0, _251098), leq(_251098, n4)], (1105 ^ _209653) ^ [_251379] : [-(a_select2(sigma_init, _251379) = init), leq(n0, _251379), leq(_251379, n4)], (1115 ^ _209653) ^ [_251660] : [-(a_select3(center_init, _251660, n0) = init), leq(n0, _251660), leq(_251660, n4)], (1125 ^ _209653) ^ [] : [gt(loopcounter, n1), 1128 ^ _209653 : [(1129 ^ _209653) ^ [_252005] : [-(a_select2(muold_init, _252005) = init), leq(n0, _252005), leq(_252005, n4)]]], (1139 ^ _209653) ^ [] : [gt(loopcounter, n1), 1142 ^ _209653 : [(1143 ^ _209653) ^ [_252353] : [-(a_select2(rhoold_init, _252353) = init), leq(n0, _252353), leq(_252353, n4)]]], (1153 ^ _209653) ^ [] : [gt(loopcounter, n1), 1156 ^ _209653 : [(1157 ^ _209653) ^ [_252681] : [-(a_select2(sigmaold_init, _252681) = init), leq(n0, _252681), leq(_252681, n4)]]], (2 ^ _209653) ^ [_209797] : [-(_209797 = _209797)], (4 ^ _209653) ^ [_209904, _209906] : [_209906 = _209904, -(_209904 = _209906)], (10 ^ _209653) ^ [_210108, _210110, _210112] : [-(_210112 = _210108), _210112 = _210110, _210110 = _210108], (20 ^ _209653) ^ [_210449, _210451, _210453, _210455] : [-(lt(_210453, _210449)), lt(_210455, _210451), _210455 = _210453, _210451 = _210449], (34 ^ _209653) ^ [_210893, _210895, _210897, _210899] : [-(geq(_210897, _210893)), geq(_210899, _210895), _210899 = _210897, _210895 = _210893], (48 ^ _209653) ^ [_211337, _211339, _211341, _211343] : [-(gt(_211341, _211337)), gt(_211343, _211339), _211343 = _211341, _211339 = _211337], (62 ^ _209653) ^ [_211761, _211763, _211765, _211767] : [-(leq(_211765, _211761)), leq(_211767, _211763), _211767 = _211765, _211763 = _211761], (76 ^ _209653) ^ [_212217, _212219, _212221, _212223] : [-(uniform_int_rnd(_212223, _212219) = uniform_int_rnd(_212221, _212217)), _212223 = _212221, _212219 = _212217], (86 ^ _209653) ^ [_212576, _212578, _212580, _212582] : [-(tptp_const_array1(_212582, _212578) = tptp_const_array1(_212580, _212576)), _212582 = _212580, _212578 = _212576], (96 ^ _209653) ^ [_212963, _212965, _212967, _212969, _212971, _212973] : [-(tptp_const_array2(_212973, _212969, _212965) = tptp_const_array2(_212971, _212967, _212963)), _212973 = _212971, _212969 = _212967, _212965 = _212963], (110 ^ _209653) ^ [_213451, _213453, _213455, _213457] : [-(dim(_213457, _213453) = dim(_213455, _213451)), _213457 = _213455, _213453 = _213451], (120 ^ _209653) ^ [_213782, _213784] : [_213784 = _213782, -(inv(_213784) = inv(_213782))], (126 ^ _209653) ^ [_214028, _214030, _214032, _214034] : [-(tptp_msub(_214034, _214030) = tptp_msub(_214032, _214028)), _214034 = _214032, _214030 = _214028], (136 ^ _209653) ^ [_214387, _214389, _214391, _214393] : [-(tptp_madd(_214393, _214389) = tptp_madd(_214391, _214387)), _214393 = _214391, _214389 = _214387], (146 ^ _209653) ^ [_214746, _214748, _214750, _214752] : [-(tptp_mmul(_214752, _214748) = tptp_mmul(_214750, _214746)), _214752 = _214750, _214748 = _214746], (156 ^ _209653) ^ [_215077, _215079] : [_215079 = _215077, -(trans(_215079) = trans(_215077))], (162 ^ _209653) ^ [_215351, _215353, _215355, _215357, _215359, _215361] : [-(sum(_215361, _215357, _215353) = sum(_215359, _215355, _215351)), _215361 = _215359, _215357 = _215355, _215353 = _215351], (176 ^ _209653) ^ [_215839, _215841, _215843, _215845] : [-(plus(_215845, _215841) = plus(_215843, _215839)), _215845 = _215843, _215841 = _215839], (186 ^ _209653) ^ [_216170, _216172] : [_216172 = _216170, -(pred(_216172) = pred(_216170))], (192 ^ _209653) ^ [_216416, _216418, _216420, _216422] : [-(minus(_216422, _216418) = minus(_216420, _216416)), _216422 = _216420, _216418 = _216416], (202 ^ _209653) ^ [_216831, _216833, _216835, _216837, _216839, _216841, _216843, _216845] : [-(tptp_update3(_216845, _216841, _216837, _216833) = tptp_update3(_216843, _216839, _216835, _216831)), _216845 = _216843, _216841 = _216839, _216837 = _216835, _216833 = _216831], (220 ^ _209653) ^ [_217492, _217494, _217496, _217498, _217500, _217502] : [-(tptp_update2(_217502, _217498, _217494) = tptp_update2(_217500, _217496, _217492)), _217502 = _217500, _217498 = _217496, _217494 = _217492], (234 ^ _209653) ^ [_217952, _217954] : [_217954 = _217952, -(succ(_217954) = succ(_217952))], (254 ^ _209653) ^ [_218694, _218696, _218698, _218700] : [-(a_select2(_218700, _218696) = a_select2(_218698, _218694)), _218700 = _218698, _218696 = _218694], (240 ^ _209653) ^ [_218226, _218228, _218230, _218232, _218234, _218236] : [-(a_select3(_218236, _218232, _218228) = a_select3(_218234, _218230, _218226)), _218236 = _218234, _218232 = _218230, _218228 = _218226], (869 ^ _209653) ^ [] : [-(gt(n5, n4))], (871 ^ _209653) ^ [] : [-(gt(n135299, n4))], (873 ^ _209653) ^ [] : [-(gt(n135299, n5))], (875 ^ _209653) ^ [] : [-(gt(n4, tptp_minus_1))], (877 ^ _209653) ^ [] : [-(gt(n5, tptp_minus_1))], (879 ^ _209653) ^ [] : [-(gt(n135299, tptp_minus_1))], (881 ^ _209653) ^ [] : [-(gt(n0, tptp_minus_1))], (883 ^ _209653) ^ [] : [-(gt(n1, tptp_minus_1))], (885 ^ _209653) ^ [] : [-(gt(n2, tptp_minus_1))], (887 ^ _209653) ^ [] : [-(gt(n3, tptp_minus_1))], (889 ^ _209653) ^ [] : [-(gt(n4, n0))], (891 ^ _209653) ^ [] : [-(gt(n5, n0))], (893 ^ _209653) ^ [] : [-(gt(n135299, n0))], (895 ^ _209653) ^ [] : [-(gt(n1, n0))], (897 ^ _209653) ^ [] : [-(gt(n2, n0))], (899 ^ _209653) ^ [] : [-(gt(n3, n0))], (901 ^ _209653) ^ [] : [-(gt(n4, n1))], (903 ^ _209653) ^ [] : [-(gt(n5, n1))], (905 ^ _209653) ^ [] : [-(gt(n135299, n1))], (907 ^ _209653) ^ [] : [-(gt(n2, n1))], (909 ^ _209653) ^ [] : [-(gt(n3, n1))], (911 ^ _209653) ^ [] : [-(gt(n4, n2))], (913 ^ _209653) ^ [] : [-(gt(n5, n2))], (915 ^ _209653) ^ [] : [-(gt(n135299, n2))], (917 ^ _209653) ^ [] : [-(gt(n3, n2))], (919 ^ _209653) ^ [] : [-(gt(n4, n3))], (921 ^ _209653) ^ [] : [-(gt(n5, n3))], (923 ^ _209653) ^ [] : [-(gt(n135299, n3))], (925 ^ _209653) ^ [_246534] : [leq(n0, _246534), leq(_246534, n4), -(_246534 = n0), -(_246534 = n1), -(_246534 = n2), -(_246534 = n3), -(_246534 = n4)], (951 ^ _209653) ^ [_247155] : [leq(n0, _247155), leq(_247155, n5), -(_247155 = n0), -(_247155 = n1), -(_247155 = n2), -(_247155 = n3), -(_247155 = n4), -(_247155 = n5)], (981 ^ _209653) ^ [_247862] : [-(_247862 = n0), leq(n0, _247862), leq(_247862, n0)], (991 ^ _209653) ^ [_248137] : [leq(n0, _248137), leq(_248137, n1), -(_248137 = n0), -(_248137 = n1)], (1005 ^ _209653) ^ [_248500] : [leq(n0, _248500), leq(_248500, n2), -(_248500 = n0), -(_248500 = n1), -(_248500 = n2)], (1045 ^ _209653) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (1047 ^ _209653) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (1049 ^ _209653) ^ [] : [-(succ(n0) = n1)], (1051 ^ _209653) ^ [] : [-(succ(succ(n0)) = n2)], (1053 ^ _209653) ^ [] : [-(succ(succ(succ(n0))) = n3)], (1023 ^ _209653) ^ [_248949] : [leq(n0, _248949), leq(_248949, n3), -(_248949 = n0), -(_248949 = n1), -(_248949 = n2), -(_248949 = n3)], (264 ^ _209653) ^ [_219125, _219127] : [-(gt(_219127, _219125)), -(gt(_219125, _219127)), -(_219127 = _219125)], (274 ^ _209653) ^ [_219440, _219442, _219444] : [-(gt(_219444, _219440)), gt(_219444, _219442), gt(_219442, _219440)], (284 ^ _209653) ^ [_219719] : [gt(_219719, _219719)], (286 ^ _209653) ^ [_219797] : [-(leq(_219797, _219797))], (288 ^ _209653) ^ [_219918, _219920, _219922] : [-(leq(_219922, _219918)), leq(_219922, _219920), leq(_219920, _219918)], (298 ^ _209653) ^ [_220256, _220258] : [lt(_220258, _220256), -(gt(_220256, _220258))], (304 ^ _209653) ^ [_220418, _220420] : [gt(_220418, _220420), -(lt(_220420, _220418))], (310 ^ _209653) ^ [_220659, _220661] : [geq(_220661, _220659), -(leq(_220659, _220661))], (316 ^ _209653) ^ [_220821, _220823] : [leq(_220821, _220823), -(geq(_220823, _220821))], (322 ^ _209653) ^ [_221033, _221035] : [gt(_221033, _221035), -(leq(_221035, _221033))], (328 ^ _209653) ^ [_221243, _221245] : [-(gt(_221243, _221245)), leq(_221245, _221243), -(_221245 = _221243)], (338 ^ _209653) ^ [_221574, _221576] : [leq(_221576, pred(_221574)), -(gt(_221574, _221576))], (344 ^ _209653) ^ [_221740, _221742] : [gt(_221740, _221742), -(leq(_221742, pred(_221740)))], (350 ^ _209653) ^ [_221927] : [-(gt(succ(_221927), _221927))], (352 ^ _209653) ^ [_222036, _222038] : [leq(_222038, _222036), -(leq(_222038, succ(_222036)))], (358 ^ _209653) ^ [_222279, _222281] : [leq(_222281, _222279), -(gt(succ(_222279), _222281))], (364 ^ _209653) ^ [_222445, _222447] : [gt(succ(_222445), _222447), -(leq(_222447, _222445))], (370 ^ _209653) ^ [_222661, _222663] : [leq(n0, _222663), -(leq(uniform_int_rnd(_222661, _222663), _222663))], (376 ^ _209653) ^ [_222877, _222879] : [leq(n0, _222879), -(leq(n0, uniform_int_rnd(_222877, _222879)))], (382 ^ _209653) ^ [_223121, _223123, _223125, _223127] : [-(a_select2(tptp_const_array1(dim(_223125, _223123), _223121), _223127) = _223121), leq(_223125, _223127), leq(_223127, _223123)], (392 ^ _209653) ^ [_223528, _223530, _223532, _223534, _223536, _223538, _223540] : [-(a_select3(tptp_const_array2(dim(_223538, _223536), dim(_223532, _223530), _223528), _223540, _223534) = _223528), leq(_223538, _223540), leq(_223540, _223536), leq(_223532, _223534), leq(_223534, _223530)], (410 ^ _209653) ^ [_224123, _224125] : [413 ^ _209653 : [(414 ^ _209653) ^ [] : [-(leq(n0, 411 ^ [_224123, _224125]))], (416 ^ _209653) ^ [] : [-(leq(411 ^ [_224123, _224125], _224123))], (418 ^ _209653) ^ [] : [-(leq(n0, 412 ^ [_224123, _224125]))], (420 ^ _209653) ^ [] : [-(leq(412 ^ [_224123, _224125], _224123))], (422 ^ _209653) ^ [] : [a_select3(_224125, 411 ^ [_224123, _224125], 412 ^ [_224123, _224125]) = a_select3(_224125, 412 ^ [_224123, _224125], 411 ^ [_224123, _224125])]], 423 ^ _209653 : [(424 ^ _209653) ^ [_224880, _224882] : [-(a_select3(trans(_224125), _224882, _224880) = a_select3(trans(_224125), _224880, _224882)), leq(n0, _224882), leq(_224882, _224123), leq(n0, _224880), leq(_224880, _224123)]]], (442 ^ _209653) ^ [_225427, _225429] : [445 ^ _209653 : [(446 ^ _209653) ^ [] : [-(leq(n0, 443 ^ [_225427, _225429]))], (448 ^ _209653) ^ [] : [-(leq(443 ^ [_225427, _225429], _225427))], (450 ^ _209653) ^ [] : [-(leq(n0, 444 ^ [_225427, _225429]))], (452 ^ _209653) ^ [] : [-(leq(444 ^ [_225427, _225429], _225427))], (454 ^ _209653) ^ [] : [a_select3(_225429, 443 ^ [_225427, _225429], 444 ^ [_225427, _225429]) = a_select3(_225429, 444 ^ [_225427, _225429], 443 ^ [_225427, _225429])]], 455 ^ _209653 : [(456 ^ _209653) ^ [_226184, _226186] : [-(a_select3(inv(_225429), _226186, _226184) = a_select3(inv(_225429), _226184, _226186)), leq(n0, _226186), leq(_226186, _225427), leq(n0, _226184), leq(_226184, _225427)]]], (474 ^ _209653) ^ [_226731, _226733] : [477 ^ _209653 : [(478 ^ _209653) ^ [] : [-(leq(n0, 475 ^ [_226731, _226733]))], (480 ^ _209653) ^ [] : [-(leq(475 ^ [_226731, _226733], _226731))], (482 ^ _209653) ^ [] : [-(leq(n0, 476 ^ [_226731, _226733]))], (484 ^ _209653) ^ [] : [-(leq(476 ^ [_226731, _226733], _226731))], (486 ^ _209653) ^ [] : [a_select3(_226733, 475 ^ [_226731, _226733], 476 ^ [_226731, _226733]) = a_select3(_226733, 476 ^ [_226731, _226733], 475 ^ [_226731, _226733])]], 487 ^ _209653 : [(488 ^ _209653) ^ [_227544, _227546, _227548, _227550] : [-(a_select3(tptp_update3(_226733, _227546, _227546, _227544), _227550, _227548) = a_select3(tptp_update3(_226733, _227546, _227546, _227544), _227548, _227550)), leq(n0, _227550), leq(_227550, _226731), leq(n0, _227548), leq(_227548, _226731), leq(n0, _227546), leq(_227546, _226731)]]], (514 ^ _209653) ^ [_228363, _228365, _228367] : [519 ^ _209653 : [(520 ^ _209653) ^ [] : [-(leq(n0, 517 ^ [_228363, _228365, _228367]))], (522 ^ _209653) ^ [] : [-(leq(517 ^ [_228363, _228365, _228367], _228363))], (524 ^ _209653) ^ [] : [-(leq(n0, 518 ^ [_228363, _228365, _228367]))], (526 ^ _209653) ^ [] : [-(leq(518 ^ [_228363, _228365, _228367], _228363))], (528 ^ _209653) ^ [] : [a_select3(_228367, 517 ^ [_228363, _228365, _228367], 518 ^ [_228363, _228365, _228367]) = a_select3(_228367, 518 ^ [_228363, _228365, _228367], 517 ^ [_228363, _228365, _228367])]], 531 ^ _209653 : [(532 ^ _209653) ^ [] : [-(leq(n0, 529 ^ [_228363, _228365, _228367]))], (534 ^ _209653) ^ [] : [-(leq(529 ^ [_228363, _228365, _228367], _228363))], (536 ^ _209653) ^ [] : [-(leq(n0, 530 ^ [_228363, _228365, _228367]))], (538 ^ _209653) ^ [] : [-(leq(530 ^ [_228363, _228365, _228367], _228363))], (540 ^ _209653) ^ [] : [a_select3(_228365, 529 ^ [_228363, _228365, _228367], 530 ^ [_228363, _228365, _228367]) = a_select3(_228365, 530 ^ [_228363, _228365, _228367], 529 ^ [_228363, _228365, _228367])]], 541 ^ _209653 : [(542 ^ _209653) ^ [_229872, _229874] : [-(a_select3(tptp_madd(_228367, _228365), _229874, _229872) = a_select3(tptp_madd(_228367, _228365), _229872, _229874)), leq(n0, _229874), leq(_229874, _228363), leq(n0, _229872), leq(_229872, _228363)]]], (560 ^ _209653) ^ [_230458, _230460, _230462] : [565 ^ _209653 : [(566 ^ _209653) ^ [] : [-(leq(n0, 563 ^ [_230458, _230460, _230462]))], (568 ^ _209653) ^ [] : [-(leq(563 ^ [_230458, _230460, _230462], _230458))], (570 ^ _209653) ^ [] : [-(leq(n0, 564 ^ [_230458, _230460, _230462]))], (572 ^ _209653) ^ [] : [-(leq(564 ^ [_230458, _230460, _230462], _230458))], (574 ^ _209653) ^ [] : [a_select3(_230462, 563 ^ [_230458, _230460, _230462], 564 ^ [_230458, _230460, _230462]) = a_select3(_230462, 564 ^ [_230458, _230460, _230462], 563 ^ [_230458, _230460, _230462])]], 577 ^ _209653 : [(578 ^ _209653) ^ [] : [-(leq(n0, 575 ^ [_230458, _230460, _230462]))], (580 ^ _209653) ^ [] : [-(leq(575 ^ [_230458, _230460, _230462], _230458))], (582 ^ _209653) ^ [] : [-(leq(n0, 576 ^ [_230458, _230460, _230462]))], (584 ^ _209653) ^ [] : [-(leq(576 ^ [_230458, _230460, _230462], _230458))], (586 ^ _209653) ^ [] : [a_select3(_230460, 575 ^ [_230458, _230460, _230462], 576 ^ [_230458, _230460, _230462]) = a_select3(_230460, 576 ^ [_230458, _230460, _230462], 575 ^ [_230458, _230460, _230462])]], 587 ^ _209653 : [(588 ^ _209653) ^ [_231967, _231969] : [-(a_select3(tptp_msub(_230462, _230460), _231969, _231967) = a_select3(tptp_msub(_230462, _230460), _231967, _231969)), leq(n0, _231969), leq(_231969, _230458), leq(n0, _231967), leq(_231967, _230458)]]], (606 ^ _209653) ^ [_232553, _232555, _232557] : [609 ^ _209653 : [(610 ^ _209653) ^ [] : [-(leq(n0, 607 ^ [_232553, _232555, _232557]))], (612 ^ _209653) ^ [] : [-(leq(607 ^ [_232553, _232555, _232557], _232553))], (614 ^ _209653) ^ [] : [-(leq(n0, 608 ^ [_232553, _232555, _232557]))], (616 ^ _209653) ^ [] : [-(leq(608 ^ [_232553, _232555, _232557], _232553))], (618 ^ _209653) ^ [] : [a_select3(_232555, 607 ^ [_232553, _232555, _232557], 608 ^ [_232553, _232555, _232557]) = a_select3(_232555, 608 ^ [_232553, _232555, _232557], 607 ^ [_232553, _232555, _232557])]], 619 ^ _209653 : [(620 ^ _209653) ^ [_233366, _233368] : [-(a_select3(tptp_mmul(_232557, tptp_mmul(_232555, trans(_232557))), _233368, _233366) = a_select3(tptp_mmul(_232557, tptp_mmul(_232555, trans(_232557))), _233366, _233368)), leq(n0, _233368), leq(_233368, _232553), leq(n0, _233366), leq(_233366, _232553)]]], (638 ^ _209653) ^ [_233985, _233987, _233989, _233991] : [641 ^ _209653 : [(642 ^ _209653) ^ [] : [-(leq(n0, 639 ^ [_233985, _233987, _233989, _233991]))], (644 ^ _209653) ^ [] : [-(leq(639 ^ [_233985, _233987, _233989, _233991], _233985))], (646 ^ _209653) ^ [] : [-(leq(n0, 640 ^ [_233985, _233987, _233989, _233991]))], (648 ^ _209653) ^ [] : [-(leq(640 ^ [_233985, _233987, _233989, _233991], _233985))], (650 ^ _209653) ^ [] : [a_select3(_233989, 639 ^ [_233985, _233987, _233989, _233991], 640 ^ [_233985, _233987, _233989, _233991]) = a_select3(_233989, 640 ^ [_233985, _233987, _233989, _233991], 639 ^ [_233985, _233987, _233989, _233991])]], 651 ^ _209653 : [(652 ^ _209653) ^ [_234842, _234844] : [-(a_select3(tptp_mmul(_233991, tptp_mmul(_233989, trans(_233991))), _234844, _234842) = a_select3(tptp_mmul(_233991, tptp_mmul(_233989, trans(_233991))), _234842, _234844)), leq(n0, _234844), leq(_234844, _233987), leq(n0, _234842), leq(_234842, _233987)]]], (670 ^ _209653) ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551] : [675 ^ _209653 : [(676 ^ _209653) ^ [] : [-(leq(n0, 673 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551]))], (678 ^ _209653) ^ [] : [-(leq(673 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551], _235537))], (680 ^ _209653) ^ [] : [-(leq(n0, 674 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551]))], (682 ^ _209653) ^ [] : [-(leq(674 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551], _235537))], (684 ^ _209653) ^ [] : [a_select3(_235545, 673 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551], 674 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551]) = a_select3(_235545, 674 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551], 673 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551])]], 689 ^ _209653 : [(690 ^ _209653) ^ [] : [-(leq(n0, 687 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551]))], (692 ^ _209653) ^ [] : [-(leq(687 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551], _235539))], (694 ^ _209653) ^ [] : [-(leq(n0, 688 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551]))], (696 ^ _209653) ^ [] : [-(leq(688 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551], _235539))], (698 ^ _209653) ^ [] : [a_select3(_235551, 687 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551], 688 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551]) = a_select3(_235551, 688 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551], 687 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551])]], 701 ^ _209653 : [(702 ^ _209653) ^ [] : [-(leq(n0, 699 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551]))], (704 ^ _209653) ^ [] : [-(leq(699 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551], _235539))], (706 ^ _209653) ^ [] : [-(leq(n0, 700 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551]))], (708 ^ _209653) ^ [] : [-(leq(700 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551], _235539))], (710 ^ _209653) ^ [] : [a_select3(_235541, 699 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551], 700 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551]) = a_select3(_235541, 700 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551], 699 ^ [_235537, _235539, _235541, _235543, _235545, _235547, _235549, _235551])]], 711 ^ _209653 : [(712 ^ _209653) ^ [_238465, _238467] : [-(a_select3(tptp_madd(_235551, tptp_mmul(_235549, tptp_mmul(tptp_madd(tptp_mmul(_235547, tptp_mmul(_235545, trans(_235547))), tptp_mmul(_235543, tptp_mmul(_235541, trans(_235543)))), trans(_235549)))), _238467, _238465) = a_select3(tptp_madd(_235551, tptp_mmul(_235549, tptp_mmul(tptp_madd(tptp_mmul(_235547, tptp_mmul(_235545, trans(_235547))), tptp_mmul(_235543, tptp_mmul(_235541, trans(_235543)))), trans(_235549)))), _238465, _238467)), leq(n0, _238467), leq(_238467, _235539), leq(n0, _238465), leq(_238465, _235539)]]], (730 ^ _209653) ^ [_239218] : [-(sum(n0, tptp_minus_1, _239218) = n0)], (732 ^ _209653) ^ [_239300] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _239300))], (734 ^ _209653) ^ [] : [-(succ(tptp_minus_1) = n0)], (736 ^ _209653) ^ [_239435] : [-(plus(_239435, n1) = succ(_239435))], (738 ^ _209653) ^ [_239518] : [-(plus(n1, _239518) = succ(_239518))], (740 ^ _209653) ^ [_239601] : [-(plus(_239601, n2) = succ(succ(_239601)))], (742 ^ _209653) ^ [_239686] : [-(plus(n2, _239686) = succ(succ(_239686)))], (744 ^ _209653) ^ [_239771] : [-(plus(_239771, n3) = succ(succ(succ(_239771))))], (746 ^ _209653) ^ [_239858] : [-(plus(n3, _239858) = succ(succ(succ(_239858))))], (748 ^ _209653) ^ [_239945] : [-(plus(_239945, n4) = succ(succ(succ(succ(_239945)))))], (750 ^ _209653) ^ [_240034] : [-(plus(n4, _240034) = succ(succ(succ(succ(_240034)))))], (752 ^ _209653) ^ [_240123] : [-(plus(_240123, n5) = succ(succ(succ(succ(succ(_240123))))))], (754 ^ _209653) ^ [_240214] : [-(plus(n5, _240214) = succ(succ(succ(succ(succ(_240214))))))], (756 ^ _209653) ^ [_240305] : [-(minus(_240305, n1) = pred(_240305))], (758 ^ _209653) ^ [_240388] : [-(pred(succ(_240388)) = _240388)], (760 ^ _209653) ^ [_240470] : [-(succ(pred(_240470)) = _240470)], (762 ^ _209653) ^ [_240610, _240612] : [leq(succ(_240612), succ(_240610)), -(leq(_240612, _240610))], (768 ^ _209653) ^ [_240780, _240782] : [leq(_240782, _240780), -(leq(succ(_240782), succ(_240780)))], (774 ^ _209653) ^ [_241000, _241002] : [leq(succ(_241002), _241000), -(gt(_241000, _241002))], (780 ^ _209653) ^ [_241214, _241216] : [leq(minus(_241216, _241214), _241216), -(leq(n0, _241214))], (786 ^ _209653) ^ [_241443, _241445, _241447, _241449] : [-(a_select3(tptp_update3(_241449, _241447, _241445, _241443), _241447, _241445) = _241443)], (788 ^ _209653) ^ [_241635, _241637, _241639, _241641, _241643, _241645, _241647] : [-(a_select3(tptp_update3(_241639, _241647, _241645, _241635), _241643, _241641) = _241637), -(_241647 = _241643), _241645 = _241641, a_select3(_241639, _241643, _241641) = _241637], (802 ^ _209653) ^ [_242178, _242180, _242182, _242184, _242186, _242188] : [-(a_select3(tptp_update3(_242180, _242184, _242182, _242178), _242188, _242186) = _242178), 807 ^ _209653 : [(808 ^ _209653) ^ [] : [-(leq(n0, 805 ^ [_242178, _242180, _242182, _242184, _242186, _242188]))], (810 ^ _209653) ^ [] : [-(leq(n0, 806 ^ [_242178, _242180, _242182, _242184, _242186, _242188]))], (812 ^ _209653) ^ [] : [-(leq(805 ^ [_242178, _242180, _242182, _242184, _242186, _242188], _242184))], (814 ^ _209653) ^ [] : [-(leq(806 ^ [_242178, _242180, _242182, _242184, _242186, _242188], _242182))], (816 ^ _209653) ^ [] : [a_select3(_242180, 805 ^ [_242178, _242180, _242182, _242184, _242186, _242188], 806 ^ [_242178, _242180, _242182, _242184, _242186, _242188]) = _242178]], leq(n0, _242188), leq(_242188, _242184), leq(n0, _242186), leq(_242186, _242182)], (834 ^ _209653) ^ [_243520, _243522, _243524] : [-(a_select2(tptp_update2(_243524, _243522, _243520), _243522) = _243520)], (836 ^ _209653) ^ [_243680, _243682, _243684, _243686, _243688] : [-(a_select2(tptp_update2(_243684, _243688, _243680), _243686) = _243682), -(_243688 = _243686), a_select2(_243684, _243686) = _243682], (865 ^ _209653) ^ [] : [-(true)], (867 ^ _209653) ^ [] : [def = use], (846 ^ _209653) ^ [_244060, _244062, _244064, _244066] : [-(a_select2(tptp_update2(_244062, _244064, _244060), _244066) = _244060), 850 ^ _209653 : [(851 ^ _209653) ^ [] : [-(leq(n0, 849 ^ [_244060, _244062, _244064, _244066]))], (853 ^ _209653) ^ [] : [-(leq(849 ^ [_244060, _244062, _244064, _244066], _244064))], (855 ^ _209653) ^ [] : [a_select2(_244062, 849 ^ [_244060, _244062, _244064, _244066]) = _244060]], leq(n0, _244066), leq(_244066, _244064)]], input).
% 0.34/1.40 ncf('1',plain,[a_select2(sigma_init, pv52) = init],start(1167 ^ 0)).
% 0.34/1.40 ncf('1.1',plain,[-(a_select2(sigma_init, pv52) = init), leq(n0, pv52), leq(pv52, n4)],extension(1105 ^ 1,bind([[_251379], [pv52]]))).
% 0.34/1.40 ncf('1.1.1',plain,[-(leq(n0, pv52))],extension(1057 ^ 2)).
% 0.34/1.40 ncf('1.1.2',plain,[-(leq(pv52, n4))],extension(1063 ^ 2)).
% 0.34/1.40 %-----------------------------------------------------
% 0.34/1.40 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------