%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : ITP019+2 : TPTP v8.1.2. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n010.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 11:23:21 EDT 2023
% Result : Theorem 0.34s 1.37s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ITP019+2 : TPTP v8.1.2. Bugfixed v7.5.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n010.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 18 21:33:27 EDT 2023
% 0.13/0.33 % CPUTime :
% 0.34/1.37
% 0.34/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.34/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 ncf(matrix, plain, [(538 ^ _62177) ^ [] : [-(mem(536 ^ [], ty_2Epair_2Eprod(ty_2Erealax_2Ereal, ty_2Erealax_2Ereal)))], (540 ^ _62177) ^ [] : [536 ^ [] = ap(c_2Ecomplex_2Ecomplex__of__num, c_2Enum_2E0)], (542 ^ _62177) ^ [] : [-(ap(c_2Ecomplex_2Ecomplex__inv, 536 ^ []) = ap(c_2Ecomplex_2Ecomplex__of__num, c_2Enum_2E0))], (2 ^ _62177) ^ [_62321] : [-(_62321 = _62321)], (4 ^ _62177) ^ [_62428, _62430] : [_62430 = _62428, -(_62428 = _62430)], (10 ^ _62177) ^ [_62632, _62634, _62636] : [-(_62636 = _62632), _62636 = _62634, _62634 = _62632], (20 ^ _62177) ^ [_62945, _62947] : [-(ne(_62945)), _62947 = _62945, ne(_62947)], (30 ^ _62177) ^ [_63240, _63242] : [-(p(_63240)), _63242 = _63240, p(_63242)], (40 ^ _62177) ^ [_63543, _63545, _63547, _63549] : [-(mem(_63547, _63543)), mem(_63549, _63545), _63549 = _63547, _63545 = _63543], (54 ^ _62177) ^ [_63997, _63999, _64001, _64003] : [-(k(_64003, _63999) = k(_64001, _63997)), _64003 = _64001, _63999 = _63997], (64 ^ _62177) ^ [_64328, _64330] : [_64330 = _64328, -(i(_64330) = i(_64328))], (70 ^ _62177) ^ [_64546, _64548] : [_64548 = _64546, -(c_2Emin_2E_3D(_64548) = c_2Emin_2E_3D(_64546))], (76 ^ _62177) ^ [_64792, _64794, _64796, _64798] : [-(arr(_64798, _64794) = arr(_64796, _64792)), _64798 = _64796, _64794 = _64792], (86 ^ _62177) ^ [_65123, _65125] : [_65125 = _65123, -(c_2Ebool_2E_21(_65125) = c_2Ebool_2E_21(_65123))], (92 ^ _62177) ^ [_65369, _65371, _65373, _65375] : [-(ty_2Epair_2Eprod(_65375, _65371) = ty_2Epair_2Eprod(_65373, _65369)), _65375 = _65373, _65371 = _65369], (102 ^ _62177) ^ [_65708, _65710, _65712, _65714] : [-(ap(_65714, _65710) = ap(_65712, _65708)), _65714 = _65712, _65710 = _65708], (112 ^ _62177) ^ [] : [-(ne(bool))], (114 ^ _62177) ^ [] : [-(ne(ind))], (116 ^ _62177) ^ [_66175] : [ne(_66175), 119 ^ _62177 : [(120 ^ _62177) ^ [_66307] : [ne(_66307), -(ne(arr(_66175, _66307)))]]], (126 ^ _62177) ^ [_66540, _66542, _66544] : [mem(_66540, arr(_66544, _66542)), 129 ^ _62177 : [(130 ^ _62177) ^ [_66690] : [mem(_66690, _66544), -(mem(ap(_66540, _66690), _66542))]]], (136 ^ _62177) ^ [_66915] : [mem(_66915, bool), 139 ^ _62177 : [(140 ^ _62177) ^ [_67058] : [mem(_67058, bool), -(_66915 = _67058), 147 ^ _62177 : [(148 ^ _62177) ^ [] : [-(p(_66915))], (150 ^ _62177) ^ [] : [p(_67058)]], 151 ^ _62177 : [(152 ^ _62177) ^ [] : [-(p(_67058))], (154 ^ _62177) ^ [] : [p(_66915)]]]]], (158 ^ _62177) ^ [_67608, _67610, _67612] : [mem(_67608, arr(_67612, _67610)), 161 ^ _62177 : [(162 ^ _62177) ^ [_67781] : [mem(_67781, arr(_67612, _67610)), 168 ^ _62177 : [(169 ^ _62177) ^ [] : [-(mem(167 ^ [_67608, _67610, _67612, _67781], _67612))], (171 ^ _62177) ^ [] : [ap(_67608, 167 ^ [_67608, _67610, _67612, _67781]) = ap(_67781, 167 ^ [_67608, _67610, _67612, _67781])]], -(_67608 = _67781)]]], (175 ^ _62177) ^ [_68325, _68327, _68329] : [mem(_68325, _68329), -(ap(k(_68329, _68327), _68325) = _68327)], (181 ^ _62177) ^ [_68533, _68535] : [mem(_68533, _68535), -(ap(i(_68535), _68533) = _68533)], (187 ^ _62177) ^ [] : [-(mem(c_2Ebool_2E_7E, arr(bool, bool)))], (189 ^ _62177) ^ [_68806] : [mem(_68806, bool), 192 ^ _62177 : [(193 ^ _62177) ^ [] : [p(ap(c_2Ebool_2E_7E, _68806)), p(_68806)], (199 ^ _62177) ^ [] : [-(p(_68806)), -(p(ap(c_2Ebool_2E_7E, _68806)))]]], (205 ^ _62177) ^ [] : [-(mem(c_2Ebool_2EF, bool))], (207 ^ _62177) ^ [] : [p(c_2Ebool_2EF)], (209 ^ _62177) ^ [] : [-(mem(c_2Ebool_2ET, bool))], (211 ^ _62177) ^ [] : [-(p(c_2Ebool_2ET))], (213 ^ _62177) ^ [] : [-(mem(c_2Emin_2E_3D_3D_3E, arr(bool, arr(bool, bool))))], (215 ^ _62177) ^ [_69505] : [mem(_69505, bool), 218 ^ _62177 : [(219 ^ _62177) ^ [_69653] : [mem(_69653, bool), 222 ^ _62177 : [(233 ^ _62177) ^ [] : [234 ^ _62177 : [(235 ^ _62177) ^ [] : [-(p(_69505))], (237 ^ _62177) ^ [] : [p(_69653)]], -(p(ap(ap(c_2Emin_2E_3D_3D_3E, _69505), _69653)))], (223 ^ _62177) ^ [] : [p(ap(ap(c_2Emin_2E_3D_3D_3E, _69505), _69653)), p(_69505), -(p(_69653))]]]]], (241 ^ _62177) ^ [] : [-(mem(c_2Ebool_2E_2F_5C, arr(bool, arr(bool, bool))))], (243 ^ _62177) ^ [_70326] : [mem(_70326, bool), 246 ^ _62177 : [(247 ^ _62177) ^ [_70474] : [mem(_70474, bool), 250 ^ _62177 : [(251 ^ _62177) ^ [] : [p(ap(ap(c_2Ebool_2E_2F_5C, _70326), _70474)), 254 ^ _62177 : [(255 ^ _62177) ^ [] : [-(p(_70326))], (257 ^ _62177) ^ [] : [-(p(_70474))]]], (259 ^ _62177) ^ [] : [-(p(ap(ap(c_2Ebool_2E_2F_5C, _70326), _70474))), p(_70326), p(_70474)]]]]], (269 ^ _62177) ^ [] : [-(ne(ty_2Enum_2Enum))], (271 ^ _62177) ^ [] : [-(mem(c_2Enum_2E0, ty_2Enum_2Enum))], (273 ^ _62177) ^ [] : [-(ne(ty_2Erealax_2Ereal))], (275 ^ _62177) ^ [_71253] : [ne(_71253), 278 ^ _62177 : [(279 ^ _62177) ^ [_71385] : [ne(_71385), -(ne(ty_2Epair_2Eprod(_71253, _71385)))]]], (285 ^ _62177) ^ [] : [-(mem(c_2Ecomplex_2Ecomplex__of__num, arr(ty_2Enum_2Enum, ty_2Epair_2Eprod(ty_2Erealax_2Ereal, ty_2Erealax_2Ereal))))], (287 ^ _62177) ^ [] : [-(mem(c_2Ecomplex_2Ecomplex__inv, arr(ty_2Epair_2Eprod(ty_2Erealax_2Ereal, ty_2Erealax_2Ereal), ty_2Epair_2Eprod(ty_2Erealax_2Ereal, ty_2Erealax_2Ereal))))], (289 ^ _62177) ^ [_71696] : [ne(_71696), -(mem(c_2Emin_2E_3D(_71696), arr(_71696, arr(_71696, bool))))], (295 ^ _62177) ^ [_71900] : [ne(_71900), 298 ^ _62177 : [(299 ^ _62177) ^ [_72055] : [mem(_72055, _71900), 302 ^ _62177 : [(303 ^ _62177) ^ [_72207] : [mem(_72207, _71900), 306 ^ _62177 : [(307 ^ _62177) ^ [] : [p(ap(ap(c_2Emin_2E_3D(_71900), _72055), _72207)), -(_72055 = _72207)], (313 ^ _62177) ^ [] : [_72055 = _72207, -(p(ap(ap(c_2Emin_2E_3D(_71900), _72055), _72207)))]]]]]]], (319 ^ _62177) ^ [_72704] : [ne(_72704), -(mem(c_2Ebool_2E_21(_72704), arr(arr(_72704, bool), bool)))], (325 ^ _62177) ^ [_72908] : [ne(_72908), 328 ^ _62177 : [(329 ^ _62177) ^ [_73065] : [mem(_73065, arr(_72908, bool)), 332 ^ _62177 : [(343 ^ _62177) ^ [] : [345 ^ _62177 : [(346 ^ _62177) ^ [] : [-(mem(344 ^ [_72908, _73065], _72908))], (348 ^ _62177) ^ [] : [p(ap(_73065, 344 ^ [_72908, _73065]))]], -(p(ap(c_2Ebool_2E_21(_72908), _73065)))], (333 ^ _62177) ^ [] : [p(ap(c_2Ebool_2E_21(_72908), _73065)), 336 ^ _62177 : [(337 ^ _62177) ^ [_73334] : [mem(_73334, _72908), -(p(ap(_73065, _73334)))]]]]]]], (352 ^ _62177) ^ [] : [true___, -(true___)], (358 ^ _62177) ^ [_73951] : [ne(_73951), 361 ^ _62177 : [(362 ^ _62177) ^ [_74097] : [mem(_74097, bool), 365 ^ _62177 : [(366 ^ _62177) ^ [] : [368 ^ _62177 : [(369 ^ _62177) ^ [] : [-(mem(367 ^ [_73951, _74097], _73951))], (371 ^ _62177) ^ [] : [p(_74097)]], -(p(_74097))], (375 ^ _62177) ^ [] : [p(_74097), 378 ^ _62177 : [(379 ^ _62177) ^ [_74600] : [mem(_74600, _73951), -(p(_74097))]]]]]]], (521 ^ _62177) ^ [_78138] : [mem(_78138, ty_2Epair_2Eprod(ty_2Erealax_2Ereal, ty_2Erealax_2Ereal)), 524 ^ _62177 : [(525 ^ _62177) ^ [] : [ap(c_2Ecomplex_2Ecomplex__inv, _78138) = ap(c_2Ecomplex_2Ecomplex__of__num, c_2Enum_2E0), -(_78138 = ap(c_2Ecomplex_2Ecomplex__of__num, c_2Enum_2E0))], (531 ^ _62177) ^ [] : [_78138 = ap(c_2Ecomplex_2Ecomplex__of__num, c_2Enum_2E0), -(ap(c_2Ecomplex_2Ecomplex__inv, _78138) = ap(c_2Ecomplex_2Ecomplex__of__num, c_2Enum_2E0))]]], (385 ^ _62177) ^ [_74821] : [mem(_74821, bool), 388 ^ _62177 : [(389 ^ _62177) ^ [] : [-(p(_74821)), 390 ^ _62177 : [(397 ^ _62177) ^ [] : [p(_74821)], (391 ^ _62177) ^ [] : [true___, -(true___)]]], (401 ^ _62177) ^ [] : [p(_74821), 406 ^ _62177 : [(407 ^ _62177) ^ [] : [-(true___)], (409 ^ _62177) ^ [] : [true___]], -(p(_74821))], (413 ^ _62177) ^ [] : [414 ^ _62177 : [(415 ^ _62177) ^ [] : [-(p(_74821))], (417 ^ _62177) ^ [] : [-(true___)], (419 ^ _62177) ^ [] : [true___]], true___, -(true___)], (427 ^ _62177) ^ [] : [428 ^ _62177 : [(429 ^ _62177) ^ [] : [-(true___)], (431 ^ _62177) ^ [] : [true___]], p(_74821), true___, -(true___)], (443 ^ _62177) ^ [] : [444 ^ _62177 : [(445 ^ _62177) ^ [] : [-(false___)], (447 ^ _62177) ^ [] : [false___], (449 ^ _62177) ^ [] : [p(_74821)]], true___, -(true___)], (457 ^ _62177) ^ [] : [458 ^ _62177 : [(459 ^ _62177) ^ [] : [-(true___)], (461 ^ _62177) ^ [] : [true___]], -(p(_74821)), false___, -(false___)], (473 ^ _62177) ^ [] : [474 ^ _62177 : [(475 ^ _62177) ^ [] : [-(p(_74821))], (477 ^ _62177) ^ [] : [p(_74821)]], true___, -(true___)], (485 ^ _62177) ^ [] : [486 ^ _62177 : [(487 ^ _62177) ^ [] : [-(true___)], (489 ^ _62177) ^ [] : [true___]], p(_74821), -(p(_74821))], (497 ^ _62177) ^ [] : [p(_74821), 498 ^ _62177 : [(499 ^ _62177) ^ [] : [-(p(_74821))], (501 ^ _62177) ^ [] : [false___, -(false___)]]], (509 ^ _62177) ^ [] : [-(p(_74821)), p(_74821), 516 ^ _62177 : [(517 ^ _62177) ^ [] : [-(false___)], (519 ^ _62177) ^ [] : [false___]]]]]], input).
% 0.34/1.37 ncf('1',plain,[536 ^ [] = ap(c_2Ecomplex_2Ecomplex__of__num, c_2Enum_2E0)],start(540 ^ 0)).
% 0.34/1.37 ncf('1.1',plain,[-(536 ^ [] = ap(c_2Ecomplex_2Ecomplex__of__num, c_2Enum_2E0)), 525 : ap(c_2Ecomplex_2Ecomplex__inv, 536 ^ []) = ap(c_2Ecomplex_2Ecomplex__of__num, c_2Enum_2E0), 525 : mem(536 ^ [], ty_2Epair_2Eprod(ty_2Erealax_2Ereal, ty_2Erealax_2Ereal))],extension(521 ^ 1,bind([[_78138], [536 ^ []]]))).
% 0.34/1.37 ncf('1.1.1',plain,[-(ap(c_2Ecomplex_2Ecomplex__inv, 536 ^ []) = ap(c_2Ecomplex_2Ecomplex__of__num, c_2Enum_2E0))],extension(542 ^ 4)).
% 0.34/1.37 ncf('1.1.2',plain,[-(mem(536 ^ [], ty_2Epair_2Eprod(ty_2Erealax_2Ereal, ty_2Erealax_2Ereal)))],extension(538 ^ 2)).
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------