%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV105+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n002.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:19:59 EDT 2023
% Result : Theorem 0.33s 1.38s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWV105+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n002.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri May 19 02:57:05 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.33/1.38
% 0.33/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.33/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 ncf(matrix, plain, [(1091 ^ _200913) ^ [] : [-(leq(n0, pv43))], (1093 ^ _200913) ^ [] : [-(leq(pv43, minus(n6, n1)))], (1095 ^ _200913) ^ [] : [-(lt(n0, a_select2(sigma, pv43)))], (1097 ^ _200913) ^ [] : [true], (2 ^ _200913) ^ [_201057] : [-(_201057 = _201057)], (4 ^ _200913) ^ [_201164, _201166] : [_201166 = _201164, -(_201164 = _201166)], (10 ^ _200913) ^ [_201368, _201370, _201372] : [-(_201372 = _201368), _201372 = _201370, _201370 = _201368], (20 ^ _200913) ^ [_201709, _201711, _201713, _201715] : [-(geq(_201713, _201709)), geq(_201715, _201711), _201715 = _201713, _201711 = _201709], (34 ^ _200913) ^ [_202153, _202155, _202157, _202159] : [-(gt(_202157, _202153)), gt(_202159, _202155), _202159 = _202157, _202155 = _202153], (48 ^ _200913) ^ [_202597, _202599, _202601, _202603] : [-(leq(_202601, _202597)), leq(_202603, _202599), _202603 = _202601, _202599 = _202597], (62 ^ _200913) ^ [_203021, _203023, _203025, _203027] : [-(lt(_203025, _203021)), lt(_203027, _203023), _203027 = _203025, _203023 = _203021], (76 ^ _200913) ^ [_203477, _203479, _203481, _203483] : [-(uniform_int_rnd(_203483, _203479) = uniform_int_rnd(_203481, _203477)), _203483 = _203481, _203479 = _203477], (86 ^ _200913) ^ [_203836, _203838, _203840, _203842] : [-(tptp_const_array1(_203842, _203838) = tptp_const_array1(_203840, _203836)), _203842 = _203840, _203838 = _203836], (96 ^ _200913) ^ [_204223, _204225, _204227, _204229, _204231, _204233] : [-(tptp_const_array2(_204233, _204229, _204225) = tptp_const_array2(_204231, _204227, _204223)), _204233 = _204231, _204229 = _204227, _204225 = _204223], (110 ^ _200913) ^ [_204711, _204713, _204715, _204717] : [-(dim(_204717, _204713) = dim(_204715, _204711)), _204717 = _204715, _204713 = _204711], (120 ^ _200913) ^ [_205042, _205044] : [_205044 = _205042, -(inv(_205044) = inv(_205042))], (126 ^ _200913) ^ [_205288, _205290, _205292, _205294] : [-(tptp_msub(_205294, _205290) = tptp_msub(_205292, _205288)), _205294 = _205292, _205290 = _205288], (136 ^ _200913) ^ [_205647, _205649, _205651, _205653] : [-(tptp_madd(_205653, _205649) = tptp_madd(_205651, _205647)), _205653 = _205651, _205649 = _205647], (146 ^ _200913) ^ [_206006, _206008, _206010, _206012] : [-(tptp_mmul(_206012, _206008) = tptp_mmul(_206010, _206006)), _206012 = _206010, _206008 = _206006], (156 ^ _200913) ^ [_206337, _206339] : [_206339 = _206337, -(trans(_206339) = trans(_206337))], (162 ^ _200913) ^ [_206611, _206613, _206615, _206617, _206619, _206621] : [-(sum(_206621, _206617, _206613) = sum(_206619, _206615, _206611)), _206621 = _206619, _206617 = _206615, _206613 = _206611], (176 ^ _200913) ^ [_207099, _207101, _207103, _207105] : [-(plus(_207105, _207101) = plus(_207103, _207099)), _207105 = _207103, _207101 = _207099], (186 ^ _200913) ^ [_207430, _207432] : [_207432 = _207430, -(pred(_207432) = pred(_207430))], (192 ^ _200913) ^ [_207704, _207706, _207708, _207710, _207712, _207714] : [-(a_select3(_207714, _207710, _207706) = a_select3(_207712, _207708, _207704)), _207714 = _207712, _207710 = _207708, _207706 = _207704], (206 ^ _200913) ^ [_208248, _208250, _208252, _208254, _208256, _208258, _208260, _208262] : [-(tptp_update3(_208262, _208258, _208254, _208250) = tptp_update3(_208260, _208256, _208252, _208248)), _208262 = _208260, _208258 = _208256, _208254 = _208252, _208250 = _208248], (224 ^ _200913) ^ [_208909, _208911, _208913, _208915, _208917, _208919] : [-(tptp_update2(_208919, _208915, _208911) = tptp_update2(_208917, _208913, _208909)), _208919 = _208917, _208915 = _208913, _208911 = _208909], (238 ^ _200913) ^ [_209369, _209371] : [_209371 = _209369, -(succ(_209371) = succ(_209369))], (244 ^ _200913) ^ [_209615, _209617, _209619, _209621] : [-(minus(_209621, _209617) = minus(_209619, _209615)), _209621 = _209619, _209617 = _209615], (254 ^ _200913) ^ [_209954, _209956, _209958, _209960] : [-(a_select2(_209960, _209956) = a_select2(_209958, _209954)), _209960 = _209958, _209956 = _209954], (869 ^ _200913) ^ [] : [-(gt(n5, n4))], (871 ^ _200913) ^ [] : [-(gt(n6, n4))], (873 ^ _200913) ^ [] : [-(gt(n6, n5))], (875 ^ _200913) ^ [] : [-(gt(n4, tptp_minus_1))], (877 ^ _200913) ^ [] : [-(gt(n5, tptp_minus_1))], (879 ^ _200913) ^ [] : [-(gt(n6, tptp_minus_1))], (881 ^ _200913) ^ [] : [-(gt(n0, tptp_minus_1))], (883 ^ _200913) ^ [] : [-(gt(n1, tptp_minus_1))], (885 ^ _200913) ^ [] : [-(gt(n2, tptp_minus_1))], (887 ^ _200913) ^ [] : [-(gt(n3, tptp_minus_1))], (889 ^ _200913) ^ [] : [-(gt(n4, n0))], (891 ^ _200913) ^ [] : [-(gt(n5, n0))], (893 ^ _200913) ^ [] : [-(gt(n6, n0))], (895 ^ _200913) ^ [] : [-(gt(n1, n0))], (897 ^ _200913) ^ [] : [-(gt(n2, n0))], (899 ^ _200913) ^ [] : [-(gt(n3, n0))], (901 ^ _200913) ^ [] : [-(gt(n4, n1))], (903 ^ _200913) ^ [] : [-(gt(n5, n1))], (905 ^ _200913) ^ [] : [-(gt(n6, n1))], (907 ^ _200913) ^ [] : [-(gt(n2, n1))], (909 ^ _200913) ^ [] : [-(gt(n3, n1))], (911 ^ _200913) ^ [] : [-(gt(n4, n2))], (913 ^ _200913) ^ [] : [-(gt(n5, n2))], (915 ^ _200913) ^ [] : [-(gt(n6, n2))], (917 ^ _200913) ^ [] : [-(gt(n3, n2))], (919 ^ _200913) ^ [] : [-(gt(n4, n3))], (921 ^ _200913) ^ [] : [-(gt(n5, n3))], (923 ^ _200913) ^ [] : [-(gt(n6, n3))], (925 ^ _200913) ^ [_237794] : [leq(n0, _237794), leq(_237794, n4), -(_237794 = n0), -(_237794 = n1), -(_237794 = n2), -(_237794 = n3), -(_237794 = n4)], (951 ^ _200913) ^ [_238415] : [leq(n0, _238415), leq(_238415, n5), -(_238415 = n0), -(_238415 = n1), -(_238415 = n2), -(_238415 = n3), -(_238415 = n4), -(_238415 = n5)], (981 ^ _200913) ^ [_239122] : [leq(n0, _239122), leq(_239122, n6), -(_239122 = n0), -(_239122 = n1), -(_239122 = n2), -(_239122 = n3), -(_239122 = n4), -(_239122 = n5), -(_239122 = n6)], (1015 ^ _200913) ^ [_239915] : [-(_239915 = n0), leq(n0, _239915), leq(_239915, n0)], (1025 ^ _200913) ^ [_240190] : [leq(n0, _240190), leq(_240190, n1), -(_240190 = n0), -(_240190 = n1)], (1039 ^ _200913) ^ [_240553] : [leq(n0, _240553), leq(_240553, n2), -(_240553 = n0), -(_240553 = n1), -(_240553 = n2)], (1079 ^ _200913) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (1081 ^ _200913) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (1083 ^ _200913) ^ [] : [-(succ(succ(succ(succ(succ(succ(n0)))))) = n6)], (1085 ^ _200913) ^ [] : [-(succ(n0) = n1)], (1087 ^ _200913) ^ [] : [-(succ(succ(n0)) = n2)], (1089 ^ _200913) ^ [] : [-(succ(succ(succ(n0))) = n3)], (1057 ^ _200913) ^ [_241002] : [leq(n0, _241002), leq(_241002, n3), -(_241002 = n0), -(_241002 = n1), -(_241002 = n2), -(_241002 = n3)], (264 ^ _200913) ^ [_210385, _210387] : [-(gt(_210387, _210385)), -(gt(_210385, _210387)), -(_210387 = _210385)], (274 ^ _200913) ^ [_210700, _210702, _210704] : [-(gt(_210704, _210700)), gt(_210704, _210702), gt(_210702, _210700)], (284 ^ _200913) ^ [_210979] : [gt(_210979, _210979)], (286 ^ _200913) ^ [_211057] : [-(leq(_211057, _211057))], (288 ^ _200913) ^ [_211178, _211180, _211182] : [-(leq(_211182, _211178)), leq(_211182, _211180), leq(_211180, _211178)], (298 ^ _200913) ^ [_211516, _211518] : [lt(_211518, _211516), -(gt(_211516, _211518))], (304 ^ _200913) ^ [_211678, _211680] : [gt(_211678, _211680), -(lt(_211680, _211678))], (310 ^ _200913) ^ [_211919, _211921] : [geq(_211921, _211919), -(leq(_211919, _211921))], (316 ^ _200913) ^ [_212081, _212083] : [leq(_212081, _212083), -(geq(_212083, _212081))], (322 ^ _200913) ^ [_212293, _212295] : [gt(_212293, _212295), -(leq(_212295, _212293))], (328 ^ _200913) ^ [_212503, _212505] : [-(gt(_212503, _212505)), leq(_212505, _212503), -(_212505 = _212503)], (338 ^ _200913) ^ [_212834, _212836] : [leq(_212836, pred(_212834)), -(gt(_212834, _212836))], (344 ^ _200913) ^ [_213000, _213002] : [gt(_213000, _213002), -(leq(_213002, pred(_213000)))], (350 ^ _200913) ^ [_213187] : [-(gt(succ(_213187), _213187))], (352 ^ _200913) ^ [_213296, _213298] : [leq(_213298, _213296), -(leq(_213298, succ(_213296)))], (358 ^ _200913) ^ [_213539, _213541] : [leq(_213541, _213539), -(gt(succ(_213539), _213541))], (364 ^ _200913) ^ [_213705, _213707] : [gt(succ(_213705), _213707), -(leq(_213707, _213705))], (370 ^ _200913) ^ [_213921, _213923] : [leq(n0, _213923), -(leq(uniform_int_rnd(_213921, _213923), _213923))], (376 ^ _200913) ^ [_214137, _214139] : [leq(n0, _214139), -(leq(n0, uniform_int_rnd(_214137, _214139)))], (382 ^ _200913) ^ [_214381, _214383, _214385, _214387] : [-(a_select2(tptp_const_array1(dim(_214385, _214383), _214381), _214387) = _214381), leq(_214385, _214387), leq(_214387, _214383)], (392 ^ _200913) ^ [_214788, _214790, _214792, _214794, _214796, _214798, _214800] : [-(a_select3(tptp_const_array2(dim(_214798, _214796), dim(_214792, _214790), _214788), _214800, _214794) = _214788), leq(_214798, _214800), leq(_214800, _214796), leq(_214792, _214794), leq(_214794, _214790)], (410 ^ _200913) ^ [_215383, _215385] : [413 ^ _200913 : [(414 ^ _200913) ^ [] : [-(leq(n0, 411 ^ [_215383, _215385]))], (416 ^ _200913) ^ [] : [-(leq(411 ^ [_215383, _215385], _215383))], (418 ^ _200913) ^ [] : [-(leq(n0, 412 ^ [_215383, _215385]))], (420 ^ _200913) ^ [] : [-(leq(412 ^ [_215383, _215385], _215383))], (422 ^ _200913) ^ [] : [a_select3(_215385, 411 ^ [_215383, _215385], 412 ^ [_215383, _215385]) = a_select3(_215385, 412 ^ [_215383, _215385], 411 ^ [_215383, _215385])]], 423 ^ _200913 : [(424 ^ _200913) ^ [_216140, _216142] : [-(a_select3(trans(_215385), _216142, _216140) = a_select3(trans(_215385), _216140, _216142)), leq(n0, _216142), leq(_216142, _215383), leq(n0, _216140), leq(_216140, _215383)]]], (442 ^ _200913) ^ [_216687, _216689] : [445 ^ _200913 : [(446 ^ _200913) ^ [] : [-(leq(n0, 443 ^ [_216687, _216689]))], (448 ^ _200913) ^ [] : [-(leq(443 ^ [_216687, _216689], _216687))], (450 ^ _200913) ^ [] : [-(leq(n0, 444 ^ [_216687, _216689]))], (452 ^ _200913) ^ [] : [-(leq(444 ^ [_216687, _216689], _216687))], (454 ^ _200913) ^ [] : [a_select3(_216689, 443 ^ [_216687, _216689], 444 ^ [_216687, _216689]) = a_select3(_216689, 444 ^ [_216687, _216689], 443 ^ [_216687, _216689])]], 455 ^ _200913 : [(456 ^ _200913) ^ [_217444, _217446] : [-(a_select3(inv(_216689), _217446, _217444) = a_select3(inv(_216689), _217444, _217446)), leq(n0, _217446), leq(_217446, _216687), leq(n0, _217444), leq(_217444, _216687)]]], (474 ^ _200913) ^ [_217991, _217993] : [477 ^ _200913 : [(478 ^ _200913) ^ [] : [-(leq(n0, 475 ^ [_217991, _217993]))], (480 ^ _200913) ^ [] : [-(leq(475 ^ [_217991, _217993], _217991))], (482 ^ _200913) ^ [] : [-(leq(n0, 476 ^ [_217991, _217993]))], (484 ^ _200913) ^ [] : [-(leq(476 ^ [_217991, _217993], _217991))], (486 ^ _200913) ^ [] : [a_select3(_217993, 475 ^ [_217991, _217993], 476 ^ [_217991, _217993]) = a_select3(_217993, 476 ^ [_217991, _217993], 475 ^ [_217991, _217993])]], 487 ^ _200913 : [(488 ^ _200913) ^ [_218804, _218806, _218808, _218810] : [-(a_select3(tptp_update3(_217993, _218806, _218806, _218804), _218810, _218808) = a_select3(tptp_update3(_217993, _218806, _218806, _218804), _218808, _218810)), leq(n0, _218810), leq(_218810, _217991), leq(n0, _218808), leq(_218808, _217991), leq(n0, _218806), leq(_218806, _217991)]]], (514 ^ _200913) ^ [_219623, _219625, _219627] : [519 ^ _200913 : [(520 ^ _200913) ^ [] : [-(leq(n0, 517 ^ [_219623, _219625, _219627]))], (522 ^ _200913) ^ [] : [-(leq(517 ^ [_219623, _219625, _219627], _219623))], (524 ^ _200913) ^ [] : [-(leq(n0, 518 ^ [_219623, _219625, _219627]))], (526 ^ _200913) ^ [] : [-(leq(518 ^ [_219623, _219625, _219627], _219623))], (528 ^ _200913) ^ [] : [a_select3(_219627, 517 ^ [_219623, _219625, _219627], 518 ^ [_219623, _219625, _219627]) = a_select3(_219627, 518 ^ [_219623, _219625, _219627], 517 ^ [_219623, _219625, _219627])]], 531 ^ _200913 : [(532 ^ _200913) ^ [] : [-(leq(n0, 529 ^ [_219623, _219625, _219627]))], (534 ^ _200913) ^ [] : [-(leq(529 ^ [_219623, _219625, _219627], _219623))], (536 ^ _200913) ^ [] : [-(leq(n0, 530 ^ [_219623, _219625, _219627]))], (538 ^ _200913) ^ [] : [-(leq(530 ^ [_219623, _219625, _219627], _219623))], (540 ^ _200913) ^ [] : [a_select3(_219625, 529 ^ [_219623, _219625, _219627], 530 ^ [_219623, _219625, _219627]) = a_select3(_219625, 530 ^ [_219623, _219625, _219627], 529 ^ [_219623, _219625, _219627])]], 541 ^ _200913 : [(542 ^ _200913) ^ [_221132, _221134] : [-(a_select3(tptp_madd(_219627, _219625), _221134, _221132) = a_select3(tptp_madd(_219627, _219625), _221132, _221134)), leq(n0, _221134), leq(_221134, _219623), leq(n0, _221132), leq(_221132, _219623)]]], (560 ^ _200913) ^ [_221718, _221720, _221722] : [565 ^ _200913 : [(566 ^ _200913) ^ [] : [-(leq(n0, 563 ^ [_221718, _221720, _221722]))], (568 ^ _200913) ^ [] : [-(leq(563 ^ [_221718, _221720, _221722], _221718))], (570 ^ _200913) ^ [] : [-(leq(n0, 564 ^ [_221718, _221720, _221722]))], (572 ^ _200913) ^ [] : [-(leq(564 ^ [_221718, _221720, _221722], _221718))], (574 ^ _200913) ^ [] : [a_select3(_221722, 563 ^ [_221718, _221720, _221722], 564 ^ [_221718, _221720, _221722]) = a_select3(_221722, 564 ^ [_221718, _221720, _221722], 563 ^ [_221718, _221720, _221722])]], 577 ^ _200913 : [(578 ^ _200913) ^ [] : [-(leq(n0, 575 ^ [_221718, _221720, _221722]))], (580 ^ _200913) ^ [] : [-(leq(575 ^ [_221718, _221720, _221722], _221718))], (582 ^ _200913) ^ [] : [-(leq(n0, 576 ^ [_221718, _221720, _221722]))], (584 ^ _200913) ^ [] : [-(leq(576 ^ [_221718, _221720, _221722], _221718))], (586 ^ _200913) ^ [] : [a_select3(_221720, 575 ^ [_221718, _221720, _221722], 576 ^ [_221718, _221720, _221722]) = a_select3(_221720, 576 ^ [_221718, _221720, _221722], 575 ^ [_221718, _221720, _221722])]], 587 ^ _200913 : [(588 ^ _200913) ^ [_223227, _223229] : [-(a_select3(tptp_msub(_221722, _221720), _223229, _223227) = a_select3(tptp_msub(_221722, _221720), _223227, _223229)), leq(n0, _223229), leq(_223229, _221718), leq(n0, _223227), leq(_223227, _221718)]]], (606 ^ _200913) ^ [_223813, _223815, _223817] : [609 ^ _200913 : [(610 ^ _200913) ^ [] : [-(leq(n0, 607 ^ [_223813, _223815, _223817]))], (612 ^ _200913) ^ [] : [-(leq(607 ^ [_223813, _223815, _223817], _223813))], (614 ^ _200913) ^ [] : [-(leq(n0, 608 ^ [_223813, _223815, _223817]))], (616 ^ _200913) ^ [] : [-(leq(608 ^ [_223813, _223815, _223817], _223813))], (618 ^ _200913) ^ [] : [a_select3(_223815, 607 ^ [_223813, _223815, _223817], 608 ^ [_223813, _223815, _223817]) = a_select3(_223815, 608 ^ [_223813, _223815, _223817], 607 ^ [_223813, _223815, _223817])]], 619 ^ _200913 : [(620 ^ _200913) ^ [_224626, _224628] : [-(a_select3(tptp_mmul(_223817, tptp_mmul(_223815, trans(_223817))), _224628, _224626) = a_select3(tptp_mmul(_223817, tptp_mmul(_223815, trans(_223817))), _224626, _224628)), leq(n0, _224628), leq(_224628, _223813), leq(n0, _224626), leq(_224626, _223813)]]], (638 ^ _200913) ^ [_225245, _225247, _225249, _225251] : [641 ^ _200913 : [(642 ^ _200913) ^ [] : [-(leq(n0, 639 ^ [_225245, _225247, _225249, _225251]))], (644 ^ _200913) ^ [] : [-(leq(639 ^ [_225245, _225247, _225249, _225251], _225245))], (646 ^ _200913) ^ [] : [-(leq(n0, 640 ^ [_225245, _225247, _225249, _225251]))], (648 ^ _200913) ^ [] : [-(leq(640 ^ [_225245, _225247, _225249, _225251], _225245))], (650 ^ _200913) ^ [] : [a_select3(_225249, 639 ^ [_225245, _225247, _225249, _225251], 640 ^ [_225245, _225247, _225249, _225251]) = a_select3(_225249, 640 ^ [_225245, _225247, _225249, _225251], 639 ^ [_225245, _225247, _225249, _225251])]], 651 ^ _200913 : [(652 ^ _200913) ^ [_226102, _226104] : [-(a_select3(tptp_mmul(_225251, tptp_mmul(_225249, trans(_225251))), _226104, _226102) = a_select3(tptp_mmul(_225251, tptp_mmul(_225249, trans(_225251))), _226102, _226104)), leq(n0, _226104), leq(_226104, _225247), leq(n0, _226102), leq(_226102, _225247)]]], (670 ^ _200913) ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811] : [675 ^ _200913 : [(676 ^ _200913) ^ [] : [-(leq(n0, 673 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811]))], (678 ^ _200913) ^ [] : [-(leq(673 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811], _226797))], (680 ^ _200913) ^ [] : [-(leq(n0, 674 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811]))], (682 ^ _200913) ^ [] : [-(leq(674 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811], _226797))], (684 ^ _200913) ^ [] : [a_select3(_226805, 673 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811], 674 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811]) = a_select3(_226805, 674 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811], 673 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811])]], 689 ^ _200913 : [(690 ^ _200913) ^ [] : [-(leq(n0, 687 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811]))], (692 ^ _200913) ^ [] : [-(leq(687 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811], _226799))], (694 ^ _200913) ^ [] : [-(leq(n0, 688 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811]))], (696 ^ _200913) ^ [] : [-(leq(688 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811], _226799))], (698 ^ _200913) ^ [] : [a_select3(_226811, 687 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811], 688 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811]) = a_select3(_226811, 688 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811], 687 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811])]], 701 ^ _200913 : [(702 ^ _200913) ^ [] : [-(leq(n0, 699 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811]))], (704 ^ _200913) ^ [] : [-(leq(699 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811], _226799))], (706 ^ _200913) ^ [] : [-(leq(n0, 700 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811]))], (708 ^ _200913) ^ [] : [-(leq(700 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811], _226799))], (710 ^ _200913) ^ [] : [a_select3(_226801, 699 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811], 700 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811]) = a_select3(_226801, 700 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811], 699 ^ [_226797, _226799, _226801, _226803, _226805, _226807, _226809, _226811])]], 711 ^ _200913 : [(712 ^ _200913) ^ [_229725, _229727] : [-(a_select3(tptp_madd(_226811, tptp_mmul(_226809, tptp_mmul(tptp_madd(tptp_mmul(_226807, tptp_mmul(_226805, trans(_226807))), tptp_mmul(_226803, tptp_mmul(_226801, trans(_226803)))), trans(_226809)))), _229727, _229725) = a_select3(tptp_madd(_226811, tptp_mmul(_226809, tptp_mmul(tptp_madd(tptp_mmul(_226807, tptp_mmul(_226805, trans(_226807))), tptp_mmul(_226803, tptp_mmul(_226801, trans(_226803)))), trans(_226809)))), _229725, _229727)), leq(n0, _229727), leq(_229727, _226799), leq(n0, _229725), leq(_229725, _226799)]]], (730 ^ _200913) ^ [_230478] : [-(sum(n0, tptp_minus_1, _230478) = n0)], (732 ^ _200913) ^ [_230560] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _230560))], (734 ^ _200913) ^ [] : [-(succ(tptp_minus_1) = n0)], (736 ^ _200913) ^ [_230695] : [-(plus(_230695, n1) = succ(_230695))], (738 ^ _200913) ^ [_230778] : [-(plus(n1, _230778) = succ(_230778))], (740 ^ _200913) ^ [_230861] : [-(plus(_230861, n2) = succ(succ(_230861)))], (742 ^ _200913) ^ [_230946] : [-(plus(n2, _230946) = succ(succ(_230946)))], (744 ^ _200913) ^ [_231031] : [-(plus(_231031, n3) = succ(succ(succ(_231031))))], (746 ^ _200913) ^ [_231118] : [-(plus(n3, _231118) = succ(succ(succ(_231118))))], (748 ^ _200913) ^ [_231205] : [-(plus(_231205, n4) = succ(succ(succ(succ(_231205)))))], (750 ^ _200913) ^ [_231294] : [-(plus(n4, _231294) = succ(succ(succ(succ(_231294)))))], (752 ^ _200913) ^ [_231383] : [-(plus(_231383, n5) = succ(succ(succ(succ(succ(_231383))))))], (754 ^ _200913) ^ [_231474] : [-(plus(n5, _231474) = succ(succ(succ(succ(succ(_231474))))))], (756 ^ _200913) ^ [_231565] : [-(minus(_231565, n1) = pred(_231565))], (758 ^ _200913) ^ [_231648] : [-(pred(succ(_231648)) = _231648)], (760 ^ _200913) ^ [_231730] : [-(succ(pred(_231730)) = _231730)], (762 ^ _200913) ^ [_231870, _231872] : [leq(succ(_231872), succ(_231870)), -(leq(_231872, _231870))], (768 ^ _200913) ^ [_232040, _232042] : [leq(_232042, _232040), -(leq(succ(_232042), succ(_232040)))], (774 ^ _200913) ^ [_232260, _232262] : [leq(succ(_232262), _232260), -(gt(_232260, _232262))], (780 ^ _200913) ^ [_232474, _232476] : [leq(minus(_232476, _232474), _232476), -(leq(n0, _232474))], (786 ^ _200913) ^ [_232703, _232705, _232707, _232709] : [-(a_select3(tptp_update3(_232709, _232707, _232705, _232703), _232707, _232705) = _232703)], (788 ^ _200913) ^ [_232895, _232897, _232899, _232901, _232903, _232905, _232907] : [-(a_select3(tptp_update3(_232899, _232907, _232905, _232895), _232903, _232901) = _232897), -(_232907 = _232903), _232905 = _232901, a_select3(_232899, _232903, _232901) = _232897], (802 ^ _200913) ^ [_233438, _233440, _233442, _233444, _233446, _233448] : [-(a_select3(tptp_update3(_233440, _233444, _233442, _233438), _233448, _233446) = _233438), 807 ^ _200913 : [(808 ^ _200913) ^ [] : [-(leq(n0, 805 ^ [_233438, _233440, _233442, _233444, _233446, _233448]))], (810 ^ _200913) ^ [] : [-(leq(n0, 806 ^ [_233438, _233440, _233442, _233444, _233446, _233448]))], (812 ^ _200913) ^ [] : [-(leq(805 ^ [_233438, _233440, _233442, _233444, _233446, _233448], _233444))], (814 ^ _200913) ^ [] : [-(leq(806 ^ [_233438, _233440, _233442, _233444, _233446, _233448], _233442))], (816 ^ _200913) ^ [] : [a_select3(_233440, 805 ^ [_233438, _233440, _233442, _233444, _233446, _233448], 806 ^ [_233438, _233440, _233442, _233444, _233446, _233448]) = _233438]], leq(n0, _233448), leq(_233448, _233444), leq(n0, _233446), leq(_233446, _233442)], (834 ^ _200913) ^ [_234780, _234782, _234784] : [-(a_select2(tptp_update2(_234784, _234782, _234780), _234782) = _234780)], (836 ^ _200913) ^ [_234940, _234942, _234944, _234946, _234948] : [-(a_select2(tptp_update2(_234944, _234948, _234940), _234946) = _234942), -(_234948 = _234946), a_select2(_234944, _234946) = _234942], (865 ^ _200913) ^ [] : [-(true)], (867 ^ _200913) ^ [] : [def = use], (846 ^ _200913) ^ [_235320, _235322, _235324, _235326] : [-(a_select2(tptp_update2(_235322, _235324, _235320), _235326) = _235320), 850 ^ _200913 : [(851 ^ _200913) ^ [] : [-(leq(n0, 849 ^ [_235320, _235322, _235324, _235326]))], (853 ^ _200913) ^ [] : [-(leq(849 ^ [_235320, _235322, _235324, _235326], _235324))], (855 ^ _200913) ^ [] : [a_select2(_235322, 849 ^ [_235320, _235322, _235324, _235326]) = _235320]], leq(n0, _235326), leq(_235326, _235324)]], input).
% 0.33/1.38 ncf('1',plain,[true],start(1097 ^ 0)).
% 0.33/1.38 ncf('1.1',plain,[-(true)],extension(865 ^ 1)).
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------