%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS189+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n003.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:26:27 EDT 2023
% Result : Theorem 8.65s 8.63s
% Output : Proof 8.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : KRS189+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n003.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 : Thu May 18 23:09:30 EDT 2023
% 0.12/0.34 % CPUTime :
% 8.65/8.63
% 8.65/8.63 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 8.65/8.63 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.65/8.63 %-----------------------------------------------------
% 8.65/8.63 ncf(matrix, plain, [(689 ^ _75072) ^ [] : [isa(eth, thm)], (509 ^ _75072) ^ [_93663, _93665] : [mighta(_93665, _93663), 514 ^ _75072 : [(515 ^ _75072) ^ [] : [-(status(512 ^ [_93663, _93665], 513 ^ [_93663, _93665], _93665))], (517 ^ _75072) ^ [] : [-(status(512 ^ [_93663, _93665], 513 ^ [_93663, _93665], _93663))]]], (499 ^ _75072) ^ [_93318, _93320] : [-(mighta(_93320, _93318)), 500 ^ _75072 : [(501 ^ _75072) ^ [_93431, _93433] : [status(_93433, _93431, _93320), status(_93433, _93431, _93318)]]], (519 ^ _75072) ^ [_94146, _94148] : [522 ^ _75072 : [(523 ^ _75072) ^ [] : [-(status(520 ^ [_94146, _94148], 521 ^ [_94146, _94148], _94148))], (525 ^ _75072) ^ [] : [status(520 ^ [_94146, _94148], 521 ^ [_94146, _94148], _94146)]], -(isa(_94148, _94146))], (529 ^ _75072) ^ [_94550, _94552] : [isa(_94552, _94550), 532 ^ _75072 : [(533 ^ _75072) ^ [_94708, _94710] : [status(_94710, _94708, _94552), -(status(_94710, _94708, _94550))]]], (549 ^ _75072) ^ [_95324, _95326] : [nota(_95326, _95324), 554 ^ _75072 : [(555 ^ _75072) ^ [] : [-(status(552 ^ [_95324, _95326], 553 ^ [_95324, _95326], _95326))], (557 ^ _75072) ^ [] : [status(552 ^ [_95324, _95326], 553 ^ [_95324, _95326], _95324)]]], (539 ^ _75072) ^ [_94974, _94976] : [-(nota(_94976, _94974)), 540 ^ _75072 : [(541 ^ _75072) ^ [_95089, _95091] : [status(_95091, _95089, _94976), -(status(_95091, _95089, _94974))]]], (559 ^ _75072) ^ [_95812, _95814] : [562 ^ _75072 : [(563 ^ _75072) ^ [] : [-(status(560 ^ [_95812, _95814], 561 ^ [_95812, _95814], _95814))], (565 ^ _75072) ^ [] : [-(status(560 ^ [_95812, _95814], 561 ^ [_95812, _95814], _95812))]], -(nevera(_95814, _95812))], (569 ^ _75072) ^ [_96223, _96225] : [nevera(_96225, _96223), 572 ^ _75072 : [(573 ^ _75072) ^ [_96383, _96385] : [status(_96385, _96383, _96225), status(_96385, _96383, _96223)]]], (597 ^ _75072) ^ [_97266, _97268] : [xora(_97268, _97266), 600 ^ _75072 : [(601 ^ _75072) ^ [_97435, _97437] : [602 ^ _75072 : [(603 ^ _75072) ^ [] : [-(status(_97437, _97435, _97268))], (605 ^ _75072) ^ [] : [status(_97437, _97435, _97266)]], 606 ^ _75072 : [(607 ^ _75072) ^ [] : [-(status(_97437, _97435, _97266))], (609 ^ _75072) ^ [] : [status(_97437, _97435, _97268)]]]]], (579 ^ _75072) ^ [_96650, _96652] : [-(xora(_96652, _96650)), 582 ^ _75072 : [(583 ^ _75072) ^ [] : [status(580 ^ [_96650, _96652], 581 ^ [_96650, _96652], _96652), -(status(580 ^ [_96650, _96652], 581 ^ [_96650, _96652], _96650))], (589 ^ _75072) ^ [] : [status(580 ^ [_96650, _96652], 581 ^ [_96650, _96652], _96650), -(status(580 ^ [_96650, _96652], 581 ^ [_96650, _96652], _96652))]]], (611 ^ _75072) ^ [_97842, _97844] : [612 ^ _75072 : [(613 ^ _75072) ^ [] : [-(model(_97844, _97842))], (615 ^ _75072) ^ [] : [model(_97844, not _97842)]], 616 ^ _75072 : [(617 ^ _75072) ^ [] : [-(model(_97844, not _97842))], (619 ^ _75072) ^ [] : [model(_97844, _97842)]]], (621 ^ _75072) ^ [_98238, _98240] : [model(_98240, _98238), model(_98240, not _98238)], (627 ^ _75072) ^ [_98405, _98407] : [-(model(_98407, not _98405)), -(model(_98407, _98405))], (634 ^ _75072) ^ [_98637] : [-(model(_98637, 632 ^ []))], (638 ^ _75072) ^ [] : [-(model(636 ^ [], 635 ^ []))], (641 ^ _75072) ^ [] : [model(639 ^ [], 635 ^ [])], (644 ^ _75072) ^ [_98996] : [model(_98996, 642 ^ [])], (649 ^ _75072) ^ [] : [-(model(647 ^ [], 645 ^ []))], (651 ^ _75072) ^ [] : [-(model(647 ^ [], 646 ^ []))], (654 ^ _75072) ^ [] : [model(652 ^ [], 645 ^ []), model(652 ^ [], 646 ^ [])], (682 ^ _75072) ^ [] : [-(model(678 ^ [], 679 ^ []))], (684 ^ _75072) ^ [] : [model(678 ^ [], 680 ^ [])], (687 ^ _75072) ^ [] : [-(model(685 ^ [], 680 ^ []))], (663 ^ _75072) ^ [] : [-(model(661 ^ [], 659 ^ []))], (672 ^ _75072) ^ [] : [model(670 ^ [], 659 ^ [])], (674 ^ _75072) ^ [] : [-(model(670 ^ [], 660 ^ []))], (677 ^ _75072) ^ [] : [model(675 ^ [], 660 ^ [])], (665 ^ _75072) ^ [_99849] : [model(_99849, 659 ^ []), -(model(_99849, 660 ^ []))], (2 ^ _75072) ^ [_75234, _75236] : [3 ^ _75072 : [(4 ^ _75072) ^ [_75340] : [model(_75340, _75236)], (7 ^ _75072) ^ [] : [-(model(5 ^ [_75234, _75236], _75234))]], -(status(_75236, _75234, unp))], (11 ^ _75072) ^ [_75555, _75557] : [status(_75557, _75555, unp), -(model(16 ^ [_75555, _75557], _75557)), 19 ^ _75072 : [(20 ^ _75072) ^ [_75819] : [model(_75819, _75555)]]], (22 ^ _75072) ^ [_75970, _75972] : [24 ^ _75072 : [(25 ^ _75072) ^ [] : [-(model(23 ^ [_75970, _75972], _75972))], (27 ^ _75072) ^ [_76170] : [model(_76170, _75970)]], -(status(_75972, _75970, sap))], (31 ^ _75072) ^ [_76287, _76289] : [status(_76289, _76287, sap), 36 ^ _75072 : [(37 ^ _75072) ^ [_76449] : [model(_76449, _76289)]], -(model(38 ^ [_76287, _76289], _76287))], (42 ^ _75072) ^ [_76698, _76700] : [-(status(_76700, _76698, esa)), 46 ^ _75072 : [(47 ^ _75072) ^ [] : [-(model(45 ^ [_76698, _76700], _76700))], (49 ^ _75072) ^ [_76941] : [model(_76941, _76698)]], 51 ^ _75072 : [(52 ^ _75072) ^ [] : [-(model(50 ^ [_76698, _76700], _76698))], (54 ^ _75072) ^ [_77122] : [model(_77122, _76700)]]], (58 ^ _75072) ^ [_77244, _77246] : [status(_77246, _77244, esa), 61 ^ _75072 : [(62 ^ _75072) ^ [] : [63 ^ _75072 : [(64 ^ _75072) ^ [_77435] : [model(_77435, _77246)]], -(model(65 ^ [_77244, _77246], _77244))], (69 ^ _75072) ^ [] : [70 ^ _75072 : [(71 ^ _75072) ^ [_77633] : [model(_77633, _77244)]], -(model(72 ^ [_77244, _77246], _77246))]]], (86 ^ _75072) ^ [_78201, _78203] : [status(_78203, _78201, sat), 90 ^ _75072 : [(91 ^ _75072) ^ [] : [-(model(89 ^ [_78201, _78203], _78203))], (93 ^ _75072) ^ [] : [-(model(89 ^ [_78201, _78203], _78201))]]], (76 ^ _75072) ^ [_77885, _77887] : [-(status(_77887, _77885, sat)), 77 ^ _75072 : [(78 ^ _75072) ^ [_77978] : [model(_77978, _77887), model(_77978, _77885)]]], (95 ^ _75072) ^ [_78589, _78591] : [97 ^ _75072 : [(98 ^ _75072) ^ [] : [-(model(96 ^ [_78589, _78591], _78591))], (100 ^ _75072) ^ [] : [model(96 ^ [_78589, _78591], _78589)]], -(status(_78591, _78589, thm))], (104 ^ _75072) ^ [_78898, _78900] : [status(_78900, _78898, thm), 107 ^ _75072 : [(108 ^ _75072) ^ [_79037] : [model(_79037, _78900), -(model(_79037, _78898))]]], (114 ^ _75072) ^ [_79293, _79295] : [-(status(_79295, _79293, eqv)), 117 ^ _75072 : [(118 ^ _75072) ^ [_79415] : [model(_79415, _79295)]], 122 ^ _75072 : [(123 ^ _75072) ^ [] : [-(model(119 ^ [_79293, _79295], _79295))], (125 ^ _75072) ^ [] : [model(119 ^ [_79293, _79295], _79293)]], 126 ^ _75072 : [(127 ^ _75072) ^ [] : [-(model(119 ^ [_79293, _79295], _79293))], (129 ^ _75072) ^ [] : [model(119 ^ [_79293, _79295], _79295)]]], (133 ^ _75072) ^ [_79888, _79890] : [status(_79890, _79888, eqv), 137 ^ _75072 : [(138 ^ _75072) ^ [] : [-(model(136 ^ [_79888, _79890], _79890))], (140 ^ _75072) ^ [_80185] : [model(_80185, _79890), -(model(_80185, _79888))], (146 ^ _75072) ^ [_80357] : [model(_80357, _79888), -(model(_80357, _79890))]]], (163 ^ _75072) ^ [_80949, _80951] : [status(_80951, _80949, tac), 167 ^ _75072 : [(168 ^ _75072) ^ [] : [-(model(166 ^ [_80949, _80951], _80951))], (170 ^ _75072) ^ [_81196] : [-(model(_81196, _80949))]]], (152 ^ _75072) ^ [_80617, _80619] : [-(status(_80619, _80617, tac)), 155 ^ _75072 : [(156 ^ _75072) ^ [_80733] : [model(_80733, _80619)]], model(157 ^ [_80617, _80619], _80617)], (193 ^ _75072) ^ [_82011, _82013] : [status(_82013, _82011, wec), 197 ^ _75072 : [(198 ^ _75072) ^ [] : [-(model(196 ^ [_82011, _82013], _82013))], (207 ^ _75072) ^ [] : [-(model(205 ^ [_82011, _82013], _82011))], (209 ^ _75072) ^ [] : [model(205 ^ [_82011, _82013], _82013)], (200 ^ _75072) ^ [_82318] : [model(_82318, _82013), -(model(_82318, _82011))]]], (172 ^ _75072) ^ [_81345, _81347] : [-(status(_81347, _81345, wec)), 175 ^ _75072 : [(176 ^ _75072) ^ [_81486] : [model(_81486, _81347)]], 180 ^ _75072 : [(181 ^ _75072) ^ [] : [-(model(179 ^ [_81345, _81347], _81347))], (183 ^ _75072) ^ [] : [model(179 ^ [_81345, _81347], _81345)]], 184 ^ _75072 : [(185 ^ _75072) ^ [_81775] : [model(_81775, _81345), -(model(_81775, _81347))]]], (211 ^ _75072) ^ [_82760, _82762] : [-(status(_82762, _82760, eth)), 214 ^ _75072 : [(215 ^ _75072) ^ [_82895] : [model(_82895, _82762)]], 218 ^ _75072 : [(219 ^ _75072) ^ [_82991] : [-(model(_82991, _82762))]], 223 ^ _75072 : [(224 ^ _75072) ^ [] : [-(model(220 ^ [_82760, _82762], _82762))], (226 ^ _75072) ^ [] : [model(220 ^ [_82760, _82762], _82760)]], 227 ^ _75072 : [(228 ^ _75072) ^ [] : [-(model(220 ^ [_82760, _82762], _82760))], (230 ^ _75072) ^ [] : [model(220 ^ [_82760, _82762], _82762)]]], (234 ^ _75072) ^ [_83469, _83471] : [status(_83471, _83469, eth), 238 ^ _75072 : [(239 ^ _75072) ^ [] : [-(model(237 ^ [_83469, _83471], _83471))], (242 ^ _75072) ^ [] : [model(240 ^ [_83469, _83471], _83471)], (244 ^ _75072) ^ [_83898] : [model(_83898, _83471), -(model(_83898, _83469))], (250 ^ _75072) ^ [_84070] : [model(_84070, _83469), -(model(_84070, _83471))]]], (267 ^ _75072) ^ [_84655, _84657] : [status(_84657, _84655, tau), 270 ^ _75072 : [(271 ^ _75072) ^ [_84799] : [-(model(_84799, _84657))], (273 ^ _75072) ^ [_84847] : [-(model(_84847, _84655))]]], (256 ^ _75072) ^ [_84332, _84334] : [-(status(_84334, _84332, tau)), model(257 ^ [_84332, _84334], _84334), model(257 ^ [_84332, _84334], _84332)], (290 ^ _75072) ^ [_85442, _85444] : [status(_85444, _85442, wtc), 294 ^ _75072 : [(295 ^ _75072) ^ [] : [-(model(293 ^ [_85442, _85444], _85444))], (298 ^ _75072) ^ [] : [model(296 ^ [_85442, _85444], _85444)], (300 ^ _75072) ^ [_85821] : [-(model(_85821, _85442))]]], (275 ^ _75072) ^ [_84996, _84998] : [-(status(_84998, _84996, wtc)), 278 ^ _75072 : [(279 ^ _75072) ^ [_85125] : [model(_85125, _84998)]], 282 ^ _75072 : [(283 ^ _75072) ^ [_85221] : [-(model(_85221, _84998))]], model(284 ^ [_84996, _84998], _84996)], (327 ^ _75072) ^ [_86752, _86754] : [status(_86754, _86752, wth), 331 ^ _75072 : [(332 ^ _75072) ^ [] : [-(model(330 ^ [_86752, _86754], _86754))], (341 ^ _75072) ^ [] : [-(model(339 ^ [_86752, _86754], _86752))], (343 ^ _75072) ^ [] : [model(339 ^ [_86752, _86754], _86754)], (346 ^ _75072) ^ [] : [model(344 ^ [_86752, _86754], _86752)], (334 ^ _75072) ^ [_87072] : [model(_87072, _86754), -(model(_87072, _86752))]]], (302 ^ _75072) ^ [_85972, _85974] : [-(status(_85974, _85972, wth)), 305 ^ _75072 : [(306 ^ _75072) ^ [_86126] : [model(_86126, _85974)]], 310 ^ _75072 : [(311 ^ _75072) ^ [] : [-(model(309 ^ [_85972, _85974], _85974))], (313 ^ _75072) ^ [] : [model(309 ^ [_85972, _85974], _85972)]], 322 ^ _75072 : [(323 ^ _75072) ^ [_86622] : [-(model(_86622, _85972))]], 316 ^ _75072 : [(317 ^ _75072) ^ [_86449] : [model(_86449, _85972), -(model(_86449, _85974))]]], (348 ^ _75072) ^ [_87639, _87641] : [-(model(349 ^ [_87639, _87641], _87641)), -(status(_87641, _87639, cax))], (355 ^ _75072) ^ [_87863, _87865] : [status(_87865, _87863, cax), 358 ^ _75072 : [(359 ^ _75072) ^ [_87982] : [model(_87982, _87865)]]], (372 ^ _75072) ^ [_88464, _88466] : [status(_88466, _88464, sca), 375 ^ _75072 : [(376 ^ _75072) ^ [_88614] : [model(_88614, _88466)], (379 ^ _75072) ^ [] : [-(model(377 ^ [_88464, _88466], _88464))]]], (361 ^ _75072) ^ [_88129, _88131] : [-(status(_88131, _88129, sca)), -(model(364 ^ [_88129, _88131], _88131)), 367 ^ _75072 : [(368 ^ _75072) ^ [_88345] : [model(_88345, _88129)]]], (393 ^ _75072) ^ [_89231, _89233] : [status(_89233, _89231, tca), 396 ^ _75072 : [(397 ^ _75072) ^ [_89381] : [model(_89381, _89233)], (399 ^ _75072) ^ [_89443] : [-(model(_89443, _89231))]]], (381 ^ _75072) ^ [_88861, _88863] : [-(status(_88863, _88861, tca)), -(model(384 ^ [_88861, _88863], _88863)), model(387 ^ [_88861, _88863], _88861)], (416 ^ _75072) ^ [_90041, _90043] : [status(_90043, _90041, wca), 419 ^ _75072 : [(420 ^ _75072) ^ [_90204] : [model(_90204, _90043)], (423 ^ _75072) ^ [] : [-(model(421 ^ [_90041, _90043], _90041))], (426 ^ _75072) ^ [] : [model(424 ^ [_90041, _90043], _90041)]]], (401 ^ _75072) ^ [_89592, _89594] : [-(status(_89594, _89592, wca)), -(model(404 ^ [_89592, _89594], _89594)), 409 ^ _75072 : [(410 ^ _75072) ^ [_89855] : [model(_89855, _89592)]], 411 ^ _75072 : [(412 ^ _75072) ^ [_89917] : [-(model(_89917, _89592))]]], (438 ^ _75072) ^ [_90894, _90896] : [status(_90896, _90894, csa), 442 ^ _75072 : [(443 ^ _75072) ^ [] : [-(model(441 ^ [_90894, _90896], _90896))], (445 ^ _75072) ^ [] : [-(model(441 ^ [_90894, _90896], not _90894))]]], (428 ^ _75072) ^ [_90572, _90574] : [-(status(_90574, _90572, csa)), 429 ^ _75072 : [(430 ^ _75072) ^ [_90667] : [model(_90667, _90574), model(_90667, not _90572)]]], (459 ^ _75072) ^ [_91661, _91663] : [status(_91663, _91661, uns), 462 ^ _75072 : [(463 ^ _75072) ^ [_91812] : [-(model(_91812, _91663))], (465 ^ _75072) ^ [_91874] : [-(model(_91874, not _91661))]]], (447 ^ _75072) ^ [_91288, _91290] : [-(status(_91290, _91288, uns)), model(450 ^ [_91288, _91290], _91290), model(453 ^ [_91288, _91290], not _91288)], (485 ^ _75072) ^ [_92568, _92570] : [status(_92570, _92568, noc), 489 ^ _75072 : [(490 ^ _75072) ^ [] : [-(model(488 ^ [_92568, _92570], _92570))], (492 ^ _75072) ^ [] : [-(model(488 ^ [_92568, _92570], _92568))], (495 ^ _75072) ^ [] : [-(model(493 ^ [_92568, _92570], _92570))], (497 ^ _75072) ^ [] : [-(model(493 ^ [_92568, _92570], not _92568))]]], (467 ^ _75072) ^ [_92005, _92007] : [-(status(_92007, _92005, noc)), 470 ^ _75072 : [(471 ^ _75072) ^ [_92151] : [model(_92151, _92007), model(_92151, _92005)]], 476 ^ _75072 : [(477 ^ _75072) ^ [_92336] : [model(_92336, _92007), model(_92336, not _92005)]]]], input).
% 8.65/8.63 ncf('1',plain,[isa(eth, thm)],start(689 ^ 0)).
% 8.65/8.63 ncf('1.1',plain,[-(isa(eth, thm)), 523 : -(status(520 ^ [thm, eth], 521 ^ [thm, eth], eth))],extension(519 ^ 1,bind([[_94146, _94148], [thm, eth]]))).
% 8.65/8.63 ncf('1.1.1',plain,[status(520 ^ [thm, eth], 521 ^ [thm, eth], eth), 244 : model(96 ^ [521 ^ [thm, eth], 520 ^ [thm, eth]], 520 ^ [thm, eth]), 244 : -(model(96 ^ [521 ^ [thm, eth], 520 ^ [thm, eth]], 521 ^ [thm, eth]))],extension(234 ^ 4,bind([[_83469, _83471, _83898], [521 ^ [thm, eth], 520 ^ [thm, eth], 96 ^ [521 ^ [thm, eth], 520 ^ [thm, eth]]]]))).
% 8.65/8.63 ncf('1.1.1.1',plain,[-(model(96 ^ [521 ^ [thm, eth], 520 ^ [thm, eth]], 520 ^ [thm, eth])), -(status(520 ^ [thm, eth], 521 ^ [thm, eth], thm))],extension(95 ^ 7,bind([[_78589, _78591], [521 ^ [thm, eth], 520 ^ [thm, eth]]]))).
% 8.65/8.63 ncf('1.1.1.1.1',plain,[status(520 ^ [thm, eth], 521 ^ [thm, eth], thm)],extension(525 ^ 8)).
% 8.65/8.63 ncf('1.1.1.2',plain,[model(96 ^ [521 ^ [thm, eth], 520 ^ [thm, eth]], 521 ^ [thm, eth]), -(status(520 ^ [thm, eth], 521 ^ [thm, eth], thm))],extension(95 ^ 7,bind([[_78589, _78591], [521 ^ [thm, eth], 520 ^ [thm, eth]]]))).
% 8.65/8.63 ncf('1.1.1.2.1',plain,[status(520 ^ [thm, eth], 521 ^ [thm, eth], thm)],extension(525 ^ 8)).
% 8.65/8.63 %-----------------------------------------------------
% 8.65/8.63 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------