%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV065+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:19:52 EDT 2023
% Result : Theorem 0.33s 1.37s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.11 % Problem : SWV065+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.02/0.11 % Command : nanocop.sh %s %d
% 0.11/0.32 % Computer : n008.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Fri May 19 02:32:54 EDT 2023
% 0.11/0.32 % CPUTime :
% 0.33/1.37
% 0.33/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.33/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 ncf(matrix, plain, [(1055 ^ _199127) ^ [] : [-(leq(n0, pv10))], (1057 ^ _199127) ^ [] : [-(leq(n0, pv53))], (1059 ^ _199127) ^ [] : [-(leq(pv10, minus(n135300, n1)))], (1061 ^ _199127) ^ [] : [-(leq(pv53, minus(n5, n1)))], (1063 ^ _199127) ^ [] : [leq(n0, n0), leq(n0, pv10), leq(n0, pv53), leq(pv10, minus(n135300, n1)), leq(pv53, minus(n5, n1))], (2 ^ _199127) ^ [_199271] : [-(_199271 = _199271)], (4 ^ _199127) ^ [_199378, _199380] : [_199380 = _199378, -(_199378 = _199380)], (10 ^ _199127) ^ [_199582, _199584, _199586] : [-(_199586 = _199582), _199586 = _199584, _199584 = _199582], (20 ^ _199127) ^ [_199923, _199925, _199927, _199929] : [-(lt(_199927, _199923)), lt(_199929, _199925), _199929 = _199927, _199925 = _199923], (34 ^ _199127) ^ [_200367, _200369, _200371, _200373] : [-(geq(_200371, _200367)), geq(_200373, _200369), _200373 = _200371, _200369 = _200367], (48 ^ _199127) ^ [_200811, _200813, _200815, _200817] : [-(gt(_200815, _200811)), gt(_200817, _200813), _200817 = _200815, _200813 = _200811], (62 ^ _199127) ^ [_201235, _201237, _201239, _201241] : [-(leq(_201239, _201235)), leq(_201241, _201237), _201241 = _201239, _201237 = _201235], (76 ^ _199127) ^ [_201691, _201693, _201695, _201697] : [-(uniform_int_rnd(_201697, _201693) = uniform_int_rnd(_201695, _201691)), _201697 = _201695, _201693 = _201691], (86 ^ _199127) ^ [_202050, _202052, _202054, _202056] : [-(tptp_const_array1(_202056, _202052) = tptp_const_array1(_202054, _202050)), _202056 = _202054, _202052 = _202050], (96 ^ _199127) ^ [_202437, _202439, _202441, _202443, _202445, _202447] : [-(tptp_const_array2(_202447, _202443, _202439) = tptp_const_array2(_202445, _202441, _202437)), _202447 = _202445, _202443 = _202441, _202439 = _202437], (110 ^ _199127) ^ [_202925, _202927, _202929, _202931] : [-(dim(_202931, _202927) = dim(_202929, _202925)), _202931 = _202929, _202927 = _202925], (120 ^ _199127) ^ [_203256, _203258] : [_203258 = _203256, -(inv(_203258) = inv(_203256))], (126 ^ _199127) ^ [_203502, _203504, _203506, _203508] : [-(tptp_msub(_203508, _203504) = tptp_msub(_203506, _203502)), _203508 = _203506, _203504 = _203502], (136 ^ _199127) ^ [_203861, _203863, _203865, _203867] : [-(tptp_madd(_203867, _203863) = tptp_madd(_203865, _203861)), _203867 = _203865, _203863 = _203861], (146 ^ _199127) ^ [_204220, _204222, _204224, _204226] : [-(tptp_mmul(_204226, _204222) = tptp_mmul(_204224, _204220)), _204226 = _204224, _204222 = _204220], (156 ^ _199127) ^ [_204551, _204553] : [_204553 = _204551, -(trans(_204553) = trans(_204551))], (162 ^ _199127) ^ [_204825, _204827, _204829, _204831, _204833, _204835] : [-(sum(_204835, _204831, _204827) = sum(_204833, _204829, _204825)), _204835 = _204833, _204831 = _204829, _204827 = _204825], (176 ^ _199127) ^ [_205313, _205315, _205317, _205319] : [-(plus(_205319, _205315) = plus(_205317, _205313)), _205319 = _205317, _205315 = _205313], (186 ^ _199127) ^ [_205644, _205646] : [_205646 = _205644, -(pred(_205646) = pred(_205644))], (192 ^ _199127) ^ [_205918, _205920, _205922, _205924, _205926, _205928] : [-(a_select3(_205928, _205924, _205920) = a_select3(_205926, _205922, _205918)), _205928 = _205926, _205924 = _205922, _205920 = _205918], (206 ^ _199127) ^ [_206462, _206464, _206466, _206468, _206470, _206472, _206474, _206476] : [-(tptp_update3(_206476, _206472, _206468, _206464) = tptp_update3(_206474, _206470, _206466, _206462)), _206476 = _206474, _206472 = _206470, _206468 = _206466, _206464 = _206462], (224 ^ _199127) ^ [_207095, _207097, _207099, _207101] : [-(a_select2(_207101, _207097) = a_select2(_207099, _207095)), _207101 = _207099, _207097 = _207095], (234 ^ _199127) ^ [_207482, _207484, _207486, _207488, _207490, _207492] : [-(tptp_update2(_207492, _207488, _207484) = tptp_update2(_207490, _207486, _207482)), _207492 = _207490, _207488 = _207486, _207484 = _207482], (248 ^ _199127) ^ [_207942, _207944] : [_207944 = _207942, -(succ(_207944) = succ(_207942))], (254 ^ _199127) ^ [_208168, _208170, _208172, _208174] : [-(minus(_208174, _208170) = minus(_208172, _208168)), _208174 = _208172, _208170 = _208168], (869 ^ _199127) ^ [] : [-(gt(n5, n4))], (871 ^ _199127) ^ [] : [-(gt(n135300, n4))], (873 ^ _199127) ^ [] : [-(gt(n135300, n5))], (875 ^ _199127) ^ [] : [-(gt(n4, tptp_minus_1))], (877 ^ _199127) ^ [] : [-(gt(n5, tptp_minus_1))], (879 ^ _199127) ^ [] : [-(gt(n135300, tptp_minus_1))], (881 ^ _199127) ^ [] : [-(gt(n0, tptp_minus_1))], (883 ^ _199127) ^ [] : [-(gt(n1, tptp_minus_1))], (885 ^ _199127) ^ [] : [-(gt(n2, tptp_minus_1))], (887 ^ _199127) ^ [] : [-(gt(n3, tptp_minus_1))], (889 ^ _199127) ^ [] : [-(gt(n4, n0))], (891 ^ _199127) ^ [] : [-(gt(n5, n0))], (893 ^ _199127) ^ [] : [-(gt(n135300, n0))], (895 ^ _199127) ^ [] : [-(gt(n1, n0))], (897 ^ _199127) ^ [] : [-(gt(n2, n0))], (899 ^ _199127) ^ [] : [-(gt(n3, n0))], (901 ^ _199127) ^ [] : [-(gt(n4, n1))], (903 ^ _199127) ^ [] : [-(gt(n5, n1))], (905 ^ _199127) ^ [] : [-(gt(n135300, n1))], (907 ^ _199127) ^ [] : [-(gt(n2, n1))], (909 ^ _199127) ^ [] : [-(gt(n3, n1))], (911 ^ _199127) ^ [] : [-(gt(n4, n2))], (913 ^ _199127) ^ [] : [-(gt(n5, n2))], (915 ^ _199127) ^ [] : [-(gt(n135300, n2))], (917 ^ _199127) ^ [] : [-(gt(n3, n2))], (919 ^ _199127) ^ [] : [-(gt(n4, n3))], (921 ^ _199127) ^ [] : [-(gt(n5, n3))], (923 ^ _199127) ^ [] : [-(gt(n135300, n3))], (925 ^ _199127) ^ [_236008] : [leq(n0, _236008), leq(_236008, n4), -(_236008 = n0), -(_236008 = n1), -(_236008 = n2), -(_236008 = n3), -(_236008 = n4)], (951 ^ _199127) ^ [_236629] : [leq(n0, _236629), leq(_236629, n5), -(_236629 = n0), -(_236629 = n1), -(_236629 = n2), -(_236629 = n3), -(_236629 = n4), -(_236629 = n5)], (981 ^ _199127) ^ [_237336] : [-(_237336 = n0), leq(n0, _237336), leq(_237336, n0)], (991 ^ _199127) ^ [_237611] : [leq(n0, _237611), leq(_237611, n1), -(_237611 = n0), -(_237611 = n1)], (1005 ^ _199127) ^ [_237974] : [leq(n0, _237974), leq(_237974, n2), -(_237974 = n0), -(_237974 = n1), -(_237974 = n2)], (1045 ^ _199127) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (1047 ^ _199127) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (1049 ^ _199127) ^ [] : [-(succ(n0) = n1)], (1051 ^ _199127) ^ [] : [-(succ(succ(n0)) = n2)], (1053 ^ _199127) ^ [] : [-(succ(succ(succ(n0))) = n3)], (1023 ^ _199127) ^ [_238423] : [leq(n0, _238423), leq(_238423, n3), -(_238423 = n0), -(_238423 = n1), -(_238423 = n2), -(_238423 = n3)], (264 ^ _199127) ^ [_208599, _208601] : [-(gt(_208601, _208599)), -(gt(_208599, _208601)), -(_208601 = _208599)], (274 ^ _199127) ^ [_208914, _208916, _208918] : [-(gt(_208918, _208914)), gt(_208918, _208916), gt(_208916, _208914)], (284 ^ _199127) ^ [_209193] : [gt(_209193, _209193)], (286 ^ _199127) ^ [_209271] : [-(leq(_209271, _209271))], (288 ^ _199127) ^ [_209392, _209394, _209396] : [-(leq(_209396, _209392)), leq(_209396, _209394), leq(_209394, _209392)], (298 ^ _199127) ^ [_209730, _209732] : [lt(_209732, _209730), -(gt(_209730, _209732))], (304 ^ _199127) ^ [_209892, _209894] : [gt(_209892, _209894), -(lt(_209894, _209892))], (310 ^ _199127) ^ [_210133, _210135] : [geq(_210135, _210133), -(leq(_210133, _210135))], (316 ^ _199127) ^ [_210295, _210297] : [leq(_210295, _210297), -(geq(_210297, _210295))], (322 ^ _199127) ^ [_210507, _210509] : [gt(_210507, _210509), -(leq(_210509, _210507))], (328 ^ _199127) ^ [_210717, _210719] : [-(gt(_210717, _210719)), leq(_210719, _210717), -(_210719 = _210717)], (338 ^ _199127) ^ [_211048, _211050] : [leq(_211050, pred(_211048)), -(gt(_211048, _211050))], (344 ^ _199127) ^ [_211214, _211216] : [gt(_211214, _211216), -(leq(_211216, pred(_211214)))], (350 ^ _199127) ^ [_211401] : [-(gt(succ(_211401), _211401))], (352 ^ _199127) ^ [_211510, _211512] : [leq(_211512, _211510), -(leq(_211512, succ(_211510)))], (358 ^ _199127) ^ [_211753, _211755] : [leq(_211755, _211753), -(gt(succ(_211753), _211755))], (364 ^ _199127) ^ [_211919, _211921] : [gt(succ(_211919), _211921), -(leq(_211921, _211919))], (370 ^ _199127) ^ [_212135, _212137] : [leq(n0, _212137), -(leq(uniform_int_rnd(_212135, _212137), _212137))], (376 ^ _199127) ^ [_212351, _212353] : [leq(n0, _212353), -(leq(n0, uniform_int_rnd(_212351, _212353)))], (382 ^ _199127) ^ [_212595, _212597, _212599, _212601] : [-(a_select2(tptp_const_array1(dim(_212599, _212597), _212595), _212601) = _212595), leq(_212599, _212601), leq(_212601, _212597)], (392 ^ _199127) ^ [_213002, _213004, _213006, _213008, _213010, _213012, _213014] : [-(a_select3(tptp_const_array2(dim(_213012, _213010), dim(_213006, _213004), _213002), _213014, _213008) = _213002), leq(_213012, _213014), leq(_213014, _213010), leq(_213006, _213008), leq(_213008, _213004)], (410 ^ _199127) ^ [_213597, _213599] : [413 ^ _199127 : [(414 ^ _199127) ^ [] : [-(leq(n0, 411 ^ [_213597, _213599]))], (416 ^ _199127) ^ [] : [-(leq(411 ^ [_213597, _213599], _213597))], (418 ^ _199127) ^ [] : [-(leq(n0, 412 ^ [_213597, _213599]))], (420 ^ _199127) ^ [] : [-(leq(412 ^ [_213597, _213599], _213597))], (422 ^ _199127) ^ [] : [a_select3(_213599, 411 ^ [_213597, _213599], 412 ^ [_213597, _213599]) = a_select3(_213599, 412 ^ [_213597, _213599], 411 ^ [_213597, _213599])]], 423 ^ _199127 : [(424 ^ _199127) ^ [_214354, _214356] : [-(a_select3(trans(_213599), _214356, _214354) = a_select3(trans(_213599), _214354, _214356)), leq(n0, _214356), leq(_214356, _213597), leq(n0, _214354), leq(_214354, _213597)]]], (442 ^ _199127) ^ [_214901, _214903] : [445 ^ _199127 : [(446 ^ _199127) ^ [] : [-(leq(n0, 443 ^ [_214901, _214903]))], (448 ^ _199127) ^ [] : [-(leq(443 ^ [_214901, _214903], _214901))], (450 ^ _199127) ^ [] : [-(leq(n0, 444 ^ [_214901, _214903]))], (452 ^ _199127) ^ [] : [-(leq(444 ^ [_214901, _214903], _214901))], (454 ^ _199127) ^ [] : [a_select3(_214903, 443 ^ [_214901, _214903], 444 ^ [_214901, _214903]) = a_select3(_214903, 444 ^ [_214901, _214903], 443 ^ [_214901, _214903])]], 455 ^ _199127 : [(456 ^ _199127) ^ [_215658, _215660] : [-(a_select3(inv(_214903), _215660, _215658) = a_select3(inv(_214903), _215658, _215660)), leq(n0, _215660), leq(_215660, _214901), leq(n0, _215658), leq(_215658, _214901)]]], (474 ^ _199127) ^ [_216205, _216207] : [477 ^ _199127 : [(478 ^ _199127) ^ [] : [-(leq(n0, 475 ^ [_216205, _216207]))], (480 ^ _199127) ^ [] : [-(leq(475 ^ [_216205, _216207], _216205))], (482 ^ _199127) ^ [] : [-(leq(n0, 476 ^ [_216205, _216207]))], (484 ^ _199127) ^ [] : [-(leq(476 ^ [_216205, _216207], _216205))], (486 ^ _199127) ^ [] : [a_select3(_216207, 475 ^ [_216205, _216207], 476 ^ [_216205, _216207]) = a_select3(_216207, 476 ^ [_216205, _216207], 475 ^ [_216205, _216207])]], 487 ^ _199127 : [(488 ^ _199127) ^ [_217018, _217020, _217022, _217024] : [-(a_select3(tptp_update3(_216207, _217020, _217020, _217018), _217024, _217022) = a_select3(tptp_update3(_216207, _217020, _217020, _217018), _217022, _217024)), leq(n0, _217024), leq(_217024, _216205), leq(n0, _217022), leq(_217022, _216205), leq(n0, _217020), leq(_217020, _216205)]]], (514 ^ _199127) ^ [_217837, _217839, _217841] : [519 ^ _199127 : [(520 ^ _199127) ^ [] : [-(leq(n0, 517 ^ [_217837, _217839, _217841]))], (522 ^ _199127) ^ [] : [-(leq(517 ^ [_217837, _217839, _217841], _217837))], (524 ^ _199127) ^ [] : [-(leq(n0, 518 ^ [_217837, _217839, _217841]))], (526 ^ _199127) ^ [] : [-(leq(518 ^ [_217837, _217839, _217841], _217837))], (528 ^ _199127) ^ [] : [a_select3(_217841, 517 ^ [_217837, _217839, _217841], 518 ^ [_217837, _217839, _217841]) = a_select3(_217841, 518 ^ [_217837, _217839, _217841], 517 ^ [_217837, _217839, _217841])]], 531 ^ _199127 : [(532 ^ _199127) ^ [] : [-(leq(n0, 529 ^ [_217837, _217839, _217841]))], (534 ^ _199127) ^ [] : [-(leq(529 ^ [_217837, _217839, _217841], _217837))], (536 ^ _199127) ^ [] : [-(leq(n0, 530 ^ [_217837, _217839, _217841]))], (538 ^ _199127) ^ [] : [-(leq(530 ^ [_217837, _217839, _217841], _217837))], (540 ^ _199127) ^ [] : [a_select3(_217839, 529 ^ [_217837, _217839, _217841], 530 ^ [_217837, _217839, _217841]) = a_select3(_217839, 530 ^ [_217837, _217839, _217841], 529 ^ [_217837, _217839, _217841])]], 541 ^ _199127 : [(542 ^ _199127) ^ [_219346, _219348] : [-(a_select3(tptp_madd(_217841, _217839), _219348, _219346) = a_select3(tptp_madd(_217841, _217839), _219346, _219348)), leq(n0, _219348), leq(_219348, _217837), leq(n0, _219346), leq(_219346, _217837)]]], (560 ^ _199127) ^ [_219932, _219934, _219936] : [565 ^ _199127 : [(566 ^ _199127) ^ [] : [-(leq(n0, 563 ^ [_219932, _219934, _219936]))], (568 ^ _199127) ^ [] : [-(leq(563 ^ [_219932, _219934, _219936], _219932))], (570 ^ _199127) ^ [] : [-(leq(n0, 564 ^ [_219932, _219934, _219936]))], (572 ^ _199127) ^ [] : [-(leq(564 ^ [_219932, _219934, _219936], _219932))], (574 ^ _199127) ^ [] : [a_select3(_219936, 563 ^ [_219932, _219934, _219936], 564 ^ [_219932, _219934, _219936]) = a_select3(_219936, 564 ^ [_219932, _219934, _219936], 563 ^ [_219932, _219934, _219936])]], 577 ^ _199127 : [(578 ^ _199127) ^ [] : [-(leq(n0, 575 ^ [_219932, _219934, _219936]))], (580 ^ _199127) ^ [] : [-(leq(575 ^ [_219932, _219934, _219936], _219932))], (582 ^ _199127) ^ [] : [-(leq(n0, 576 ^ [_219932, _219934, _219936]))], (584 ^ _199127) ^ [] : [-(leq(576 ^ [_219932, _219934, _219936], _219932))], (586 ^ _199127) ^ [] : [a_select3(_219934, 575 ^ [_219932, _219934, _219936], 576 ^ [_219932, _219934, _219936]) = a_select3(_219934, 576 ^ [_219932, _219934, _219936], 575 ^ [_219932, _219934, _219936])]], 587 ^ _199127 : [(588 ^ _199127) ^ [_221441, _221443] : [-(a_select3(tptp_msub(_219936, _219934), _221443, _221441) = a_select3(tptp_msub(_219936, _219934), _221441, _221443)), leq(n0, _221443), leq(_221443, _219932), leq(n0, _221441), leq(_221441, _219932)]]], (606 ^ _199127) ^ [_222027, _222029, _222031] : [609 ^ _199127 : [(610 ^ _199127) ^ [] : [-(leq(n0, 607 ^ [_222027, _222029, _222031]))], (612 ^ _199127) ^ [] : [-(leq(607 ^ [_222027, _222029, _222031], _222027))], (614 ^ _199127) ^ [] : [-(leq(n0, 608 ^ [_222027, _222029, _222031]))], (616 ^ _199127) ^ [] : [-(leq(608 ^ [_222027, _222029, _222031], _222027))], (618 ^ _199127) ^ [] : [a_select3(_222029, 607 ^ [_222027, _222029, _222031], 608 ^ [_222027, _222029, _222031]) = a_select3(_222029, 608 ^ [_222027, _222029, _222031], 607 ^ [_222027, _222029, _222031])]], 619 ^ _199127 : [(620 ^ _199127) ^ [_222840, _222842] : [-(a_select3(tptp_mmul(_222031, tptp_mmul(_222029, trans(_222031))), _222842, _222840) = a_select3(tptp_mmul(_222031, tptp_mmul(_222029, trans(_222031))), _222840, _222842)), leq(n0, _222842), leq(_222842, _222027), leq(n0, _222840), leq(_222840, _222027)]]], (638 ^ _199127) ^ [_223459, _223461, _223463, _223465] : [641 ^ _199127 : [(642 ^ _199127) ^ [] : [-(leq(n0, 639 ^ [_223459, _223461, _223463, _223465]))], (644 ^ _199127) ^ [] : [-(leq(639 ^ [_223459, _223461, _223463, _223465], _223459))], (646 ^ _199127) ^ [] : [-(leq(n0, 640 ^ [_223459, _223461, _223463, _223465]))], (648 ^ _199127) ^ [] : [-(leq(640 ^ [_223459, _223461, _223463, _223465], _223459))], (650 ^ _199127) ^ [] : [a_select3(_223463, 639 ^ [_223459, _223461, _223463, _223465], 640 ^ [_223459, _223461, _223463, _223465]) = a_select3(_223463, 640 ^ [_223459, _223461, _223463, _223465], 639 ^ [_223459, _223461, _223463, _223465])]], 651 ^ _199127 : [(652 ^ _199127) ^ [_224316, _224318] : [-(a_select3(tptp_mmul(_223465, tptp_mmul(_223463, trans(_223465))), _224318, _224316) = a_select3(tptp_mmul(_223465, tptp_mmul(_223463, trans(_223465))), _224316, _224318)), leq(n0, _224318), leq(_224318, _223461), leq(n0, _224316), leq(_224316, _223461)]]], (670 ^ _199127) ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025] : [675 ^ _199127 : [(676 ^ _199127) ^ [] : [-(leq(n0, 673 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025]))], (678 ^ _199127) ^ [] : [-(leq(673 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025], _225011))], (680 ^ _199127) ^ [] : [-(leq(n0, 674 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025]))], (682 ^ _199127) ^ [] : [-(leq(674 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025], _225011))], (684 ^ _199127) ^ [] : [a_select3(_225019, 673 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025], 674 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025]) = a_select3(_225019, 674 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025], 673 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025])]], 689 ^ _199127 : [(690 ^ _199127) ^ [] : [-(leq(n0, 687 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025]))], (692 ^ _199127) ^ [] : [-(leq(687 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025], _225013))], (694 ^ _199127) ^ [] : [-(leq(n0, 688 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025]))], (696 ^ _199127) ^ [] : [-(leq(688 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025], _225013))], (698 ^ _199127) ^ [] : [a_select3(_225025, 687 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025], 688 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025]) = a_select3(_225025, 688 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025], 687 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025])]], 701 ^ _199127 : [(702 ^ _199127) ^ [] : [-(leq(n0, 699 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025]))], (704 ^ _199127) ^ [] : [-(leq(699 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025], _225013))], (706 ^ _199127) ^ [] : [-(leq(n0, 700 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025]))], (708 ^ _199127) ^ [] : [-(leq(700 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025], _225013))], (710 ^ _199127) ^ [] : [a_select3(_225015, 699 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025], 700 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025]) = a_select3(_225015, 700 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025], 699 ^ [_225011, _225013, _225015, _225017, _225019, _225021, _225023, _225025])]], 711 ^ _199127 : [(712 ^ _199127) ^ [_227939, _227941] : [-(a_select3(tptp_madd(_225025, tptp_mmul(_225023, tptp_mmul(tptp_madd(tptp_mmul(_225021, tptp_mmul(_225019, trans(_225021))), tptp_mmul(_225017, tptp_mmul(_225015, trans(_225017)))), trans(_225023)))), _227941, _227939) = a_select3(tptp_madd(_225025, tptp_mmul(_225023, tptp_mmul(tptp_madd(tptp_mmul(_225021, tptp_mmul(_225019, trans(_225021))), tptp_mmul(_225017, tptp_mmul(_225015, trans(_225017)))), trans(_225023)))), _227939, _227941)), leq(n0, _227941), leq(_227941, _225013), leq(n0, _227939), leq(_227939, _225013)]]], (730 ^ _199127) ^ [_228692] : [-(sum(n0, tptp_minus_1, _228692) = n0)], (732 ^ _199127) ^ [_228774] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _228774))], (734 ^ _199127) ^ [] : [-(succ(tptp_minus_1) = n0)], (736 ^ _199127) ^ [_228909] : [-(plus(_228909, n1) = succ(_228909))], (738 ^ _199127) ^ [_228992] : [-(plus(n1, _228992) = succ(_228992))], (740 ^ _199127) ^ [_229075] : [-(plus(_229075, n2) = succ(succ(_229075)))], (742 ^ _199127) ^ [_229160] : [-(plus(n2, _229160) = succ(succ(_229160)))], (744 ^ _199127) ^ [_229245] : [-(plus(_229245, n3) = succ(succ(succ(_229245))))], (746 ^ _199127) ^ [_229332] : [-(plus(n3, _229332) = succ(succ(succ(_229332))))], (748 ^ _199127) ^ [_229419] : [-(plus(_229419, n4) = succ(succ(succ(succ(_229419)))))], (750 ^ _199127) ^ [_229508] : [-(plus(n4, _229508) = succ(succ(succ(succ(_229508)))))], (752 ^ _199127) ^ [_229597] : [-(plus(_229597, n5) = succ(succ(succ(succ(succ(_229597))))))], (754 ^ _199127) ^ [_229688] : [-(plus(n5, _229688) = succ(succ(succ(succ(succ(_229688))))))], (756 ^ _199127) ^ [_229779] : [-(minus(_229779, n1) = pred(_229779))], (758 ^ _199127) ^ [_229862] : [-(pred(succ(_229862)) = _229862)], (760 ^ _199127) ^ [_229944] : [-(succ(pred(_229944)) = _229944)], (762 ^ _199127) ^ [_230084, _230086] : [leq(succ(_230086), succ(_230084)), -(leq(_230086, _230084))], (768 ^ _199127) ^ [_230254, _230256] : [leq(_230256, _230254), -(leq(succ(_230256), succ(_230254)))], (774 ^ _199127) ^ [_230474, _230476] : [leq(succ(_230476), _230474), -(gt(_230474, _230476))], (780 ^ _199127) ^ [_230688, _230690] : [leq(minus(_230690, _230688), _230690), -(leq(n0, _230688))], (786 ^ _199127) ^ [_230917, _230919, _230921, _230923] : [-(a_select3(tptp_update3(_230923, _230921, _230919, _230917), _230921, _230919) = _230917)], (788 ^ _199127) ^ [_231109, _231111, _231113, _231115, _231117, _231119, _231121] : [-(a_select3(tptp_update3(_231113, _231121, _231119, _231109), _231117, _231115) = _231111), -(_231121 = _231117), _231119 = _231115, a_select3(_231113, _231117, _231115) = _231111], (802 ^ _199127) ^ [_231652, _231654, _231656, _231658, _231660, _231662] : [-(a_select3(tptp_update3(_231654, _231658, _231656, _231652), _231662, _231660) = _231652), 807 ^ _199127 : [(808 ^ _199127) ^ [] : [-(leq(n0, 805 ^ [_231652, _231654, _231656, _231658, _231660, _231662]))], (810 ^ _199127) ^ [] : [-(leq(n0, 806 ^ [_231652, _231654, _231656, _231658, _231660, _231662]))], (812 ^ _199127) ^ [] : [-(leq(805 ^ [_231652, _231654, _231656, _231658, _231660, _231662], _231658))], (814 ^ _199127) ^ [] : [-(leq(806 ^ [_231652, _231654, _231656, _231658, _231660, _231662], _231656))], (816 ^ _199127) ^ [] : [a_select3(_231654, 805 ^ [_231652, _231654, _231656, _231658, _231660, _231662], 806 ^ [_231652, _231654, _231656, _231658, _231660, _231662]) = _231652]], leq(n0, _231662), leq(_231662, _231658), leq(n0, _231660), leq(_231660, _231656)], (834 ^ _199127) ^ [_232994, _232996, _232998] : [-(a_select2(tptp_update2(_232998, _232996, _232994), _232996) = _232994)], (836 ^ _199127) ^ [_233154, _233156, _233158, _233160, _233162] : [-(a_select2(tptp_update2(_233158, _233162, _233154), _233160) = _233156), -(_233162 = _233160), a_select2(_233158, _233160) = _233156], (865 ^ _199127) ^ [] : [-(true)], (867 ^ _199127) ^ [] : [def = use], (846 ^ _199127) ^ [_233534, _233536, _233538, _233540] : [-(a_select2(tptp_update2(_233536, _233538, _233534), _233540) = _233534), 850 ^ _199127 : [(851 ^ _199127) ^ [] : [-(leq(n0, 849 ^ [_233534, _233536, _233538, _233540]))], (853 ^ _199127) ^ [] : [-(leq(849 ^ [_233534, _233536, _233538, _233540], _233538))], (855 ^ _199127) ^ [] : [a_select2(_233536, 849 ^ [_233534, _233536, _233538, _233540]) = _233534]], leq(n0, _233540), leq(_233540, _233538)]], input).
% 0.33/1.37 ncf('1',plain,[leq(n0, n0), leq(n0, pv10), leq(n0, pv53), leq(pv10, minus(n135300, n1)), leq(pv53, minus(n5, n1))],start(1063 ^ 0)).
% 0.33/1.37 ncf('1.1',plain,[-(leq(n0, n0))],extension(286 ^ 1,bind([[_209271], [n0]]))).
% 0.33/1.37 ncf('1.2',plain,[-(leq(n0, pv10))],extension(1055 ^ 1)).
% 0.33/1.37 ncf('1.3',plain,[-(leq(n0, pv53))],extension(1057 ^ 1)).
% 0.33/1.37 ncf('1.4',plain,[-(leq(pv10, minus(n135300, n1)))],extension(1059 ^ 1)).
% 0.33/1.37 ncf('1.5',plain,[-(leq(pv53, minus(n5, n1)))],extension(1061 ^ 1)).
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------