%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS192+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:28 EDT 2023
% Result : Theorem 9.70s 9.70s
% Output : Proof 9.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : KRS192+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.13/0.35 % Computer : n003.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 18 23:09:15 EDT 2023
% 0.13/0.35 % CPUTime :
% 9.70/9.70
% 9.70/9.70 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 9.70/9.70 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.70/9.70 %-----------------------------------------------------
% 9.70/9.70 ncf(matrix, plain, [(689 ^ _75137) ^ [] : [isa(wth, thm)], (509 ^ _75137) ^ [_93728, _93730] : [mighta(_93730, _93728), 514 ^ _75137 : [(515 ^ _75137) ^ [] : [-(status(512 ^ [_93728, _93730], 513 ^ [_93728, _93730], _93730))], (517 ^ _75137) ^ [] : [-(status(512 ^ [_93728, _93730], 513 ^ [_93728, _93730], _93728))]]], (499 ^ _75137) ^ [_93383, _93385] : [-(mighta(_93385, _93383)), 500 ^ _75137 : [(501 ^ _75137) ^ [_93496, _93498] : [status(_93498, _93496, _93385), status(_93498, _93496, _93383)]]], (519 ^ _75137) ^ [_94211, _94213] : [522 ^ _75137 : [(523 ^ _75137) ^ [] : [-(status(520 ^ [_94211, _94213], 521 ^ [_94211, _94213], _94213))], (525 ^ _75137) ^ [] : [status(520 ^ [_94211, _94213], 521 ^ [_94211, _94213], _94211)]], -(isa(_94213, _94211))], (529 ^ _75137) ^ [_94615, _94617] : [isa(_94617, _94615), 532 ^ _75137 : [(533 ^ _75137) ^ [_94773, _94775] : [status(_94775, _94773, _94617), -(status(_94775, _94773, _94615))]]], (549 ^ _75137) ^ [_95389, _95391] : [nota(_95391, _95389), 554 ^ _75137 : [(555 ^ _75137) ^ [] : [-(status(552 ^ [_95389, _95391], 553 ^ [_95389, _95391], _95391))], (557 ^ _75137) ^ [] : [status(552 ^ [_95389, _95391], 553 ^ [_95389, _95391], _95389)]]], (539 ^ _75137) ^ [_95039, _95041] : [-(nota(_95041, _95039)), 540 ^ _75137 : [(541 ^ _75137) ^ [_95154, _95156] : [status(_95156, _95154, _95041), -(status(_95156, _95154, _95039))]]], (559 ^ _75137) ^ [_95877, _95879] : [562 ^ _75137 : [(563 ^ _75137) ^ [] : [-(status(560 ^ [_95877, _95879], 561 ^ [_95877, _95879], _95879))], (565 ^ _75137) ^ [] : [-(status(560 ^ [_95877, _95879], 561 ^ [_95877, _95879], _95877))]], -(nevera(_95879, _95877))], (569 ^ _75137) ^ [_96288, _96290] : [nevera(_96290, _96288), 572 ^ _75137 : [(573 ^ _75137) ^ [_96448, _96450] : [status(_96450, _96448, _96290), status(_96450, _96448, _96288)]]], (597 ^ _75137) ^ [_97331, _97333] : [xora(_97333, _97331), 600 ^ _75137 : [(601 ^ _75137) ^ [_97500, _97502] : [602 ^ _75137 : [(603 ^ _75137) ^ [] : [-(status(_97502, _97500, _97333))], (605 ^ _75137) ^ [] : [status(_97502, _97500, _97331)]], 606 ^ _75137 : [(607 ^ _75137) ^ [] : [-(status(_97502, _97500, _97331))], (609 ^ _75137) ^ [] : [status(_97502, _97500, _97333)]]]]], (579 ^ _75137) ^ [_96715, _96717] : [-(xora(_96717, _96715)), 582 ^ _75137 : [(583 ^ _75137) ^ [] : [status(580 ^ [_96715, _96717], 581 ^ [_96715, _96717], _96717), -(status(580 ^ [_96715, _96717], 581 ^ [_96715, _96717], _96715))], (589 ^ _75137) ^ [] : [status(580 ^ [_96715, _96717], 581 ^ [_96715, _96717], _96715), -(status(580 ^ [_96715, _96717], 581 ^ [_96715, _96717], _96717))]]], (611 ^ _75137) ^ [_97907, _97909] : [612 ^ _75137 : [(613 ^ _75137) ^ [] : [-(model(_97909, _97907))], (615 ^ _75137) ^ [] : [model(_97909, not _97907)]], 616 ^ _75137 : [(617 ^ _75137) ^ [] : [-(model(_97909, not _97907))], (619 ^ _75137) ^ [] : [model(_97909, _97907)]]], (621 ^ _75137) ^ [_98303, _98305] : [model(_98305, _98303), model(_98305, not _98303)], (627 ^ _75137) ^ [_98470, _98472] : [-(model(_98472, not _98470)), -(model(_98472, _98470))], (634 ^ _75137) ^ [_98702] : [-(model(_98702, 632 ^ []))], (638 ^ _75137) ^ [] : [-(model(636 ^ [], 635 ^ []))], (641 ^ _75137) ^ [] : [model(639 ^ [], 635 ^ [])], (644 ^ _75137) ^ [_99061] : [model(_99061, 642 ^ [])], (649 ^ _75137) ^ [] : [-(model(647 ^ [], 645 ^ []))], (651 ^ _75137) ^ [] : [-(model(647 ^ [], 646 ^ []))], (654 ^ _75137) ^ [] : [model(652 ^ [], 645 ^ []), model(652 ^ [], 646 ^ [])], (682 ^ _75137) ^ [] : [-(model(678 ^ [], 679 ^ []))], (684 ^ _75137) ^ [] : [model(678 ^ [], 680 ^ [])], (687 ^ _75137) ^ [] : [-(model(685 ^ [], 680 ^ []))], (663 ^ _75137) ^ [] : [-(model(661 ^ [], 659 ^ []))], (672 ^ _75137) ^ [] : [model(670 ^ [], 659 ^ [])], (674 ^ _75137) ^ [] : [-(model(670 ^ [], 660 ^ []))], (677 ^ _75137) ^ [] : [model(675 ^ [], 660 ^ [])], (665 ^ _75137) ^ [_99914] : [model(_99914, 659 ^ []), -(model(_99914, 660 ^ []))], (2 ^ _75137) ^ [_75299, _75301] : [3 ^ _75137 : [(4 ^ _75137) ^ [_75405] : [model(_75405, _75301)], (7 ^ _75137) ^ [] : [-(model(5 ^ [_75299, _75301], _75299))]], -(status(_75301, _75299, unp))], (11 ^ _75137) ^ [_75620, _75622] : [status(_75622, _75620, unp), -(model(16 ^ [_75620, _75622], _75622)), 19 ^ _75137 : [(20 ^ _75137) ^ [_75884] : [model(_75884, _75620)]]], (22 ^ _75137) ^ [_76035, _76037] : [24 ^ _75137 : [(25 ^ _75137) ^ [] : [-(model(23 ^ [_76035, _76037], _76037))], (27 ^ _75137) ^ [_76235] : [model(_76235, _76035)]], -(status(_76037, _76035, sap))], (31 ^ _75137) ^ [_76352, _76354] : [status(_76354, _76352, sap), 36 ^ _75137 : [(37 ^ _75137) ^ [_76514] : [model(_76514, _76354)]], -(model(38 ^ [_76352, _76354], _76352))], (42 ^ _75137) ^ [_76763, _76765] : [-(status(_76765, _76763, esa)), 46 ^ _75137 : [(47 ^ _75137) ^ [] : [-(model(45 ^ [_76763, _76765], _76765))], (49 ^ _75137) ^ [_77006] : [model(_77006, _76763)]], 51 ^ _75137 : [(52 ^ _75137) ^ [] : [-(model(50 ^ [_76763, _76765], _76763))], (54 ^ _75137) ^ [_77187] : [model(_77187, _76765)]]], (58 ^ _75137) ^ [_77309, _77311] : [status(_77311, _77309, esa), 61 ^ _75137 : [(62 ^ _75137) ^ [] : [63 ^ _75137 : [(64 ^ _75137) ^ [_77500] : [model(_77500, _77311)]], -(model(65 ^ [_77309, _77311], _77309))], (69 ^ _75137) ^ [] : [70 ^ _75137 : [(71 ^ _75137) ^ [_77698] : [model(_77698, _77309)]], -(model(72 ^ [_77309, _77311], _77311))]]], (86 ^ _75137) ^ [_78266, _78268] : [status(_78268, _78266, sat), 90 ^ _75137 : [(91 ^ _75137) ^ [] : [-(model(89 ^ [_78266, _78268], _78268))], (93 ^ _75137) ^ [] : [-(model(89 ^ [_78266, _78268], _78266))]]], (76 ^ _75137) ^ [_77950, _77952] : [-(status(_77952, _77950, sat)), 77 ^ _75137 : [(78 ^ _75137) ^ [_78043] : [model(_78043, _77952), model(_78043, _77950)]]], (95 ^ _75137) ^ [_78654, _78656] : [97 ^ _75137 : [(98 ^ _75137) ^ [] : [-(model(96 ^ [_78654, _78656], _78656))], (100 ^ _75137) ^ [] : [model(96 ^ [_78654, _78656], _78654)]], -(status(_78656, _78654, thm))], (104 ^ _75137) ^ [_78963, _78965] : [status(_78965, _78963, thm), 107 ^ _75137 : [(108 ^ _75137) ^ [_79102] : [model(_79102, _78965), -(model(_79102, _78963))]]], (114 ^ _75137) ^ [_79358, _79360] : [-(status(_79360, _79358, eqv)), 117 ^ _75137 : [(118 ^ _75137) ^ [_79480] : [model(_79480, _79360)]], 122 ^ _75137 : [(123 ^ _75137) ^ [] : [-(model(119 ^ [_79358, _79360], _79360))], (125 ^ _75137) ^ [] : [model(119 ^ [_79358, _79360], _79358)]], 126 ^ _75137 : [(127 ^ _75137) ^ [] : [-(model(119 ^ [_79358, _79360], _79358))], (129 ^ _75137) ^ [] : [model(119 ^ [_79358, _79360], _79360)]]], (133 ^ _75137) ^ [_79953, _79955] : [status(_79955, _79953, eqv), 137 ^ _75137 : [(138 ^ _75137) ^ [] : [-(model(136 ^ [_79953, _79955], _79955))], (140 ^ _75137) ^ [_80250] : [model(_80250, _79955), -(model(_80250, _79953))], (146 ^ _75137) ^ [_80422] : [model(_80422, _79953), -(model(_80422, _79955))]]], (163 ^ _75137) ^ [_81014, _81016] : [status(_81016, _81014, tac), 167 ^ _75137 : [(168 ^ _75137) ^ [] : [-(model(166 ^ [_81014, _81016], _81016))], (170 ^ _75137) ^ [_81261] : [-(model(_81261, _81014))]]], (152 ^ _75137) ^ [_80682, _80684] : [-(status(_80684, _80682, tac)), 155 ^ _75137 : [(156 ^ _75137) ^ [_80798] : [model(_80798, _80684)]], model(157 ^ [_80682, _80684], _80682)], (193 ^ _75137) ^ [_82076, _82078] : [status(_82078, _82076, wec), 197 ^ _75137 : [(198 ^ _75137) ^ [] : [-(model(196 ^ [_82076, _82078], _82078))], (207 ^ _75137) ^ [] : [-(model(205 ^ [_82076, _82078], _82076))], (209 ^ _75137) ^ [] : [model(205 ^ [_82076, _82078], _82078)], (200 ^ _75137) ^ [_82383] : [model(_82383, _82078), -(model(_82383, _82076))]]], (172 ^ _75137) ^ [_81410, _81412] : [-(status(_81412, _81410, wec)), 175 ^ _75137 : [(176 ^ _75137) ^ [_81551] : [model(_81551, _81412)]], 180 ^ _75137 : [(181 ^ _75137) ^ [] : [-(model(179 ^ [_81410, _81412], _81412))], (183 ^ _75137) ^ [] : [model(179 ^ [_81410, _81412], _81410)]], 184 ^ _75137 : [(185 ^ _75137) ^ [_81840] : [model(_81840, _81410), -(model(_81840, _81412))]]], (211 ^ _75137) ^ [_82825, _82827] : [-(status(_82827, _82825, eth)), 214 ^ _75137 : [(215 ^ _75137) ^ [_82960] : [model(_82960, _82827)]], 218 ^ _75137 : [(219 ^ _75137) ^ [_83056] : [-(model(_83056, _82827))]], 223 ^ _75137 : [(224 ^ _75137) ^ [] : [-(model(220 ^ [_82825, _82827], _82827))], (226 ^ _75137) ^ [] : [model(220 ^ [_82825, _82827], _82825)]], 227 ^ _75137 : [(228 ^ _75137) ^ [] : [-(model(220 ^ [_82825, _82827], _82825))], (230 ^ _75137) ^ [] : [model(220 ^ [_82825, _82827], _82827)]]], (234 ^ _75137) ^ [_83534, _83536] : [status(_83536, _83534, eth), 238 ^ _75137 : [(239 ^ _75137) ^ [] : [-(model(237 ^ [_83534, _83536], _83536))], (242 ^ _75137) ^ [] : [model(240 ^ [_83534, _83536], _83536)], (244 ^ _75137) ^ [_83963] : [model(_83963, _83536), -(model(_83963, _83534))], (250 ^ _75137) ^ [_84135] : [model(_84135, _83534), -(model(_84135, _83536))]]], (267 ^ _75137) ^ [_84720, _84722] : [status(_84722, _84720, tau), 270 ^ _75137 : [(271 ^ _75137) ^ [_84864] : [-(model(_84864, _84722))], (273 ^ _75137) ^ [_84912] : [-(model(_84912, _84720))]]], (256 ^ _75137) ^ [_84397, _84399] : [-(status(_84399, _84397, tau)), model(257 ^ [_84397, _84399], _84399), model(257 ^ [_84397, _84399], _84397)], (290 ^ _75137) ^ [_85507, _85509] : [status(_85509, _85507, wtc), 294 ^ _75137 : [(295 ^ _75137) ^ [] : [-(model(293 ^ [_85507, _85509], _85509))], (298 ^ _75137) ^ [] : [model(296 ^ [_85507, _85509], _85509)], (300 ^ _75137) ^ [_85886] : [-(model(_85886, _85507))]]], (275 ^ _75137) ^ [_85061, _85063] : [-(status(_85063, _85061, wtc)), 278 ^ _75137 : [(279 ^ _75137) ^ [_85190] : [model(_85190, _85063)]], 282 ^ _75137 : [(283 ^ _75137) ^ [_85286] : [-(model(_85286, _85063))]], model(284 ^ [_85061, _85063], _85061)], (327 ^ _75137) ^ [_86817, _86819] : [status(_86819, _86817, wth), 331 ^ _75137 : [(332 ^ _75137) ^ [] : [-(model(330 ^ [_86817, _86819], _86819))], (341 ^ _75137) ^ [] : [-(model(339 ^ [_86817, _86819], _86817))], (343 ^ _75137) ^ [] : [model(339 ^ [_86817, _86819], _86819)], (346 ^ _75137) ^ [] : [model(344 ^ [_86817, _86819], _86817)], (334 ^ _75137) ^ [_87137] : [model(_87137, _86819), -(model(_87137, _86817))]]], (302 ^ _75137) ^ [_86037, _86039] : [-(status(_86039, _86037, wth)), 305 ^ _75137 : [(306 ^ _75137) ^ [_86191] : [model(_86191, _86039)]], 310 ^ _75137 : [(311 ^ _75137) ^ [] : [-(model(309 ^ [_86037, _86039], _86039))], (313 ^ _75137) ^ [] : [model(309 ^ [_86037, _86039], _86037)]], 322 ^ _75137 : [(323 ^ _75137) ^ [_86687] : [-(model(_86687, _86037))]], 316 ^ _75137 : [(317 ^ _75137) ^ [_86514] : [model(_86514, _86037), -(model(_86514, _86039))]]], (348 ^ _75137) ^ [_87704, _87706] : [-(model(349 ^ [_87704, _87706], _87706)), -(status(_87706, _87704, cax))], (355 ^ _75137) ^ [_87928, _87930] : [status(_87930, _87928, cax), 358 ^ _75137 : [(359 ^ _75137) ^ [_88047] : [model(_88047, _87930)]]], (372 ^ _75137) ^ [_88529, _88531] : [status(_88531, _88529, sca), 375 ^ _75137 : [(376 ^ _75137) ^ [_88679] : [model(_88679, _88531)], (379 ^ _75137) ^ [] : [-(model(377 ^ [_88529, _88531], _88529))]]], (361 ^ _75137) ^ [_88194, _88196] : [-(status(_88196, _88194, sca)), -(model(364 ^ [_88194, _88196], _88196)), 367 ^ _75137 : [(368 ^ _75137) ^ [_88410] : [model(_88410, _88194)]]], (393 ^ _75137) ^ [_89296, _89298] : [status(_89298, _89296, tca), 396 ^ _75137 : [(397 ^ _75137) ^ [_89446] : [model(_89446, _89298)], (399 ^ _75137) ^ [_89508] : [-(model(_89508, _89296))]]], (381 ^ _75137) ^ [_88926, _88928] : [-(status(_88928, _88926, tca)), -(model(384 ^ [_88926, _88928], _88928)), model(387 ^ [_88926, _88928], _88926)], (416 ^ _75137) ^ [_90106, _90108] : [status(_90108, _90106, wca), 419 ^ _75137 : [(420 ^ _75137) ^ [_90269] : [model(_90269, _90108)], (423 ^ _75137) ^ [] : [-(model(421 ^ [_90106, _90108], _90106))], (426 ^ _75137) ^ [] : [model(424 ^ [_90106, _90108], _90106)]]], (401 ^ _75137) ^ [_89657, _89659] : [-(status(_89659, _89657, wca)), -(model(404 ^ [_89657, _89659], _89659)), 409 ^ _75137 : [(410 ^ _75137) ^ [_89920] : [model(_89920, _89657)]], 411 ^ _75137 : [(412 ^ _75137) ^ [_89982] : [-(model(_89982, _89657))]]], (438 ^ _75137) ^ [_90959, _90961] : [status(_90961, _90959, csa), 442 ^ _75137 : [(443 ^ _75137) ^ [] : [-(model(441 ^ [_90959, _90961], _90961))], (445 ^ _75137) ^ [] : [-(model(441 ^ [_90959, _90961], not _90959))]]], (428 ^ _75137) ^ [_90637, _90639] : [-(status(_90639, _90637, csa)), 429 ^ _75137 : [(430 ^ _75137) ^ [_90732] : [model(_90732, _90639), model(_90732, not _90637)]]], (459 ^ _75137) ^ [_91726, _91728] : [status(_91728, _91726, uns), 462 ^ _75137 : [(463 ^ _75137) ^ [_91877] : [-(model(_91877, _91728))], (465 ^ _75137) ^ [_91939] : [-(model(_91939, not _91726))]]], (447 ^ _75137) ^ [_91353, _91355] : [-(status(_91355, _91353, uns)), model(450 ^ [_91353, _91355], _91355), model(453 ^ [_91353, _91355], not _91353)], (485 ^ _75137) ^ [_92633, _92635] : [status(_92635, _92633, noc), 489 ^ _75137 : [(490 ^ _75137) ^ [] : [-(model(488 ^ [_92633, _92635], _92635))], (492 ^ _75137) ^ [] : [-(model(488 ^ [_92633, _92635], _92633))], (495 ^ _75137) ^ [] : [-(model(493 ^ [_92633, _92635], _92635))], (497 ^ _75137) ^ [] : [-(model(493 ^ [_92633, _92635], not _92633))]]], (467 ^ _75137) ^ [_92070, _92072] : [-(status(_92072, _92070, noc)), 470 ^ _75137 : [(471 ^ _75137) ^ [_92216] : [model(_92216, _92072), model(_92216, _92070)]], 476 ^ _75137 : [(477 ^ _75137) ^ [_92401] : [model(_92401, _92072), model(_92401, not _92070)]]]], input).
% 9.70/9.70 ncf('1',plain,[isa(wth, thm)],start(689 ^ 0)).
% 9.70/9.70 ncf('1.1',plain,[-(isa(wth, thm)), 523 : -(status(520 ^ [thm, wth], 521 ^ [thm, wth], wth))],extension(519 ^ 1,bind([[_94211, _94213], [thm, wth]]))).
% 9.70/9.70 ncf('1.1.1',plain,[status(520 ^ [thm, wth], 521 ^ [thm, wth], wth), 334 : model(96 ^ [521 ^ [thm, wth], 520 ^ [thm, wth]], 520 ^ [thm, wth]), 334 : -(model(96 ^ [521 ^ [thm, wth], 520 ^ [thm, wth]], 521 ^ [thm, wth]))],extension(327 ^ 4,bind([[_86817, _86819, _87137], [521 ^ [thm, wth], 520 ^ [thm, wth], 96 ^ [521 ^ [thm, wth], 520 ^ [thm, wth]]]]))).
% 9.70/9.70 ncf('1.1.1.1',plain,[-(model(96 ^ [521 ^ [thm, wth], 520 ^ [thm, wth]], 520 ^ [thm, wth])), -(status(520 ^ [thm, wth], 521 ^ [thm, wth], thm))],extension(95 ^ 7,bind([[_78654, _78656], [521 ^ [thm, wth], 520 ^ [thm, wth]]]))).
% 9.70/9.70 ncf('1.1.1.1.1',plain,[status(520 ^ [thm, wth], 521 ^ [thm, wth], thm)],extension(525 ^ 8)).
% 9.70/9.70 ncf('1.1.1.2',plain,[model(96 ^ [521 ^ [thm, wth], 520 ^ [thm, wth]], 521 ^ [thm, wth]), -(status(520 ^ [thm, wth], 521 ^ [thm, wth], thm))],extension(95 ^ 7,bind([[_78654, _78656], [521 ^ [thm, wth], 520 ^ [thm, wth]]]))).
% 9.70/9.70 ncf('1.1.1.2.1',plain,[status(520 ^ [thm, wth], 521 ^ [thm, wth], thm)],extension(525 ^ 8)).
% 9.70/9.70 %-----------------------------------------------------
% 9.70/9.70 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------