%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV169+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n026.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 : SWV169+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.03/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n026.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 03:03:35 EDT 2023
% 0.13/0.34 % 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, [(1143 ^ _206997) ^ [] : [a_select3(center_init, pv65, n0) = init], (1055 ^ _206997) ^ [] : [-(leq(n0, pv10))], (1057 ^ _206997) ^ [] : [-(leq(n0, pv11))], (1059 ^ _206997) ^ [] : [-(leq(n0, pv65))], (1061 ^ _206997) ^ [] : [-(leq(pv10, n135299))], (1063 ^ _206997) ^ [] : [-(leq(pv11, n4))], (1065 ^ _206997) ^ [] : [-(leq(pv65, n4))], (1067 ^ _206997) ^ [_247645, _247647] : [-(a_select3(q_init, _247647, _247645) = init), _247647 = pv10, gt(pv11, _247645), leq(n0, _247647), leq(n0, _247645), leq(_247647, n135299), leq(_247645, n4)], (1093 ^ _206997) ^ [_248312, _248314] : [gt(pv10, _248314), -(a_select3(q_init, _248314, _248312) = init), leq(n0, _248314), leq(n0, _248312), leq(_248314, n135299), leq(_248312, n4)], (1133 ^ _206997) ^ [_249384] : [-(a_select3(center_init, _249384, n0) = init), leq(n0, _249384), leq(_249384, n4)], (1115 ^ _206997) ^ [_248874] : [leq(n0, _248874), leq(_248874, pred(pv10)), 1122 ^ _206997 : [(1123 ^ _206997) ^ [_249102] : [-(a_select3(q_init, _248874, _249102) = init), leq(n0, _249102), leq(_249102, n4)]]], (2 ^ _206997) ^ [_207141] : [-(_207141 = _207141)], (4 ^ _206997) ^ [_207248, _207250] : [_207250 = _207248, -(_207248 = _207250)], (10 ^ _206997) ^ [_207452, _207454, _207456] : [-(_207456 = _207452), _207456 = _207454, _207454 = _207452], (20 ^ _206997) ^ [_207793, _207795, _207797, _207799] : [-(lt(_207797, _207793)), lt(_207799, _207795), _207799 = _207797, _207795 = _207793], (34 ^ _206997) ^ [_208237, _208239, _208241, _208243] : [-(geq(_208241, _208237)), geq(_208243, _208239), _208243 = _208241, _208239 = _208237], (48 ^ _206997) ^ [_208681, _208683, _208685, _208687] : [-(gt(_208685, _208681)), gt(_208687, _208683), _208687 = _208685, _208683 = _208681], (62 ^ _206997) ^ [_209105, _209107, _209109, _209111] : [-(leq(_209109, _209105)), leq(_209111, _209107), _209111 = _209109, _209107 = _209105], (76 ^ _206997) ^ [_209561, _209563, _209565, _209567] : [-(uniform_int_rnd(_209567, _209563) = uniform_int_rnd(_209565, _209561)), _209567 = _209565, _209563 = _209561], (86 ^ _206997) ^ [_209920, _209922, _209924, _209926] : [-(tptp_const_array1(_209926, _209922) = tptp_const_array1(_209924, _209920)), _209926 = _209924, _209922 = _209920], (96 ^ _206997) ^ [_210307, _210309, _210311, _210313, _210315, _210317] : [-(tptp_const_array2(_210317, _210313, _210309) = tptp_const_array2(_210315, _210311, _210307)), _210317 = _210315, _210313 = _210311, _210309 = _210307], (110 ^ _206997) ^ [_210795, _210797, _210799, _210801] : [-(dim(_210801, _210797) = dim(_210799, _210795)), _210801 = _210799, _210797 = _210795], (120 ^ _206997) ^ [_211126, _211128] : [_211128 = _211126, -(inv(_211128) = inv(_211126))], (126 ^ _206997) ^ [_211372, _211374, _211376, _211378] : [-(tptp_msub(_211378, _211374) = tptp_msub(_211376, _211372)), _211378 = _211376, _211374 = _211372], (136 ^ _206997) ^ [_211731, _211733, _211735, _211737] : [-(tptp_madd(_211737, _211733) = tptp_madd(_211735, _211731)), _211737 = _211735, _211733 = _211731], (146 ^ _206997) ^ [_212090, _212092, _212094, _212096] : [-(tptp_mmul(_212096, _212092) = tptp_mmul(_212094, _212090)), _212096 = _212094, _212092 = _212090], (156 ^ _206997) ^ [_212421, _212423] : [_212423 = _212421, -(trans(_212423) = trans(_212421))], (162 ^ _206997) ^ [_212695, _212697, _212699, _212701, _212703, _212705] : [-(sum(_212705, _212701, _212697) = sum(_212703, _212699, _212695)), _212705 = _212703, _212701 = _212699, _212697 = _212695], (176 ^ _206997) ^ [_213183, _213185, _213187, _213189] : [-(plus(_213189, _213185) = plus(_213187, _213183)), _213189 = _213187, _213185 = _213183], (186 ^ _206997) ^ [_213542, _213544, _213546, _213548] : [-(minus(_213548, _213544) = minus(_213546, _213542)), _213548 = _213546, _213544 = _213542], (196 ^ _206997) ^ [_213957, _213959, _213961, _213963, _213965, _213967, _213969, _213971] : [-(tptp_update3(_213971, _213967, _213963, _213959) = tptp_update3(_213969, _213965, _213961, _213957)), _213971 = _213969, _213967 = _213965, _213963 = _213961, _213959 = _213957], (214 ^ _206997) ^ [_214590, _214592, _214594, _214596] : [-(a_select2(_214596, _214592) = a_select2(_214594, _214590)), _214596 = _214594, _214592 = _214590], (224 ^ _206997) ^ [_214977, _214979, _214981, _214983, _214985, _214987] : [-(tptp_update2(_214987, _214983, _214979) = tptp_update2(_214985, _214981, _214977)), _214987 = _214985, _214983 = _214981, _214979 = _214977], (238 ^ _206997) ^ [_215437, _215439] : [_215439 = _215437, -(succ(_215439) = succ(_215437))], (244 ^ _206997) ^ [_215655, _215657] : [_215657 = _215655, -(pred(_215657) = pred(_215655))], (250 ^ _206997) ^ [_215909, _215911, _215913, _215915, _215917, _215919] : [-(a_select3(_215919, _215915, _215911) = a_select3(_215917, _215913, _215909)), _215919 = _215917, _215915 = _215913, _215911 = _215909], (869 ^ _206997) ^ [] : [-(gt(n5, n4))], (871 ^ _206997) ^ [] : [-(gt(n135299, n4))], (873 ^ _206997) ^ [] : [-(gt(n135299, n5))], (875 ^ _206997) ^ [] : [-(gt(n4, tptp_minus_1))], (877 ^ _206997) ^ [] : [-(gt(n5, tptp_minus_1))], (879 ^ _206997) ^ [] : [-(gt(n135299, tptp_minus_1))], (881 ^ _206997) ^ [] : [-(gt(n0, tptp_minus_1))], (883 ^ _206997) ^ [] : [-(gt(n1, tptp_minus_1))], (885 ^ _206997) ^ [] : [-(gt(n2, tptp_minus_1))], (887 ^ _206997) ^ [] : [-(gt(n3, tptp_minus_1))], (889 ^ _206997) ^ [] : [-(gt(n4, n0))], (891 ^ _206997) ^ [] : [-(gt(n5, n0))], (893 ^ _206997) ^ [] : [-(gt(n135299, n0))], (895 ^ _206997) ^ [] : [-(gt(n1, n0))], (897 ^ _206997) ^ [] : [-(gt(n2, n0))], (899 ^ _206997) ^ [] : [-(gt(n3, n0))], (901 ^ _206997) ^ [] : [-(gt(n4, n1))], (903 ^ _206997) ^ [] : [-(gt(n5, n1))], (905 ^ _206997) ^ [] : [-(gt(n135299, n1))], (907 ^ _206997) ^ [] : [-(gt(n2, n1))], (909 ^ _206997) ^ [] : [-(gt(n3, n1))], (911 ^ _206997) ^ [] : [-(gt(n4, n2))], (913 ^ _206997) ^ [] : [-(gt(n5, n2))], (915 ^ _206997) ^ [] : [-(gt(n135299, n2))], (917 ^ _206997) ^ [] : [-(gt(n3, n2))], (919 ^ _206997) ^ [] : [-(gt(n4, n3))], (921 ^ _206997) ^ [] : [-(gt(n5, n3))], (923 ^ _206997) ^ [] : [-(gt(n135299, n3))], (925 ^ _206997) ^ [_243878] : [leq(n0, _243878), leq(_243878, n4), -(_243878 = n0), -(_243878 = n1), -(_243878 = n2), -(_243878 = n3), -(_243878 = n4)], (951 ^ _206997) ^ [_244499] : [leq(n0, _244499), leq(_244499, n5), -(_244499 = n0), -(_244499 = n1), -(_244499 = n2), -(_244499 = n3), -(_244499 = n4), -(_244499 = n5)], (981 ^ _206997) ^ [_245206] : [-(_245206 = n0), leq(n0, _245206), leq(_245206, n0)], (991 ^ _206997) ^ [_245481] : [leq(n0, _245481), leq(_245481, n1), -(_245481 = n0), -(_245481 = n1)], (1005 ^ _206997) ^ [_245844] : [leq(n0, _245844), leq(_245844, n2), -(_245844 = n0), -(_245844 = n1), -(_245844 = n2)], (1045 ^ _206997) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (1047 ^ _206997) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (1049 ^ _206997) ^ [] : [-(succ(n0) = n1)], (1051 ^ _206997) ^ [] : [-(succ(succ(n0)) = n2)], (1053 ^ _206997) ^ [] : [-(succ(succ(succ(n0))) = n3)], (1023 ^ _206997) ^ [_246293] : [leq(n0, _246293), leq(_246293, n3), -(_246293 = n0), -(_246293 = n1), -(_246293 = n2), -(_246293 = n3)], (264 ^ _206997) ^ [_216469, _216471] : [-(gt(_216471, _216469)), -(gt(_216469, _216471)), -(_216471 = _216469)], (274 ^ _206997) ^ [_216784, _216786, _216788] : [-(gt(_216788, _216784)), gt(_216788, _216786), gt(_216786, _216784)], (284 ^ _206997) ^ [_217063] : [gt(_217063, _217063)], (286 ^ _206997) ^ [_217141] : [-(leq(_217141, _217141))], (288 ^ _206997) ^ [_217262, _217264, _217266] : [-(leq(_217266, _217262)), leq(_217266, _217264), leq(_217264, _217262)], (298 ^ _206997) ^ [_217600, _217602] : [lt(_217602, _217600), -(gt(_217600, _217602))], (304 ^ _206997) ^ [_217762, _217764] : [gt(_217762, _217764), -(lt(_217764, _217762))], (310 ^ _206997) ^ [_218003, _218005] : [geq(_218005, _218003), -(leq(_218003, _218005))], (316 ^ _206997) ^ [_218165, _218167] : [leq(_218165, _218167), -(geq(_218167, _218165))], (322 ^ _206997) ^ [_218377, _218379] : [gt(_218377, _218379), -(leq(_218379, _218377))], (328 ^ _206997) ^ [_218587, _218589] : [-(gt(_218587, _218589)), leq(_218589, _218587), -(_218589 = _218587)], (338 ^ _206997) ^ [_218918, _218920] : [leq(_218920, pred(_218918)), -(gt(_218918, _218920))], (344 ^ _206997) ^ [_219084, _219086] : [gt(_219084, _219086), -(leq(_219086, pred(_219084)))], (350 ^ _206997) ^ [_219271] : [-(gt(succ(_219271), _219271))], (352 ^ _206997) ^ [_219380, _219382] : [leq(_219382, _219380), -(leq(_219382, succ(_219380)))], (358 ^ _206997) ^ [_219623, _219625] : [leq(_219625, _219623), -(gt(succ(_219623), _219625))], (364 ^ _206997) ^ [_219789, _219791] : [gt(succ(_219789), _219791), -(leq(_219791, _219789))], (370 ^ _206997) ^ [_220005, _220007] : [leq(n0, _220007), -(leq(uniform_int_rnd(_220005, _220007), _220007))], (376 ^ _206997) ^ [_220221, _220223] : [leq(n0, _220223), -(leq(n0, uniform_int_rnd(_220221, _220223)))], (382 ^ _206997) ^ [_220465, _220467, _220469, _220471] : [-(a_select2(tptp_const_array1(dim(_220469, _220467), _220465), _220471) = _220465), leq(_220469, _220471), leq(_220471, _220467)], (392 ^ _206997) ^ [_220872, _220874, _220876, _220878, _220880, _220882, _220884] : [-(a_select3(tptp_const_array2(dim(_220882, _220880), dim(_220876, _220874), _220872), _220884, _220878) = _220872), leq(_220882, _220884), leq(_220884, _220880), leq(_220876, _220878), leq(_220878, _220874)], (410 ^ _206997) ^ [_221467, _221469] : [413 ^ _206997 : [(414 ^ _206997) ^ [] : [-(leq(n0, 411 ^ [_221467, _221469]))], (416 ^ _206997) ^ [] : [-(leq(411 ^ [_221467, _221469], _221467))], (418 ^ _206997) ^ [] : [-(leq(n0, 412 ^ [_221467, _221469]))], (420 ^ _206997) ^ [] : [-(leq(412 ^ [_221467, _221469], _221467))], (422 ^ _206997) ^ [] : [a_select3(_221469, 411 ^ [_221467, _221469], 412 ^ [_221467, _221469]) = a_select3(_221469, 412 ^ [_221467, _221469], 411 ^ [_221467, _221469])]], 423 ^ _206997 : [(424 ^ _206997) ^ [_222224, _222226] : [-(a_select3(trans(_221469), _222226, _222224) = a_select3(trans(_221469), _222224, _222226)), leq(n0, _222226), leq(_222226, _221467), leq(n0, _222224), leq(_222224, _221467)]]], (442 ^ _206997) ^ [_222771, _222773] : [445 ^ _206997 : [(446 ^ _206997) ^ [] : [-(leq(n0, 443 ^ [_222771, _222773]))], (448 ^ _206997) ^ [] : [-(leq(443 ^ [_222771, _222773], _222771))], (450 ^ _206997) ^ [] : [-(leq(n0, 444 ^ [_222771, _222773]))], (452 ^ _206997) ^ [] : [-(leq(444 ^ [_222771, _222773], _222771))], (454 ^ _206997) ^ [] : [a_select3(_222773, 443 ^ [_222771, _222773], 444 ^ [_222771, _222773]) = a_select3(_222773, 444 ^ [_222771, _222773], 443 ^ [_222771, _222773])]], 455 ^ _206997 : [(456 ^ _206997) ^ [_223528, _223530] : [-(a_select3(inv(_222773), _223530, _223528) = a_select3(inv(_222773), _223528, _223530)), leq(n0, _223530), leq(_223530, _222771), leq(n0, _223528), leq(_223528, _222771)]]], (474 ^ _206997) ^ [_224075, _224077] : [477 ^ _206997 : [(478 ^ _206997) ^ [] : [-(leq(n0, 475 ^ [_224075, _224077]))], (480 ^ _206997) ^ [] : [-(leq(475 ^ [_224075, _224077], _224075))], (482 ^ _206997) ^ [] : [-(leq(n0, 476 ^ [_224075, _224077]))], (484 ^ _206997) ^ [] : [-(leq(476 ^ [_224075, _224077], _224075))], (486 ^ _206997) ^ [] : [a_select3(_224077, 475 ^ [_224075, _224077], 476 ^ [_224075, _224077]) = a_select3(_224077, 476 ^ [_224075, _224077], 475 ^ [_224075, _224077])]], 487 ^ _206997 : [(488 ^ _206997) ^ [_224888, _224890, _224892, _224894] : [-(a_select3(tptp_update3(_224077, _224890, _224890, _224888), _224894, _224892) = a_select3(tptp_update3(_224077, _224890, _224890, _224888), _224892, _224894)), leq(n0, _224894), leq(_224894, _224075), leq(n0, _224892), leq(_224892, _224075), leq(n0, _224890), leq(_224890, _224075)]]], (514 ^ _206997) ^ [_225707, _225709, _225711] : [519 ^ _206997 : [(520 ^ _206997) ^ [] : [-(leq(n0, 517 ^ [_225707, _225709, _225711]))], (522 ^ _206997) ^ [] : [-(leq(517 ^ [_225707, _225709, _225711], _225707))], (524 ^ _206997) ^ [] : [-(leq(n0, 518 ^ [_225707, _225709, _225711]))], (526 ^ _206997) ^ [] : [-(leq(518 ^ [_225707, _225709, _225711], _225707))], (528 ^ _206997) ^ [] : [a_select3(_225711, 517 ^ [_225707, _225709, _225711], 518 ^ [_225707, _225709, _225711]) = a_select3(_225711, 518 ^ [_225707, _225709, _225711], 517 ^ [_225707, _225709, _225711])]], 531 ^ _206997 : [(532 ^ _206997) ^ [] : [-(leq(n0, 529 ^ [_225707, _225709, _225711]))], (534 ^ _206997) ^ [] : [-(leq(529 ^ [_225707, _225709, _225711], _225707))], (536 ^ _206997) ^ [] : [-(leq(n0, 530 ^ [_225707, _225709, _225711]))], (538 ^ _206997) ^ [] : [-(leq(530 ^ [_225707, _225709, _225711], _225707))], (540 ^ _206997) ^ [] : [a_select3(_225709, 529 ^ [_225707, _225709, _225711], 530 ^ [_225707, _225709, _225711]) = a_select3(_225709, 530 ^ [_225707, _225709, _225711], 529 ^ [_225707, _225709, _225711])]], 541 ^ _206997 : [(542 ^ _206997) ^ [_227216, _227218] : [-(a_select3(tptp_madd(_225711, _225709), _227218, _227216) = a_select3(tptp_madd(_225711, _225709), _227216, _227218)), leq(n0, _227218), leq(_227218, _225707), leq(n0, _227216), leq(_227216, _225707)]]], (560 ^ _206997) ^ [_227802, _227804, _227806] : [565 ^ _206997 : [(566 ^ _206997) ^ [] : [-(leq(n0, 563 ^ [_227802, _227804, _227806]))], (568 ^ _206997) ^ [] : [-(leq(563 ^ [_227802, _227804, _227806], _227802))], (570 ^ _206997) ^ [] : [-(leq(n0, 564 ^ [_227802, _227804, _227806]))], (572 ^ _206997) ^ [] : [-(leq(564 ^ [_227802, _227804, _227806], _227802))], (574 ^ _206997) ^ [] : [a_select3(_227806, 563 ^ [_227802, _227804, _227806], 564 ^ [_227802, _227804, _227806]) = a_select3(_227806, 564 ^ [_227802, _227804, _227806], 563 ^ [_227802, _227804, _227806])]], 577 ^ _206997 : [(578 ^ _206997) ^ [] : [-(leq(n0, 575 ^ [_227802, _227804, _227806]))], (580 ^ _206997) ^ [] : [-(leq(575 ^ [_227802, _227804, _227806], _227802))], (582 ^ _206997) ^ [] : [-(leq(n0, 576 ^ [_227802, _227804, _227806]))], (584 ^ _206997) ^ [] : [-(leq(576 ^ [_227802, _227804, _227806], _227802))], (586 ^ _206997) ^ [] : [a_select3(_227804, 575 ^ [_227802, _227804, _227806], 576 ^ [_227802, _227804, _227806]) = a_select3(_227804, 576 ^ [_227802, _227804, _227806], 575 ^ [_227802, _227804, _227806])]], 587 ^ _206997 : [(588 ^ _206997) ^ [_229311, _229313] : [-(a_select3(tptp_msub(_227806, _227804), _229313, _229311) = a_select3(tptp_msub(_227806, _227804), _229311, _229313)), leq(n0, _229313), leq(_229313, _227802), leq(n0, _229311), leq(_229311, _227802)]]], (606 ^ _206997) ^ [_229897, _229899, _229901] : [609 ^ _206997 : [(610 ^ _206997) ^ [] : [-(leq(n0, 607 ^ [_229897, _229899, _229901]))], (612 ^ _206997) ^ [] : [-(leq(607 ^ [_229897, _229899, _229901], _229897))], (614 ^ _206997) ^ [] : [-(leq(n0, 608 ^ [_229897, _229899, _229901]))], (616 ^ _206997) ^ [] : [-(leq(608 ^ [_229897, _229899, _229901], _229897))], (618 ^ _206997) ^ [] : [a_select3(_229899, 607 ^ [_229897, _229899, _229901], 608 ^ [_229897, _229899, _229901]) = a_select3(_229899, 608 ^ [_229897, _229899, _229901], 607 ^ [_229897, _229899, _229901])]], 619 ^ _206997 : [(620 ^ _206997) ^ [_230710, _230712] : [-(a_select3(tptp_mmul(_229901, tptp_mmul(_229899, trans(_229901))), _230712, _230710) = a_select3(tptp_mmul(_229901, tptp_mmul(_229899, trans(_229901))), _230710, _230712)), leq(n0, _230712), leq(_230712, _229897), leq(n0, _230710), leq(_230710, _229897)]]], (638 ^ _206997) ^ [_231329, _231331, _231333, _231335] : [641 ^ _206997 : [(642 ^ _206997) ^ [] : [-(leq(n0, 639 ^ [_231329, _231331, _231333, _231335]))], (644 ^ _206997) ^ [] : [-(leq(639 ^ [_231329, _231331, _231333, _231335], _231329))], (646 ^ _206997) ^ [] : [-(leq(n0, 640 ^ [_231329, _231331, _231333, _231335]))], (648 ^ _206997) ^ [] : [-(leq(640 ^ [_231329, _231331, _231333, _231335], _231329))], (650 ^ _206997) ^ [] : [a_select3(_231333, 639 ^ [_231329, _231331, _231333, _231335], 640 ^ [_231329, _231331, _231333, _231335]) = a_select3(_231333, 640 ^ [_231329, _231331, _231333, _231335], 639 ^ [_231329, _231331, _231333, _231335])]], 651 ^ _206997 : [(652 ^ _206997) ^ [_232186, _232188] : [-(a_select3(tptp_mmul(_231335, tptp_mmul(_231333, trans(_231335))), _232188, _232186) = a_select3(tptp_mmul(_231335, tptp_mmul(_231333, trans(_231335))), _232186, _232188)), leq(n0, _232188), leq(_232188, _231331), leq(n0, _232186), leq(_232186, _231331)]]], (670 ^ _206997) ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895] : [675 ^ _206997 : [(676 ^ _206997) ^ [] : [-(leq(n0, 673 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895]))], (678 ^ _206997) ^ [] : [-(leq(673 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895], _232881))], (680 ^ _206997) ^ [] : [-(leq(n0, 674 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895]))], (682 ^ _206997) ^ [] : [-(leq(674 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895], _232881))], (684 ^ _206997) ^ [] : [a_select3(_232889, 673 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895], 674 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895]) = a_select3(_232889, 674 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895], 673 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895])]], 689 ^ _206997 : [(690 ^ _206997) ^ [] : [-(leq(n0, 687 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895]))], (692 ^ _206997) ^ [] : [-(leq(687 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895], _232883))], (694 ^ _206997) ^ [] : [-(leq(n0, 688 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895]))], (696 ^ _206997) ^ [] : [-(leq(688 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895], _232883))], (698 ^ _206997) ^ [] : [a_select3(_232895, 687 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895], 688 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895]) = a_select3(_232895, 688 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895], 687 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895])]], 701 ^ _206997 : [(702 ^ _206997) ^ [] : [-(leq(n0, 699 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895]))], (704 ^ _206997) ^ [] : [-(leq(699 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895], _232883))], (706 ^ _206997) ^ [] : [-(leq(n0, 700 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895]))], (708 ^ _206997) ^ [] : [-(leq(700 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895], _232883))], (710 ^ _206997) ^ [] : [a_select3(_232885, 699 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895], 700 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895]) = a_select3(_232885, 700 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895], 699 ^ [_232881, _232883, _232885, _232887, _232889, _232891, _232893, _232895])]], 711 ^ _206997 : [(712 ^ _206997) ^ [_235809, _235811] : [-(a_select3(tptp_madd(_232895, tptp_mmul(_232893, tptp_mmul(tptp_madd(tptp_mmul(_232891, tptp_mmul(_232889, trans(_232891))), tptp_mmul(_232887, tptp_mmul(_232885, trans(_232887)))), trans(_232893)))), _235811, _235809) = a_select3(tptp_madd(_232895, tptp_mmul(_232893, tptp_mmul(tptp_madd(tptp_mmul(_232891, tptp_mmul(_232889, trans(_232891))), tptp_mmul(_232887, tptp_mmul(_232885, trans(_232887)))), trans(_232893)))), _235809, _235811)), leq(n0, _235811), leq(_235811, _232883), leq(n0, _235809), leq(_235809, _232883)]]], (730 ^ _206997) ^ [_236562] : [-(sum(n0, tptp_minus_1, _236562) = n0)], (732 ^ _206997) ^ [_236644] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _236644))], (734 ^ _206997) ^ [] : [-(succ(tptp_minus_1) = n0)], (736 ^ _206997) ^ [_236779] : [-(plus(_236779, n1) = succ(_236779))], (738 ^ _206997) ^ [_236862] : [-(plus(n1, _236862) = succ(_236862))], (740 ^ _206997) ^ [_236945] : [-(plus(_236945, n2) = succ(succ(_236945)))], (742 ^ _206997) ^ [_237030] : [-(plus(n2, _237030) = succ(succ(_237030)))], (744 ^ _206997) ^ [_237115] : [-(plus(_237115, n3) = succ(succ(succ(_237115))))], (746 ^ _206997) ^ [_237202] : [-(plus(n3, _237202) = succ(succ(succ(_237202))))], (748 ^ _206997) ^ [_237289] : [-(plus(_237289, n4) = succ(succ(succ(succ(_237289)))))], (750 ^ _206997) ^ [_237378] : [-(plus(n4, _237378) = succ(succ(succ(succ(_237378)))))], (752 ^ _206997) ^ [_237467] : [-(plus(_237467, n5) = succ(succ(succ(succ(succ(_237467))))))], (754 ^ _206997) ^ [_237558] : [-(plus(n5, _237558) = succ(succ(succ(succ(succ(_237558))))))], (756 ^ _206997) ^ [_237649] : [-(minus(_237649, n1) = pred(_237649))], (758 ^ _206997) ^ [_237732] : [-(pred(succ(_237732)) = _237732)], (760 ^ _206997) ^ [_237814] : [-(succ(pred(_237814)) = _237814)], (762 ^ _206997) ^ [_237954, _237956] : [leq(succ(_237956), succ(_237954)), -(leq(_237956, _237954))], (768 ^ _206997) ^ [_238124, _238126] : [leq(_238126, _238124), -(leq(succ(_238126), succ(_238124)))], (774 ^ _206997) ^ [_238344, _238346] : [leq(succ(_238346), _238344), -(gt(_238344, _238346))], (780 ^ _206997) ^ [_238558, _238560] : [leq(minus(_238560, _238558), _238560), -(leq(n0, _238558))], (786 ^ _206997) ^ [_238787, _238789, _238791, _238793] : [-(a_select3(tptp_update3(_238793, _238791, _238789, _238787), _238791, _238789) = _238787)], (788 ^ _206997) ^ [_238979, _238981, _238983, _238985, _238987, _238989, _238991] : [-(a_select3(tptp_update3(_238983, _238991, _238989, _238979), _238987, _238985) = _238981), -(_238991 = _238987), _238989 = _238985, a_select3(_238983, _238987, _238985) = _238981], (802 ^ _206997) ^ [_239522, _239524, _239526, _239528, _239530, _239532] : [-(a_select3(tptp_update3(_239524, _239528, _239526, _239522), _239532, _239530) = _239522), 807 ^ _206997 : [(808 ^ _206997) ^ [] : [-(leq(n0, 805 ^ [_239522, _239524, _239526, _239528, _239530, _239532]))], (810 ^ _206997) ^ [] : [-(leq(n0, 806 ^ [_239522, _239524, _239526, _239528, _239530, _239532]))], (812 ^ _206997) ^ [] : [-(leq(805 ^ [_239522, _239524, _239526, _239528, _239530, _239532], _239528))], (814 ^ _206997) ^ [] : [-(leq(806 ^ [_239522, _239524, _239526, _239528, _239530, _239532], _239526))], (816 ^ _206997) ^ [] : [a_select3(_239524, 805 ^ [_239522, _239524, _239526, _239528, _239530, _239532], 806 ^ [_239522, _239524, _239526, _239528, _239530, _239532]) = _239522]], leq(n0, _239532), leq(_239532, _239528), leq(n0, _239530), leq(_239530, _239526)], (834 ^ _206997) ^ [_240864, _240866, _240868] : [-(a_select2(tptp_update2(_240868, _240866, _240864), _240866) = _240864)], (836 ^ _206997) ^ [_241024, _241026, _241028, _241030, _241032] : [-(a_select2(tptp_update2(_241028, _241032, _241024), _241030) = _241026), -(_241032 = _241030), a_select2(_241028, _241030) = _241026], (865 ^ _206997) ^ [] : [-(true)], (867 ^ _206997) ^ [] : [def = use], (846 ^ _206997) ^ [_241404, _241406, _241408, _241410] : [-(a_select2(tptp_update2(_241406, _241408, _241404), _241410) = _241404), 850 ^ _206997 : [(851 ^ _206997) ^ [] : [-(leq(n0, 849 ^ [_241404, _241406, _241408, _241410]))], (853 ^ _206997) ^ [] : [-(leq(849 ^ [_241404, _241406, _241408, _241410], _241408))], (855 ^ _206997) ^ [] : [a_select2(_241406, 849 ^ [_241404, _241406, _241408, _241410]) = _241404]], leq(n0, _241410), leq(_241410, _241408)]], input).
% 0.34/1.40 ncf('1',plain,[a_select3(center_init, pv65, n0) = init],start(1143 ^ 0)).
% 0.34/1.40 ncf('1.1',plain,[-(a_select3(center_init, pv65, n0) = init), leq(n0, pv65), leq(pv65, n4)],extension(1133 ^ 1,bind([[_249384], [pv65]]))).
% 0.34/1.40 ncf('1.1.1',plain,[-(leq(n0, pv65))],extension(1059 ^ 2)).
% 0.34/1.40 ncf('1.1.2',plain,[-(leq(pv65, n4))],extension(1065 ^ 2)).
% 0.34/1.40 %-----------------------------------------------------
% 0.34/1.40 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------