%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV135+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:01 EDT 2023
% Result : Theorem 27.85s 27.37s
% Output : Proof 27.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : SWV135+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.04/0.14 % Command : nanocop.sh %s %d
% 0.14/0.36 % Computer : n004.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Fri May 19 02:08:39 EDT 2023
% 0.14/0.36 % CPUTime :
% 27.85/27.37
% 27.85/27.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 27.85/27.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.85/27.37 %-----------------------------------------------------
% 27.85/27.37 ncf(matrix, plain, [(1041 ^ _200464) ^ [] : [-(leq(n0, s_best7))], (1043 ^ _200464) ^ [] : [-(leq(n0, s_sworst7))], (1045 ^ _200464) ^ [] : [-(leq(n0, s_worst7))], (1047 ^ _200464) ^ [] : [-(leq(n2, pv1325))], (1049 ^ _200464) ^ [] : [-(leq(s_best7, n3))], (1051 ^ _200464) ^ [] : [-(leq(s_sworst7, n3))], (1053 ^ _200464) ^ [] : [-(leq(s_worst7, n3))], (1055 ^ _200464) ^ [] : [-(leq(pv1325, n3))], (1057 ^ _200464) ^ [] : [leq(n0, pv1325)], (2 ^ _200464) ^ [_200608] : [-(_200608 = _200608)], (4 ^ _200464) ^ [_200715, _200717] : [_200717 = _200715, -(_200715 = _200717)], (10 ^ _200464) ^ [_200919, _200921, _200923] : [-(_200923 = _200919), _200923 = _200921, _200921 = _200919], (20 ^ _200464) ^ [_201260, _201262, _201264, _201266] : [-(lt(_201264, _201260)), lt(_201266, _201262), _201266 = _201264, _201262 = _201260], (34 ^ _200464) ^ [_201704, _201706, _201708, _201710] : [-(geq(_201708, _201704)), geq(_201710, _201706), _201710 = _201708, _201706 = _201704], (48 ^ _200464) ^ [_202148, _202150, _202152, _202154] : [-(gt(_202152, _202148)), gt(_202154, _202150), _202154 = _202152, _202150 = _202148], (62 ^ _200464) ^ [_202572, _202574, _202576, _202578] : [-(leq(_202576, _202572)), leq(_202578, _202574), _202578 = _202576, _202574 = _202572], (76 ^ _200464) ^ [_203028, _203030, _203032, _203034] : [-(uniform_int_rnd(_203034, _203030) = uniform_int_rnd(_203032, _203028)), _203034 = _203032, _203030 = _203028], (86 ^ _200464) ^ [_203387, _203389, _203391, _203393] : [-(tptp_const_array1(_203393, _203389) = tptp_const_array1(_203391, _203387)), _203393 = _203391, _203389 = _203387], (96 ^ _200464) ^ [_203774, _203776, _203778, _203780, _203782, _203784] : [-(tptp_const_array2(_203784, _203780, _203776) = tptp_const_array2(_203782, _203778, _203774)), _203784 = _203782, _203780 = _203778, _203776 = _203774], (110 ^ _200464) ^ [_204262, _204264, _204266, _204268] : [-(dim(_204268, _204264) = dim(_204266, _204262)), _204268 = _204266, _204264 = _204262], (120 ^ _200464) ^ [_204593, _204595] : [_204595 = _204593, -(inv(_204595) = inv(_204593))], (126 ^ _200464) ^ [_204839, _204841, _204843, _204845] : [-(tptp_msub(_204845, _204841) = tptp_msub(_204843, _204839)), _204845 = _204843, _204841 = _204839], (136 ^ _200464) ^ [_205198, _205200, _205202, _205204] : [-(tptp_madd(_205204, _205200) = tptp_madd(_205202, _205198)), _205204 = _205202, _205200 = _205198], (146 ^ _200464) ^ [_205557, _205559, _205561, _205563] : [-(tptp_mmul(_205563, _205559) = tptp_mmul(_205561, _205557)), _205563 = _205561, _205559 = _205557], (156 ^ _200464) ^ [_205888, _205890] : [_205890 = _205888, -(trans(_205890) = trans(_205888))], (162 ^ _200464) ^ [_206162, _206164, _206166, _206168, _206170, _206172] : [-(sum(_206172, _206168, _206164) = sum(_206170, _206166, _206162)), _206172 = _206170, _206168 = _206166, _206164 = _206162], (176 ^ _200464) ^ [_206650, _206652, _206654, _206656] : [-(plus(_206656, _206652) = plus(_206654, _206650)), _206656 = _206654, _206652 = _206650], (186 ^ _200464) ^ [_206981, _206983] : [_206983 = _206981, -(pred(_206983) = pred(_206981))], (192 ^ _200464) ^ [_207227, _207229, _207231, _207233] : [-(minus(_207233, _207229) = minus(_207231, _207227)), _207233 = _207231, _207229 = _207227], (202 ^ _200464) ^ [_207614, _207616, _207618, _207620, _207622, _207624] : [-(a_select3(_207624, _207620, _207616) = a_select3(_207622, _207618, _207614)), _207624 = _207622, _207620 = _207618, _207616 = _207614], (216 ^ _200464) ^ [_208158, _208160, _208162, _208164, _208166, _208168, _208170, _208172] : [-(tptp_update3(_208172, _208168, _208164, _208160) = tptp_update3(_208170, _208166, _208162, _208158)), _208172 = _208170, _208168 = _208166, _208164 = _208162, _208160 = _208158], (234 ^ _200464) ^ [_208791, _208793, _208795, _208797] : [-(a_select2(_208797, _208793) = a_select2(_208795, _208791)), _208797 = _208795, _208793 = _208791], (258 ^ _200464) ^ [_209618, _209620] : [_209620 = _209618, -(succ(_209620) = succ(_209618))], (244 ^ _200464) ^ [_209178, _209180, _209182, _209184, _209186, _209188] : [-(tptp_update2(_209188, _209184, _209180) = tptp_update2(_209186, _209182, _209178)), _209188 = _209186, _209184 = _209182, _209180 = _209178], (869 ^ _200464) ^ [] : [-(gt(n5, n4))], (871 ^ _200464) ^ [] : [-(gt(n4, tptp_minus_1))], (873 ^ _200464) ^ [] : [-(gt(n5, tptp_minus_1))], (875 ^ _200464) ^ [] : [-(gt(n0, tptp_minus_1))], (877 ^ _200464) ^ [] : [-(gt(n1, tptp_minus_1))], (879 ^ _200464) ^ [] : [-(gt(n2, tptp_minus_1))], (881 ^ _200464) ^ [] : [-(gt(n3, tptp_minus_1))], (883 ^ _200464) ^ [] : [-(gt(n4, n0))], (885 ^ _200464) ^ [] : [-(gt(n5, n0))], (887 ^ _200464) ^ [] : [-(gt(n1, n0))], (889 ^ _200464) ^ [] : [-(gt(n2, n0))], (891 ^ _200464) ^ [] : [-(gt(n3, n0))], (893 ^ _200464) ^ [] : [-(gt(n4, n1))], (895 ^ _200464) ^ [] : [-(gt(n5, n1))], (897 ^ _200464) ^ [] : [-(gt(n2, n1))], (899 ^ _200464) ^ [] : [-(gt(n3, n1))], (901 ^ _200464) ^ [] : [-(gt(n4, n2))], (903 ^ _200464) ^ [] : [-(gt(n5, n2))], (905 ^ _200464) ^ [] : [-(gt(n3, n2))], (907 ^ _200464) ^ [] : [-(gt(n4, n3))], (909 ^ _200464) ^ [] : [-(gt(n5, n3))], (911 ^ _200464) ^ [_236974] : [leq(n0, _236974), leq(_236974, n4), -(_236974 = n0), -(_236974 = n1), -(_236974 = n2), -(_236974 = n3), -(_236974 = n4)], (937 ^ _200464) ^ [_237595] : [leq(n0, _237595), leq(_237595, n5), -(_237595 = n0), -(_237595 = n1), -(_237595 = n2), -(_237595 = n3), -(_237595 = n4), -(_237595 = n5)], (967 ^ _200464) ^ [_238302] : [-(_238302 = n0), leq(n0, _238302), leq(_238302, n0)], (977 ^ _200464) ^ [_238577] : [leq(n0, _238577), leq(_238577, n1), -(_238577 = n0), -(_238577 = n1)], (991 ^ _200464) ^ [_238940] : [leq(n0, _238940), leq(_238940, n2), -(_238940 = n0), -(_238940 = n1), -(_238940 = n2)], (1031 ^ _200464) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (1033 ^ _200464) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (1035 ^ _200464) ^ [] : [-(succ(n0) = n1)], (1037 ^ _200464) ^ [] : [-(succ(succ(n0)) = n2)], (1039 ^ _200464) ^ [] : [-(succ(succ(succ(n0))) = n3)], (1009 ^ _200464) ^ [_239389] : [leq(n0, _239389), leq(_239389, n3), -(_239389 = n0), -(_239389 = n1), -(_239389 = n2), -(_239389 = n3)], (264 ^ _200464) ^ [_209936, _209938] : [-(gt(_209938, _209936)), -(gt(_209936, _209938)), -(_209938 = _209936)], (274 ^ _200464) ^ [_210251, _210253, _210255] : [-(gt(_210255, _210251)), gt(_210255, _210253), gt(_210253, _210251)], (284 ^ _200464) ^ [_210530] : [gt(_210530, _210530)], (286 ^ _200464) ^ [_210608] : [-(leq(_210608, _210608))], (288 ^ _200464) ^ [_210729, _210731, _210733] : [-(leq(_210733, _210729)), leq(_210733, _210731), leq(_210731, _210729)], (298 ^ _200464) ^ [_211067, _211069] : [lt(_211069, _211067), -(gt(_211067, _211069))], (304 ^ _200464) ^ [_211229, _211231] : [gt(_211229, _211231), -(lt(_211231, _211229))], (310 ^ _200464) ^ [_211470, _211472] : [geq(_211472, _211470), -(leq(_211470, _211472))], (316 ^ _200464) ^ [_211632, _211634] : [leq(_211632, _211634), -(geq(_211634, _211632))], (322 ^ _200464) ^ [_211844, _211846] : [gt(_211844, _211846), -(leq(_211846, _211844))], (328 ^ _200464) ^ [_212054, _212056] : [-(gt(_212054, _212056)), leq(_212056, _212054), -(_212056 = _212054)], (338 ^ _200464) ^ [_212385, _212387] : [leq(_212387, pred(_212385)), -(gt(_212385, _212387))], (344 ^ _200464) ^ [_212551, _212553] : [gt(_212551, _212553), -(leq(_212553, pred(_212551)))], (350 ^ _200464) ^ [_212738] : [-(gt(succ(_212738), _212738))], (352 ^ _200464) ^ [_212847, _212849] : [leq(_212849, _212847), -(leq(_212849, succ(_212847)))], (358 ^ _200464) ^ [_213090, _213092] : [leq(_213092, _213090), -(gt(succ(_213090), _213092))], (364 ^ _200464) ^ [_213256, _213258] : [gt(succ(_213256), _213258), -(leq(_213258, _213256))], (370 ^ _200464) ^ [_213472, _213474] : [leq(n0, _213474), -(leq(uniform_int_rnd(_213472, _213474), _213474))], (376 ^ _200464) ^ [_213688, _213690] : [leq(n0, _213690), -(leq(n0, uniform_int_rnd(_213688, _213690)))], (382 ^ _200464) ^ [_213932, _213934, _213936, _213938] : [-(a_select2(tptp_const_array1(dim(_213936, _213934), _213932), _213938) = _213932), leq(_213936, _213938), leq(_213938, _213934)], (392 ^ _200464) ^ [_214339, _214341, _214343, _214345, _214347, _214349, _214351] : [-(a_select3(tptp_const_array2(dim(_214349, _214347), dim(_214343, _214341), _214339), _214351, _214345) = _214339), leq(_214349, _214351), leq(_214351, _214347), leq(_214343, _214345), leq(_214345, _214341)], (410 ^ _200464) ^ [_214934, _214936] : [413 ^ _200464 : [(414 ^ _200464) ^ [] : [-(leq(n0, 411 ^ [_214934, _214936]))], (416 ^ _200464) ^ [] : [-(leq(411 ^ [_214934, _214936], _214934))], (418 ^ _200464) ^ [] : [-(leq(n0, 412 ^ [_214934, _214936]))], (420 ^ _200464) ^ [] : [-(leq(412 ^ [_214934, _214936], _214934))], (422 ^ _200464) ^ [] : [a_select3(_214936, 411 ^ [_214934, _214936], 412 ^ [_214934, _214936]) = a_select3(_214936, 412 ^ [_214934, _214936], 411 ^ [_214934, _214936])]], 423 ^ _200464 : [(424 ^ _200464) ^ [_215691, _215693] : [-(a_select3(trans(_214936), _215693, _215691) = a_select3(trans(_214936), _215691, _215693)), leq(n0, _215693), leq(_215693, _214934), leq(n0, _215691), leq(_215691, _214934)]]], (442 ^ _200464) ^ [_216238, _216240] : [445 ^ _200464 : [(446 ^ _200464) ^ [] : [-(leq(n0, 443 ^ [_216238, _216240]))], (448 ^ _200464) ^ [] : [-(leq(443 ^ [_216238, _216240], _216238))], (450 ^ _200464) ^ [] : [-(leq(n0, 444 ^ [_216238, _216240]))], (452 ^ _200464) ^ [] : [-(leq(444 ^ [_216238, _216240], _216238))], (454 ^ _200464) ^ [] : [a_select3(_216240, 443 ^ [_216238, _216240], 444 ^ [_216238, _216240]) = a_select3(_216240, 444 ^ [_216238, _216240], 443 ^ [_216238, _216240])]], 455 ^ _200464 : [(456 ^ _200464) ^ [_216995, _216997] : [-(a_select3(inv(_216240), _216997, _216995) = a_select3(inv(_216240), _216995, _216997)), leq(n0, _216997), leq(_216997, _216238), leq(n0, _216995), leq(_216995, _216238)]]], (474 ^ _200464) ^ [_217542, _217544] : [477 ^ _200464 : [(478 ^ _200464) ^ [] : [-(leq(n0, 475 ^ [_217542, _217544]))], (480 ^ _200464) ^ [] : [-(leq(475 ^ [_217542, _217544], _217542))], (482 ^ _200464) ^ [] : [-(leq(n0, 476 ^ [_217542, _217544]))], (484 ^ _200464) ^ [] : [-(leq(476 ^ [_217542, _217544], _217542))], (486 ^ _200464) ^ [] : [a_select3(_217544, 475 ^ [_217542, _217544], 476 ^ [_217542, _217544]) = a_select3(_217544, 476 ^ [_217542, _217544], 475 ^ [_217542, _217544])]], 487 ^ _200464 : [(488 ^ _200464) ^ [_218355, _218357, _218359, _218361] : [-(a_select3(tptp_update3(_217544, _218357, _218357, _218355), _218361, _218359) = a_select3(tptp_update3(_217544, _218357, _218357, _218355), _218359, _218361)), leq(n0, _218361), leq(_218361, _217542), leq(n0, _218359), leq(_218359, _217542), leq(n0, _218357), leq(_218357, _217542)]]], (514 ^ _200464) ^ [_219174, _219176, _219178] : [519 ^ _200464 : [(520 ^ _200464) ^ [] : [-(leq(n0, 517 ^ [_219174, _219176, _219178]))], (522 ^ _200464) ^ [] : [-(leq(517 ^ [_219174, _219176, _219178], _219174))], (524 ^ _200464) ^ [] : [-(leq(n0, 518 ^ [_219174, _219176, _219178]))], (526 ^ _200464) ^ [] : [-(leq(518 ^ [_219174, _219176, _219178], _219174))], (528 ^ _200464) ^ [] : [a_select3(_219178, 517 ^ [_219174, _219176, _219178], 518 ^ [_219174, _219176, _219178]) = a_select3(_219178, 518 ^ [_219174, _219176, _219178], 517 ^ [_219174, _219176, _219178])]], 531 ^ _200464 : [(532 ^ _200464) ^ [] : [-(leq(n0, 529 ^ [_219174, _219176, _219178]))], (534 ^ _200464) ^ [] : [-(leq(529 ^ [_219174, _219176, _219178], _219174))], (536 ^ _200464) ^ [] : [-(leq(n0, 530 ^ [_219174, _219176, _219178]))], (538 ^ _200464) ^ [] : [-(leq(530 ^ [_219174, _219176, _219178], _219174))], (540 ^ _200464) ^ [] : [a_select3(_219176, 529 ^ [_219174, _219176, _219178], 530 ^ [_219174, _219176, _219178]) = a_select3(_219176, 530 ^ [_219174, _219176, _219178], 529 ^ [_219174, _219176, _219178])]], 541 ^ _200464 : [(542 ^ _200464) ^ [_220683, _220685] : [-(a_select3(tptp_madd(_219178, _219176), _220685, _220683) = a_select3(tptp_madd(_219178, _219176), _220683, _220685)), leq(n0, _220685), leq(_220685, _219174), leq(n0, _220683), leq(_220683, _219174)]]], (560 ^ _200464) ^ [_221269, _221271, _221273] : [565 ^ _200464 : [(566 ^ _200464) ^ [] : [-(leq(n0, 563 ^ [_221269, _221271, _221273]))], (568 ^ _200464) ^ [] : [-(leq(563 ^ [_221269, _221271, _221273], _221269))], (570 ^ _200464) ^ [] : [-(leq(n0, 564 ^ [_221269, _221271, _221273]))], (572 ^ _200464) ^ [] : [-(leq(564 ^ [_221269, _221271, _221273], _221269))], (574 ^ _200464) ^ [] : [a_select3(_221273, 563 ^ [_221269, _221271, _221273], 564 ^ [_221269, _221271, _221273]) = a_select3(_221273, 564 ^ [_221269, _221271, _221273], 563 ^ [_221269, _221271, _221273])]], 577 ^ _200464 : [(578 ^ _200464) ^ [] : [-(leq(n0, 575 ^ [_221269, _221271, _221273]))], (580 ^ _200464) ^ [] : [-(leq(575 ^ [_221269, _221271, _221273], _221269))], (582 ^ _200464) ^ [] : [-(leq(n0, 576 ^ [_221269, _221271, _221273]))], (584 ^ _200464) ^ [] : [-(leq(576 ^ [_221269, _221271, _221273], _221269))], (586 ^ _200464) ^ [] : [a_select3(_221271, 575 ^ [_221269, _221271, _221273], 576 ^ [_221269, _221271, _221273]) = a_select3(_221271, 576 ^ [_221269, _221271, _221273], 575 ^ [_221269, _221271, _221273])]], 587 ^ _200464 : [(588 ^ _200464) ^ [_222778, _222780] : [-(a_select3(tptp_msub(_221273, _221271), _222780, _222778) = a_select3(tptp_msub(_221273, _221271), _222778, _222780)), leq(n0, _222780), leq(_222780, _221269), leq(n0, _222778), leq(_222778, _221269)]]], (606 ^ _200464) ^ [_223364, _223366, _223368] : [609 ^ _200464 : [(610 ^ _200464) ^ [] : [-(leq(n0, 607 ^ [_223364, _223366, _223368]))], (612 ^ _200464) ^ [] : [-(leq(607 ^ [_223364, _223366, _223368], _223364))], (614 ^ _200464) ^ [] : [-(leq(n0, 608 ^ [_223364, _223366, _223368]))], (616 ^ _200464) ^ [] : [-(leq(608 ^ [_223364, _223366, _223368], _223364))], (618 ^ _200464) ^ [] : [a_select3(_223366, 607 ^ [_223364, _223366, _223368], 608 ^ [_223364, _223366, _223368]) = a_select3(_223366, 608 ^ [_223364, _223366, _223368], 607 ^ [_223364, _223366, _223368])]], 619 ^ _200464 : [(620 ^ _200464) ^ [_224177, _224179] : [-(a_select3(tptp_mmul(_223368, tptp_mmul(_223366, trans(_223368))), _224179, _224177) = a_select3(tptp_mmul(_223368, tptp_mmul(_223366, trans(_223368))), _224177, _224179)), leq(n0, _224179), leq(_224179, _223364), leq(n0, _224177), leq(_224177, _223364)]]], (638 ^ _200464) ^ [_224796, _224798, _224800, _224802] : [641 ^ _200464 : [(642 ^ _200464) ^ [] : [-(leq(n0, 639 ^ [_224796, _224798, _224800, _224802]))], (644 ^ _200464) ^ [] : [-(leq(639 ^ [_224796, _224798, _224800, _224802], _224796))], (646 ^ _200464) ^ [] : [-(leq(n0, 640 ^ [_224796, _224798, _224800, _224802]))], (648 ^ _200464) ^ [] : [-(leq(640 ^ [_224796, _224798, _224800, _224802], _224796))], (650 ^ _200464) ^ [] : [a_select3(_224800, 639 ^ [_224796, _224798, _224800, _224802], 640 ^ [_224796, _224798, _224800, _224802]) = a_select3(_224800, 640 ^ [_224796, _224798, _224800, _224802], 639 ^ [_224796, _224798, _224800, _224802])]], 651 ^ _200464 : [(652 ^ _200464) ^ [_225653, _225655] : [-(a_select3(tptp_mmul(_224802, tptp_mmul(_224800, trans(_224802))), _225655, _225653) = a_select3(tptp_mmul(_224802, tptp_mmul(_224800, trans(_224802))), _225653, _225655)), leq(n0, _225655), leq(_225655, _224798), leq(n0, _225653), leq(_225653, _224798)]]], (670 ^ _200464) ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362] : [675 ^ _200464 : [(676 ^ _200464) ^ [] : [-(leq(n0, 673 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362]))], (678 ^ _200464) ^ [] : [-(leq(673 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362], _226348))], (680 ^ _200464) ^ [] : [-(leq(n0, 674 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362]))], (682 ^ _200464) ^ [] : [-(leq(674 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362], _226348))], (684 ^ _200464) ^ [] : [a_select3(_226356, 673 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362], 674 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362]) = a_select3(_226356, 674 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362], 673 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362])]], 689 ^ _200464 : [(690 ^ _200464) ^ [] : [-(leq(n0, 687 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362]))], (692 ^ _200464) ^ [] : [-(leq(687 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362], _226350))], (694 ^ _200464) ^ [] : [-(leq(n0, 688 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362]))], (696 ^ _200464) ^ [] : [-(leq(688 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362], _226350))], (698 ^ _200464) ^ [] : [a_select3(_226362, 687 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362], 688 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362]) = a_select3(_226362, 688 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362], 687 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362])]], 701 ^ _200464 : [(702 ^ _200464) ^ [] : [-(leq(n0, 699 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362]))], (704 ^ _200464) ^ [] : [-(leq(699 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362], _226350))], (706 ^ _200464) ^ [] : [-(leq(n0, 700 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362]))], (708 ^ _200464) ^ [] : [-(leq(700 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362], _226350))], (710 ^ _200464) ^ [] : [a_select3(_226352, 699 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362], 700 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362]) = a_select3(_226352, 700 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362], 699 ^ [_226348, _226350, _226352, _226354, _226356, _226358, _226360, _226362])]], 711 ^ _200464 : [(712 ^ _200464) ^ [_229276, _229278] : [-(a_select3(tptp_madd(_226362, tptp_mmul(_226360, tptp_mmul(tptp_madd(tptp_mmul(_226358, tptp_mmul(_226356, trans(_226358))), tptp_mmul(_226354, tptp_mmul(_226352, trans(_226354)))), trans(_226360)))), _229278, _229276) = a_select3(tptp_madd(_226362, tptp_mmul(_226360, tptp_mmul(tptp_madd(tptp_mmul(_226358, tptp_mmul(_226356, trans(_226358))), tptp_mmul(_226354, tptp_mmul(_226352, trans(_226354)))), trans(_226360)))), _229276, _229278)), leq(n0, _229278), leq(_229278, _226350), leq(n0, _229276), leq(_229276, _226350)]]], (730 ^ _200464) ^ [_230029] : [-(sum(n0, tptp_minus_1, _230029) = n0)], (732 ^ _200464) ^ [_230111] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _230111))], (734 ^ _200464) ^ [] : [-(succ(tptp_minus_1) = n0)], (736 ^ _200464) ^ [_230246] : [-(plus(_230246, n1) = succ(_230246))], (738 ^ _200464) ^ [_230329] : [-(plus(n1, _230329) = succ(_230329))], (740 ^ _200464) ^ [_230412] : [-(plus(_230412, n2) = succ(succ(_230412)))], (742 ^ _200464) ^ [_230497] : [-(plus(n2, _230497) = succ(succ(_230497)))], (744 ^ _200464) ^ [_230582] : [-(plus(_230582, n3) = succ(succ(succ(_230582))))], (746 ^ _200464) ^ [_230669] : [-(plus(n3, _230669) = succ(succ(succ(_230669))))], (748 ^ _200464) ^ [_230756] : [-(plus(_230756, n4) = succ(succ(succ(succ(_230756)))))], (750 ^ _200464) ^ [_230845] : [-(plus(n4, _230845) = succ(succ(succ(succ(_230845)))))], (752 ^ _200464) ^ [_230934] : [-(plus(_230934, n5) = succ(succ(succ(succ(succ(_230934))))))], (754 ^ _200464) ^ [_231025] : [-(plus(n5, _231025) = succ(succ(succ(succ(succ(_231025))))))], (756 ^ _200464) ^ [_231116] : [-(minus(_231116, n1) = pred(_231116))], (758 ^ _200464) ^ [_231199] : [-(pred(succ(_231199)) = _231199)], (760 ^ _200464) ^ [_231281] : [-(succ(pred(_231281)) = _231281)], (762 ^ _200464) ^ [_231421, _231423] : [leq(succ(_231423), succ(_231421)), -(leq(_231423, _231421))], (768 ^ _200464) ^ [_231591, _231593] : [leq(_231593, _231591), -(leq(succ(_231593), succ(_231591)))], (774 ^ _200464) ^ [_231811, _231813] : [leq(succ(_231813), _231811), -(gt(_231811, _231813))], (780 ^ _200464) ^ [_232025, _232027] : [leq(minus(_232027, _232025), _232027), -(leq(n0, _232025))], (786 ^ _200464) ^ [_232254, _232256, _232258, _232260] : [-(a_select3(tptp_update3(_232260, _232258, _232256, _232254), _232258, _232256) = _232254)], (788 ^ _200464) ^ [_232446, _232448, _232450, _232452, _232454, _232456, _232458] : [-(a_select3(tptp_update3(_232450, _232458, _232456, _232446), _232454, _232452) = _232448), -(_232458 = _232454), _232456 = _232452, a_select3(_232450, _232454, _232452) = _232448], (802 ^ _200464) ^ [_232989, _232991, _232993, _232995, _232997, _232999] : [-(a_select3(tptp_update3(_232991, _232995, _232993, _232989), _232999, _232997) = _232989), 807 ^ _200464 : [(808 ^ _200464) ^ [] : [-(leq(n0, 805 ^ [_232989, _232991, _232993, _232995, _232997, _232999]))], (810 ^ _200464) ^ [] : [-(leq(n0, 806 ^ [_232989, _232991, _232993, _232995, _232997, _232999]))], (812 ^ _200464) ^ [] : [-(leq(805 ^ [_232989, _232991, _232993, _232995, _232997, _232999], _232995))], (814 ^ _200464) ^ [] : [-(leq(806 ^ [_232989, _232991, _232993, _232995, _232997, _232999], _232993))], (816 ^ _200464) ^ [] : [a_select3(_232991, 805 ^ [_232989, _232991, _232993, _232995, _232997, _232999], 806 ^ [_232989, _232991, _232993, _232995, _232997, _232999]) = _232989]], leq(n0, _232999), leq(_232999, _232995), leq(n0, _232997), leq(_232997, _232993)], (834 ^ _200464) ^ [_234331, _234333, _234335] : [-(a_select2(tptp_update2(_234335, _234333, _234331), _234333) = _234331)], (836 ^ _200464) ^ [_234491, _234493, _234495, _234497, _234499] : [-(a_select2(tptp_update2(_234495, _234499, _234491), _234497) = _234493), -(_234499 = _234497), a_select2(_234495, _234497) = _234493], (865 ^ _200464) ^ [] : [-(true)], (867 ^ _200464) ^ [] : [def = use], (846 ^ _200464) ^ [_234871, _234873, _234875, _234877] : [-(a_select2(tptp_update2(_234873, _234875, _234871), _234877) = _234871), 850 ^ _200464 : [(851 ^ _200464) ^ [] : [-(leq(n0, 849 ^ [_234871, _234873, _234875, _234877]))], (853 ^ _200464) ^ [] : [-(leq(849 ^ [_234871, _234873, _234875, _234877], _234875))], (855 ^ _200464) ^ [] : [a_select2(_234873, 849 ^ [_234871, _234873, _234875, _234877]) = _234871]], leq(n0, _234877), leq(_234877, _234875)]], input).
% 27.85/27.37 ncf('1',plain,[gt(pv1325, pv1325)],start(284 ^ 0,bind([[_210530], [pv1325]]))).
% 27.85/27.37 ncf('1.1',plain,[-(gt(pv1325, pv1325)), -(gt(pv1325, pv1325)), -(pv1325 = pv1325)],extension(264 ^ 1,bind([[_209936, _209938], [pv1325, pv1325]]))).
% 27.85/27.37 ncf('1.1.1',plain,[gt(pv1325, pv1325)],reduction('1')).
% 27.85/27.37 ncf('1.1.2',plain,[pv1325 = pv1325, -(geq(pv1325, n0)), geq(pv1325, n2), n2 = n0],extension(34 ^ 2,bind([[_201704, _201706, _201708, _201710], [n0, n2, pv1325, pv1325]]))).
% 27.85/27.37 ncf('1.1.2.1',plain,[geq(pv1325, n0), -(geq(pv1325, n0)), pv1325 = pv1325, n0 = n0],extension(34 ^ 3,bind([[_201704, _201706, _201708, _201710], [n0, n0, pv1325, pv1325]]))).
% 27.85/27.37 ncf('1.1.2.1.1',plain,[geq(pv1325, n0), -(geq(pv1325, n0)), pv1325 = pv1325, n0 = n0],extension(34 ^ 4,bind([[_201704, _201706, _201708, _201710], [n0, n0, pv1325, pv1325]]))).
% 27.85/27.37 ncf('1.1.2.1.1.1',plain,[geq(pv1325, n0), -(leq(n0, pv1325))],extension(310 ^ 5,bind([[_211470, _211472], [n0, pv1325]]))).
% 27.85/27.37 ncf('1.1.2.1.1.1.1',plain,[leq(n0, pv1325)],extension(1057 ^ 6)).
% 27.85/27.37 ncf('1.1.2.1.1.2',plain,[-(pv1325 = pv1325)],reduction('1.1')).
% 27.85/27.37 ncf('1.1.2.1.1.3',plain,[-(n0 = n0)],extension(2 ^ 5,bind([[_200608], [n0]]))).
% 27.85/27.37 ncf('1.1.2.1.2',plain,[-(pv1325 = pv1325)],reduction('1.1')).
% 27.85/27.37 ncf('1.1.2.1.3',plain,[-(n0 = n0)],extension(2 ^ 4,bind([[_200608], [n0]]))).
% 27.85/27.37 ncf('1.1.2.2',plain,[-(geq(pv1325, n2)), leq(n2, pv1325)],extension(316 ^ 3,bind([[_211632, _211634], [n2, pv1325]]))).
% 27.85/27.37 ncf('1.1.2.2.1',plain,[-(leq(n2, pv1325))],extension(1047 ^ 4)).
% 27.85/27.37 ncf('1.1.2.3',plain,[-(n2 = n0), -(gt(n2, n0)), -(gt(n0, n2))],extension(264 ^ 3,bind([[_209936, _209938], [n0, n2]]))).
% 27.85/27.37 ncf('1.1.2.3.1',plain,[gt(n2, n0), -(leq(n0, n2))],extension(322 ^ 4,bind([[_211844, _211846], [n2, n0]]))).
% 27.85/27.37 ncf('1.1.2.3.1.1',plain,[leq(n0, n2), -(leq(n0, pv1325)), leq(n2, pv1325)],extension(288 ^ 5,bind([[_210729, _210731, _210733], [pv1325, n2, n0]]))).
% 27.85/27.37 ncf('1.1.2.3.1.1.1',plain,[leq(n0, pv1325)],extension(1057 ^ 6)).
% 27.85/27.37 ncf('1.1.2.3.1.1.2',plain,[-(leq(n2, pv1325))],extension(1047 ^ 6)).
% 27.85/27.37 ncf('1.1.2.3.2',plain,[gt(n0, n2), -(gt(n0, n0)), gt(n2, n0)],extension(274 ^ 4,bind([[_210251, _210253, _210255], [n0, n2, n0]]))).
% 27.85/27.37 ncf('1.1.2.3.2.1',plain,[gt(n0, n0)],extension(284 ^ 5,bind([[_210530], [n0]]))).
% 27.85/27.37 ncf('1.1.2.3.2.2',plain,[-(gt(n2, n0))],extension(889 ^ 5)).
% 27.85/27.37 %-----------------------------------------------------
% 27.85/27.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------