%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV045+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n022.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:50 EDT 2023
% Result : Theorem 0.21s 1.33s
% Output : Proof 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.01/0.10 % Problem : SWV045+1 : TPTP v8.1.2. Bugfixed v3.3.0.
% 0.01/0.10 % Command : nanocop.sh %s %d
% 0.10/0.30 % Computer : n022.cluster.edu
% 0.10/0.30 % Model : x86_64 x86_64
% 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.30 % Memory : 8042.1875MB
% 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.30 % CPULimit : 300
% 0.10/0.30 % WCLimit : 300
% 0.10/0.30 % DateTime : Fri May 19 02:09:46 EDT 2023
% 0.10/0.30 % CPUTime :
% 0.21/1.33
% 0.21/1.33 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.21/1.33 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/1.33 %-----------------------------------------------------
% 0.21/1.33 ncf(matrix, plain, [(1055 ^ _197744) ^ [] : [-(pv76 = sum(n0, minus(n135300, n1), a_select3(q, pv77, pv25)))], (1057 ^ _197744) ^ [] : [-(leq(n0, pv25))], (1059 ^ _197744) ^ [] : [-(leq(pv25, minus(n5, n1)))], (1061 ^ _197744) ^ [] : [true], (2 ^ _197744) ^ [_197888] : [-(_197888 = _197888)], (4 ^ _197744) ^ [_197995, _197997] : [_197997 = _197995, -(_197995 = _197997)], (10 ^ _197744) ^ [_198199, _198201, _198203] : [-(_198203 = _198199), _198203 = _198201, _198201 = _198199], (20 ^ _197744) ^ [_198540, _198542, _198544, _198546] : [-(lt(_198544, _198540)), lt(_198546, _198542), _198546 = _198544, _198542 = _198540], (34 ^ _197744) ^ [_198984, _198986, _198988, _198990] : [-(geq(_198988, _198984)), geq(_198990, _198986), _198990 = _198988, _198986 = _198984], (48 ^ _197744) ^ [_199428, _199430, _199432, _199434] : [-(gt(_199432, _199428)), gt(_199434, _199430), _199434 = _199432, _199430 = _199428], (62 ^ _197744) ^ [_199852, _199854, _199856, _199858] : [-(leq(_199856, _199852)), leq(_199858, _199854), _199858 = _199856, _199854 = _199852], (76 ^ _197744) ^ [_200308, _200310, _200312, _200314] : [-(uniform_int_rnd(_200314, _200310) = uniform_int_rnd(_200312, _200308)), _200314 = _200312, _200310 = _200308], (86 ^ _197744) ^ [_200667, _200669, _200671, _200673] : [-(tptp_const_array1(_200673, _200669) = tptp_const_array1(_200671, _200667)), _200673 = _200671, _200669 = _200667], (96 ^ _197744) ^ [_201054, _201056, _201058, _201060, _201062, _201064] : [-(tptp_const_array2(_201064, _201060, _201056) = tptp_const_array2(_201062, _201058, _201054)), _201064 = _201062, _201060 = _201058, _201056 = _201054], (110 ^ _197744) ^ [_201542, _201544, _201546, _201548] : [-(dim(_201548, _201544) = dim(_201546, _201542)), _201548 = _201546, _201544 = _201542], (120 ^ _197744) ^ [_201873, _201875] : [_201875 = _201873, -(inv(_201875) = inv(_201873))], (126 ^ _197744) ^ [_202119, _202121, _202123, _202125] : [-(tptp_msub(_202125, _202121) = tptp_msub(_202123, _202119)), _202125 = _202123, _202121 = _202119], (136 ^ _197744) ^ [_202478, _202480, _202482, _202484] : [-(tptp_madd(_202484, _202480) = tptp_madd(_202482, _202478)), _202484 = _202482, _202480 = _202478], (146 ^ _197744) ^ [_202837, _202839, _202841, _202843] : [-(tptp_mmul(_202843, _202839) = tptp_mmul(_202841, _202837)), _202843 = _202841, _202839 = _202837], (156 ^ _197744) ^ [_203168, _203170] : [_203170 = _203168, -(trans(_203170) = trans(_203168))], (162 ^ _197744) ^ [_203414, _203416, _203418, _203420] : [-(plus(_203420, _203416) = plus(_203418, _203414)), _203420 = _203418, _203416 = _203414], (172 ^ _197744) ^ [_203745, _203747] : [_203747 = _203745, -(pred(_203747) = pred(_203745))], (178 ^ _197744) ^ [_204047, _204049, _204051, _204053, _204055, _204057, _204059, _204061] : [-(tptp_update3(_204061, _204057, _204053, _204049) = tptp_update3(_204059, _204055, _204051, _204047)), _204061 = _204059, _204057 = _204055, _204053 = _204051, _204049 = _204047], (196 ^ _197744) ^ [_204680, _204682, _204684, _204686] : [-(a_select2(_204686, _204682) = a_select2(_204684, _204680)), _204686 = _204684, _204682 = _204680], (206 ^ _197744) ^ [_205067, _205069, _205071, _205073, _205075, _205077] : [-(tptp_update2(_205077, _205073, _205069) = tptp_update2(_205075, _205071, _205067)), _205077 = _205075, _205073 = _205071, _205069 = _205067], (220 ^ _197744) ^ [_205527, _205529] : [_205529 = _205527, -(succ(_205529) = succ(_205527))], (226 ^ _197744) ^ [_205801, _205803, _205805, _205807, _205809, _205811] : [-(sum(_205811, _205807, _205803) = sum(_205809, _205805, _205801)), _205811 = _205809, _205807 = _205805, _205803 = _205801], (254 ^ _197744) ^ [_206785, _206787, _206789, _206791] : [-(minus(_206791, _206787) = minus(_206789, _206785)), _206791 = _206789, _206787 = _206785], (240 ^ _197744) ^ [_206317, _206319, _206321, _206323, _206325, _206327] : [-(a_select3(_206327, _206323, _206319) = a_select3(_206325, _206321, _206317)), _206327 = _206325, _206323 = _206321, _206319 = _206317], (869 ^ _197744) ^ [] : [-(gt(n5, n4))], (871 ^ _197744) ^ [] : [-(gt(n135300, n4))], (873 ^ _197744) ^ [] : [-(gt(n135300, n5))], (875 ^ _197744) ^ [] : [-(gt(n4, tptp_minus_1))], (877 ^ _197744) ^ [] : [-(gt(n5, tptp_minus_1))], (879 ^ _197744) ^ [] : [-(gt(n135300, tptp_minus_1))], (881 ^ _197744) ^ [] : [-(gt(n0, tptp_minus_1))], (883 ^ _197744) ^ [] : [-(gt(n1, tptp_minus_1))], (885 ^ _197744) ^ [] : [-(gt(n2, tptp_minus_1))], (887 ^ _197744) ^ [] : [-(gt(n3, tptp_minus_1))], (889 ^ _197744) ^ [] : [-(gt(n4, n0))], (891 ^ _197744) ^ [] : [-(gt(n5, n0))], (893 ^ _197744) ^ [] : [-(gt(n135300, n0))], (895 ^ _197744) ^ [] : [-(gt(n1, n0))], (897 ^ _197744) ^ [] : [-(gt(n2, n0))], (899 ^ _197744) ^ [] : [-(gt(n3, n0))], (901 ^ _197744) ^ [] : [-(gt(n4, n1))], (903 ^ _197744) ^ [] : [-(gt(n5, n1))], (905 ^ _197744) ^ [] : [-(gt(n135300, n1))], (907 ^ _197744) ^ [] : [-(gt(n2, n1))], (909 ^ _197744) ^ [] : [-(gt(n3, n1))], (911 ^ _197744) ^ [] : [-(gt(n4, n2))], (913 ^ _197744) ^ [] : [-(gt(n5, n2))], (915 ^ _197744) ^ [] : [-(gt(n135300, n2))], (917 ^ _197744) ^ [] : [-(gt(n3, n2))], (919 ^ _197744) ^ [] : [-(gt(n4, n3))], (921 ^ _197744) ^ [] : [-(gt(n5, n3))], (923 ^ _197744) ^ [] : [-(gt(n135300, n3))], (925 ^ _197744) ^ [_234625] : [leq(n0, _234625), leq(_234625, n4), -(_234625 = n0), -(_234625 = n1), -(_234625 = n2), -(_234625 = n3), -(_234625 = n4)], (951 ^ _197744) ^ [_235246] : [leq(n0, _235246), leq(_235246, n5), -(_235246 = n0), -(_235246 = n1), -(_235246 = n2), -(_235246 = n3), -(_235246 = n4), -(_235246 = n5)], (981 ^ _197744) ^ [_235953] : [-(_235953 = n0), leq(n0, _235953), leq(_235953, n0)], (991 ^ _197744) ^ [_236228] : [leq(n0, _236228), leq(_236228, n1), -(_236228 = n0), -(_236228 = n1)], (1005 ^ _197744) ^ [_236591] : [leq(n0, _236591), leq(_236591, n2), -(_236591 = n0), -(_236591 = n1), -(_236591 = n2)], (1045 ^ _197744) ^ [] : [-(succ(succ(succ(succ(n0)))) = n4)], (1047 ^ _197744) ^ [] : [-(succ(succ(succ(succ(succ(n0))))) = n5)], (1049 ^ _197744) ^ [] : [-(succ(n0) = n1)], (1051 ^ _197744) ^ [] : [-(succ(succ(n0)) = n2)], (1053 ^ _197744) ^ [] : [-(succ(succ(succ(n0))) = n3)], (1023 ^ _197744) ^ [_237040] : [leq(n0, _237040), leq(_237040, n3), -(_237040 = n0), -(_237040 = n1), -(_237040 = n2), -(_237040 = n3)], (264 ^ _197744) ^ [_207216, _207218] : [-(gt(_207218, _207216)), -(gt(_207216, _207218)), -(_207218 = _207216)], (274 ^ _197744) ^ [_207531, _207533, _207535] : [-(gt(_207535, _207531)), gt(_207535, _207533), gt(_207533, _207531)], (284 ^ _197744) ^ [_207810] : [gt(_207810, _207810)], (286 ^ _197744) ^ [_207888] : [-(leq(_207888, _207888))], (288 ^ _197744) ^ [_208009, _208011, _208013] : [-(leq(_208013, _208009)), leq(_208013, _208011), leq(_208011, _208009)], (298 ^ _197744) ^ [_208347, _208349] : [lt(_208349, _208347), -(gt(_208347, _208349))], (304 ^ _197744) ^ [_208509, _208511] : [gt(_208509, _208511), -(lt(_208511, _208509))], (310 ^ _197744) ^ [_208750, _208752] : [geq(_208752, _208750), -(leq(_208750, _208752))], (316 ^ _197744) ^ [_208912, _208914] : [leq(_208912, _208914), -(geq(_208914, _208912))], (322 ^ _197744) ^ [_209124, _209126] : [gt(_209124, _209126), -(leq(_209126, _209124))], (328 ^ _197744) ^ [_209334, _209336] : [-(gt(_209334, _209336)), leq(_209336, _209334), -(_209336 = _209334)], (338 ^ _197744) ^ [_209665, _209667] : [leq(_209667, pred(_209665)), -(gt(_209665, _209667))], (344 ^ _197744) ^ [_209831, _209833] : [gt(_209831, _209833), -(leq(_209833, pred(_209831)))], (350 ^ _197744) ^ [_210018] : [-(gt(succ(_210018), _210018))], (352 ^ _197744) ^ [_210127, _210129] : [leq(_210129, _210127), -(leq(_210129, succ(_210127)))], (358 ^ _197744) ^ [_210370, _210372] : [leq(_210372, _210370), -(gt(succ(_210370), _210372))], (364 ^ _197744) ^ [_210536, _210538] : [gt(succ(_210536), _210538), -(leq(_210538, _210536))], (370 ^ _197744) ^ [_210752, _210754] : [leq(n0, _210754), -(leq(uniform_int_rnd(_210752, _210754), _210754))], (376 ^ _197744) ^ [_210968, _210970] : [leq(n0, _210970), -(leq(n0, uniform_int_rnd(_210968, _210970)))], (382 ^ _197744) ^ [_211212, _211214, _211216, _211218] : [-(a_select2(tptp_const_array1(dim(_211216, _211214), _211212), _211218) = _211212), leq(_211216, _211218), leq(_211218, _211214)], (392 ^ _197744) ^ [_211619, _211621, _211623, _211625, _211627, _211629, _211631] : [-(a_select3(tptp_const_array2(dim(_211629, _211627), dim(_211623, _211621), _211619), _211631, _211625) = _211619), leq(_211629, _211631), leq(_211631, _211627), leq(_211623, _211625), leq(_211625, _211621)], (410 ^ _197744) ^ [_212214, _212216] : [413 ^ _197744 : [(414 ^ _197744) ^ [] : [-(leq(n0, 411 ^ [_212214, _212216]))], (416 ^ _197744) ^ [] : [-(leq(411 ^ [_212214, _212216], _212214))], (418 ^ _197744) ^ [] : [-(leq(n0, 412 ^ [_212214, _212216]))], (420 ^ _197744) ^ [] : [-(leq(412 ^ [_212214, _212216], _212214))], (422 ^ _197744) ^ [] : [a_select3(_212216, 411 ^ [_212214, _212216], 412 ^ [_212214, _212216]) = a_select3(_212216, 412 ^ [_212214, _212216], 411 ^ [_212214, _212216])]], 423 ^ _197744 : [(424 ^ _197744) ^ [_212971, _212973] : [-(a_select3(trans(_212216), _212973, _212971) = a_select3(trans(_212216), _212971, _212973)), leq(n0, _212973), leq(_212973, _212214), leq(n0, _212971), leq(_212971, _212214)]]], (442 ^ _197744) ^ [_213518, _213520] : [445 ^ _197744 : [(446 ^ _197744) ^ [] : [-(leq(n0, 443 ^ [_213518, _213520]))], (448 ^ _197744) ^ [] : [-(leq(443 ^ [_213518, _213520], _213518))], (450 ^ _197744) ^ [] : [-(leq(n0, 444 ^ [_213518, _213520]))], (452 ^ _197744) ^ [] : [-(leq(444 ^ [_213518, _213520], _213518))], (454 ^ _197744) ^ [] : [a_select3(_213520, 443 ^ [_213518, _213520], 444 ^ [_213518, _213520]) = a_select3(_213520, 444 ^ [_213518, _213520], 443 ^ [_213518, _213520])]], 455 ^ _197744 : [(456 ^ _197744) ^ [_214275, _214277] : [-(a_select3(inv(_213520), _214277, _214275) = a_select3(inv(_213520), _214275, _214277)), leq(n0, _214277), leq(_214277, _213518), leq(n0, _214275), leq(_214275, _213518)]]], (474 ^ _197744) ^ [_214822, _214824] : [477 ^ _197744 : [(478 ^ _197744) ^ [] : [-(leq(n0, 475 ^ [_214822, _214824]))], (480 ^ _197744) ^ [] : [-(leq(475 ^ [_214822, _214824], _214822))], (482 ^ _197744) ^ [] : [-(leq(n0, 476 ^ [_214822, _214824]))], (484 ^ _197744) ^ [] : [-(leq(476 ^ [_214822, _214824], _214822))], (486 ^ _197744) ^ [] : [a_select3(_214824, 475 ^ [_214822, _214824], 476 ^ [_214822, _214824]) = a_select3(_214824, 476 ^ [_214822, _214824], 475 ^ [_214822, _214824])]], 487 ^ _197744 : [(488 ^ _197744) ^ [_215635, _215637, _215639, _215641] : [-(a_select3(tptp_update3(_214824, _215637, _215637, _215635), _215641, _215639) = a_select3(tptp_update3(_214824, _215637, _215637, _215635), _215639, _215641)), leq(n0, _215641), leq(_215641, _214822), leq(n0, _215639), leq(_215639, _214822), leq(n0, _215637), leq(_215637, _214822)]]], (514 ^ _197744) ^ [_216454, _216456, _216458] : [519 ^ _197744 : [(520 ^ _197744) ^ [] : [-(leq(n0, 517 ^ [_216454, _216456, _216458]))], (522 ^ _197744) ^ [] : [-(leq(517 ^ [_216454, _216456, _216458], _216454))], (524 ^ _197744) ^ [] : [-(leq(n0, 518 ^ [_216454, _216456, _216458]))], (526 ^ _197744) ^ [] : [-(leq(518 ^ [_216454, _216456, _216458], _216454))], (528 ^ _197744) ^ [] : [a_select3(_216458, 517 ^ [_216454, _216456, _216458], 518 ^ [_216454, _216456, _216458]) = a_select3(_216458, 518 ^ [_216454, _216456, _216458], 517 ^ [_216454, _216456, _216458])]], 531 ^ _197744 : [(532 ^ _197744) ^ [] : [-(leq(n0, 529 ^ [_216454, _216456, _216458]))], (534 ^ _197744) ^ [] : [-(leq(529 ^ [_216454, _216456, _216458], _216454))], (536 ^ _197744) ^ [] : [-(leq(n0, 530 ^ [_216454, _216456, _216458]))], (538 ^ _197744) ^ [] : [-(leq(530 ^ [_216454, _216456, _216458], _216454))], (540 ^ _197744) ^ [] : [a_select3(_216456, 529 ^ [_216454, _216456, _216458], 530 ^ [_216454, _216456, _216458]) = a_select3(_216456, 530 ^ [_216454, _216456, _216458], 529 ^ [_216454, _216456, _216458])]], 541 ^ _197744 : [(542 ^ _197744) ^ [_217963, _217965] : [-(a_select3(tptp_madd(_216458, _216456), _217965, _217963) = a_select3(tptp_madd(_216458, _216456), _217963, _217965)), leq(n0, _217965), leq(_217965, _216454), leq(n0, _217963), leq(_217963, _216454)]]], (560 ^ _197744) ^ [_218549, _218551, _218553] : [565 ^ _197744 : [(566 ^ _197744) ^ [] : [-(leq(n0, 563 ^ [_218549, _218551, _218553]))], (568 ^ _197744) ^ [] : [-(leq(563 ^ [_218549, _218551, _218553], _218549))], (570 ^ _197744) ^ [] : [-(leq(n0, 564 ^ [_218549, _218551, _218553]))], (572 ^ _197744) ^ [] : [-(leq(564 ^ [_218549, _218551, _218553], _218549))], (574 ^ _197744) ^ [] : [a_select3(_218553, 563 ^ [_218549, _218551, _218553], 564 ^ [_218549, _218551, _218553]) = a_select3(_218553, 564 ^ [_218549, _218551, _218553], 563 ^ [_218549, _218551, _218553])]], 577 ^ _197744 : [(578 ^ _197744) ^ [] : [-(leq(n0, 575 ^ [_218549, _218551, _218553]))], (580 ^ _197744) ^ [] : [-(leq(575 ^ [_218549, _218551, _218553], _218549))], (582 ^ _197744) ^ [] : [-(leq(n0, 576 ^ [_218549, _218551, _218553]))], (584 ^ _197744) ^ [] : [-(leq(576 ^ [_218549, _218551, _218553], _218549))], (586 ^ _197744) ^ [] : [a_select3(_218551, 575 ^ [_218549, _218551, _218553], 576 ^ [_218549, _218551, _218553]) = a_select3(_218551, 576 ^ [_218549, _218551, _218553], 575 ^ [_218549, _218551, _218553])]], 587 ^ _197744 : [(588 ^ _197744) ^ [_220058, _220060] : [-(a_select3(tptp_msub(_218553, _218551), _220060, _220058) = a_select3(tptp_msub(_218553, _218551), _220058, _220060)), leq(n0, _220060), leq(_220060, _218549), leq(n0, _220058), leq(_220058, _218549)]]], (606 ^ _197744) ^ [_220644, _220646, _220648] : [609 ^ _197744 : [(610 ^ _197744) ^ [] : [-(leq(n0, 607 ^ [_220644, _220646, _220648]))], (612 ^ _197744) ^ [] : [-(leq(607 ^ [_220644, _220646, _220648], _220644))], (614 ^ _197744) ^ [] : [-(leq(n0, 608 ^ [_220644, _220646, _220648]))], (616 ^ _197744) ^ [] : [-(leq(608 ^ [_220644, _220646, _220648], _220644))], (618 ^ _197744) ^ [] : [a_select3(_220646, 607 ^ [_220644, _220646, _220648], 608 ^ [_220644, _220646, _220648]) = a_select3(_220646, 608 ^ [_220644, _220646, _220648], 607 ^ [_220644, _220646, _220648])]], 619 ^ _197744 : [(620 ^ _197744) ^ [_221457, _221459] : [-(a_select3(tptp_mmul(_220648, tptp_mmul(_220646, trans(_220648))), _221459, _221457) = a_select3(tptp_mmul(_220648, tptp_mmul(_220646, trans(_220648))), _221457, _221459)), leq(n0, _221459), leq(_221459, _220644), leq(n0, _221457), leq(_221457, _220644)]]], (638 ^ _197744) ^ [_222076, _222078, _222080, _222082] : [641 ^ _197744 : [(642 ^ _197744) ^ [] : [-(leq(n0, 639 ^ [_222076, _222078, _222080, _222082]))], (644 ^ _197744) ^ [] : [-(leq(639 ^ [_222076, _222078, _222080, _222082], _222076))], (646 ^ _197744) ^ [] : [-(leq(n0, 640 ^ [_222076, _222078, _222080, _222082]))], (648 ^ _197744) ^ [] : [-(leq(640 ^ [_222076, _222078, _222080, _222082], _222076))], (650 ^ _197744) ^ [] : [a_select3(_222080, 639 ^ [_222076, _222078, _222080, _222082], 640 ^ [_222076, _222078, _222080, _222082]) = a_select3(_222080, 640 ^ [_222076, _222078, _222080, _222082], 639 ^ [_222076, _222078, _222080, _222082])]], 651 ^ _197744 : [(652 ^ _197744) ^ [_222933, _222935] : [-(a_select3(tptp_mmul(_222082, tptp_mmul(_222080, trans(_222082))), _222935, _222933) = a_select3(tptp_mmul(_222082, tptp_mmul(_222080, trans(_222082))), _222933, _222935)), leq(n0, _222935), leq(_222935, _222078), leq(n0, _222933), leq(_222933, _222078)]]], (670 ^ _197744) ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642] : [675 ^ _197744 : [(676 ^ _197744) ^ [] : [-(leq(n0, 673 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642]))], (678 ^ _197744) ^ [] : [-(leq(673 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642], _223628))], (680 ^ _197744) ^ [] : [-(leq(n0, 674 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642]))], (682 ^ _197744) ^ [] : [-(leq(674 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642], _223628))], (684 ^ _197744) ^ [] : [a_select3(_223636, 673 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642], 674 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642]) = a_select3(_223636, 674 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642], 673 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642])]], 689 ^ _197744 : [(690 ^ _197744) ^ [] : [-(leq(n0, 687 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642]))], (692 ^ _197744) ^ [] : [-(leq(687 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642], _223630))], (694 ^ _197744) ^ [] : [-(leq(n0, 688 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642]))], (696 ^ _197744) ^ [] : [-(leq(688 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642], _223630))], (698 ^ _197744) ^ [] : [a_select3(_223642, 687 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642], 688 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642]) = a_select3(_223642, 688 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642], 687 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642])]], 701 ^ _197744 : [(702 ^ _197744) ^ [] : [-(leq(n0, 699 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642]))], (704 ^ _197744) ^ [] : [-(leq(699 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642], _223630))], (706 ^ _197744) ^ [] : [-(leq(n0, 700 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642]))], (708 ^ _197744) ^ [] : [-(leq(700 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642], _223630))], (710 ^ _197744) ^ [] : [a_select3(_223632, 699 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642], 700 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642]) = a_select3(_223632, 700 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642], 699 ^ [_223628, _223630, _223632, _223634, _223636, _223638, _223640, _223642])]], 711 ^ _197744 : [(712 ^ _197744) ^ [_226556, _226558] : [-(a_select3(tptp_madd(_223642, tptp_mmul(_223640, tptp_mmul(tptp_madd(tptp_mmul(_223638, tptp_mmul(_223636, trans(_223638))), tptp_mmul(_223634, tptp_mmul(_223632, trans(_223634)))), trans(_223640)))), _226558, _226556) = a_select3(tptp_madd(_223642, tptp_mmul(_223640, tptp_mmul(tptp_madd(tptp_mmul(_223638, tptp_mmul(_223636, trans(_223638))), tptp_mmul(_223634, tptp_mmul(_223632, trans(_223634)))), trans(_223640)))), _226556, _226558)), leq(n0, _226558), leq(_226558, _223630), leq(n0, _226556), leq(_226556, _223630)]]], (730 ^ _197744) ^ [_227309] : [-(sum(n0, tptp_minus_1, _227309) = n0)], (732 ^ _197744) ^ [_227391] : [-(tptp_float_0_0 = sum(n0, tptp_minus_1, _227391))], (734 ^ _197744) ^ [] : [-(succ(tptp_minus_1) = n0)], (736 ^ _197744) ^ [_227526] : [-(plus(_227526, n1) = succ(_227526))], (738 ^ _197744) ^ [_227609] : [-(plus(n1, _227609) = succ(_227609))], (740 ^ _197744) ^ [_227692] : [-(plus(_227692, n2) = succ(succ(_227692)))], (742 ^ _197744) ^ [_227777] : [-(plus(n2, _227777) = succ(succ(_227777)))], (744 ^ _197744) ^ [_227862] : [-(plus(_227862, n3) = succ(succ(succ(_227862))))], (746 ^ _197744) ^ [_227949] : [-(plus(n3, _227949) = succ(succ(succ(_227949))))], (748 ^ _197744) ^ [_228036] : [-(plus(_228036, n4) = succ(succ(succ(succ(_228036)))))], (750 ^ _197744) ^ [_228125] : [-(plus(n4, _228125) = succ(succ(succ(succ(_228125)))))], (752 ^ _197744) ^ [_228214] : [-(plus(_228214, n5) = succ(succ(succ(succ(succ(_228214))))))], (754 ^ _197744) ^ [_228305] : [-(plus(n5, _228305) = succ(succ(succ(succ(succ(_228305))))))], (756 ^ _197744) ^ [_228396] : [-(minus(_228396, n1) = pred(_228396))], (758 ^ _197744) ^ [_228479] : [-(pred(succ(_228479)) = _228479)], (760 ^ _197744) ^ [_228561] : [-(succ(pred(_228561)) = _228561)], (762 ^ _197744) ^ [_228701, _228703] : [leq(succ(_228703), succ(_228701)), -(leq(_228703, _228701))], (768 ^ _197744) ^ [_228871, _228873] : [leq(_228873, _228871), -(leq(succ(_228873), succ(_228871)))], (774 ^ _197744) ^ [_229091, _229093] : [leq(succ(_229093), _229091), -(gt(_229091, _229093))], (780 ^ _197744) ^ [_229305, _229307] : [leq(minus(_229307, _229305), _229307), -(leq(n0, _229305))], (786 ^ _197744) ^ [_229534, _229536, _229538, _229540] : [-(a_select3(tptp_update3(_229540, _229538, _229536, _229534), _229538, _229536) = _229534)], (788 ^ _197744) ^ [_229726, _229728, _229730, _229732, _229734, _229736, _229738] : [-(a_select3(tptp_update3(_229730, _229738, _229736, _229726), _229734, _229732) = _229728), -(_229738 = _229734), _229736 = _229732, a_select3(_229730, _229734, _229732) = _229728], (802 ^ _197744) ^ [_230269, _230271, _230273, _230275, _230277, _230279] : [-(a_select3(tptp_update3(_230271, _230275, _230273, _230269), _230279, _230277) = _230269), 807 ^ _197744 : [(808 ^ _197744) ^ [] : [-(leq(n0, 805 ^ [_230269, _230271, _230273, _230275, _230277, _230279]))], (810 ^ _197744) ^ [] : [-(leq(n0, 806 ^ [_230269, _230271, _230273, _230275, _230277, _230279]))], (812 ^ _197744) ^ [] : [-(leq(805 ^ [_230269, _230271, _230273, _230275, _230277, _230279], _230275))], (814 ^ _197744) ^ [] : [-(leq(806 ^ [_230269, _230271, _230273, _230275, _230277, _230279], _230273))], (816 ^ _197744) ^ [] : [a_select3(_230271, 805 ^ [_230269, _230271, _230273, _230275, _230277, _230279], 806 ^ [_230269, _230271, _230273, _230275, _230277, _230279]) = _230269]], leq(n0, _230279), leq(_230279, _230275), leq(n0, _230277), leq(_230277, _230273)], (834 ^ _197744) ^ [_231611, _231613, _231615] : [-(a_select2(tptp_update2(_231615, _231613, _231611), _231613) = _231611)], (836 ^ _197744) ^ [_231771, _231773, _231775, _231777, _231779] : [-(a_select2(tptp_update2(_231775, _231779, _231771), _231777) = _231773), -(_231779 = _231777), a_select2(_231775, _231777) = _231773], (865 ^ _197744) ^ [] : [-(true)], (867 ^ _197744) ^ [] : [def = use], (846 ^ _197744) ^ [_232151, _232153, _232155, _232157] : [-(a_select2(tptp_update2(_232153, _232155, _232151), _232157) = _232151), 850 ^ _197744 : [(851 ^ _197744) ^ [] : [-(leq(n0, 849 ^ [_232151, _232153, _232155, _232157]))], (853 ^ _197744) ^ [] : [-(leq(849 ^ [_232151, _232153, _232155, _232157], _232155))], (855 ^ _197744) ^ [] : [a_select2(_232153, 849 ^ [_232151, _232153, _232155, _232157]) = _232151]], leq(n0, _232157), leq(_232157, _232155)]], input).
% 0.21/1.33 ncf('1',plain,[true],start(1061 ^ 0)).
% 0.21/1.33 ncf('1.1',plain,[-(true)],extension(865 ^ 1)).
% 0.21/1.33 %-----------------------------------------------------
% 0.21/1.33 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------