%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS191+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n012.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 0.65s 1.39s
% Output : Proof 0.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS191+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.03/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n012.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 18 22:58:16 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.65/1.39
% 0.65/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.65/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.65/1.39 %-----------------------------------------------------
% 0.65/1.39 ncf(matrix, plain, [(689 ^ _75026) ^ [] : [isa(wtc, thm)], (509 ^ _75026) ^ [_93617, _93619] : [mighta(_93619, _93617), 514 ^ _75026 : [(515 ^ _75026) ^ [] : [-(status(512 ^ [_93617, _93619], 513 ^ [_93617, _93619], _93619))], (517 ^ _75026) ^ [] : [-(status(512 ^ [_93617, _93619], 513 ^ [_93617, _93619], _93617))]]], (499 ^ _75026) ^ [_93272, _93274] : [-(mighta(_93274, _93272)), 500 ^ _75026 : [(501 ^ _75026) ^ [_93385, _93387] : [status(_93387, _93385, _93274), status(_93387, _93385, _93272)]]], (519 ^ _75026) ^ [_94100, _94102] : [522 ^ _75026 : [(523 ^ _75026) ^ [] : [-(status(520 ^ [_94100, _94102], 521 ^ [_94100, _94102], _94102))], (525 ^ _75026) ^ [] : [status(520 ^ [_94100, _94102], 521 ^ [_94100, _94102], _94100)]], -(isa(_94102, _94100))], (529 ^ _75026) ^ [_94504, _94506] : [isa(_94506, _94504), 532 ^ _75026 : [(533 ^ _75026) ^ [_94662, _94664] : [status(_94664, _94662, _94506), -(status(_94664, _94662, _94504))]]], (549 ^ _75026) ^ [_95278, _95280] : [nota(_95280, _95278), 554 ^ _75026 : [(555 ^ _75026) ^ [] : [-(status(552 ^ [_95278, _95280], 553 ^ [_95278, _95280], _95280))], (557 ^ _75026) ^ [] : [status(552 ^ [_95278, _95280], 553 ^ [_95278, _95280], _95278)]]], (539 ^ _75026) ^ [_94928, _94930] : [-(nota(_94930, _94928)), 540 ^ _75026 : [(541 ^ _75026) ^ [_95043, _95045] : [status(_95045, _95043, _94930), -(status(_95045, _95043, _94928))]]], (559 ^ _75026) ^ [_95766, _95768] : [562 ^ _75026 : [(563 ^ _75026) ^ [] : [-(status(560 ^ [_95766, _95768], 561 ^ [_95766, _95768], _95768))], (565 ^ _75026) ^ [] : [-(status(560 ^ [_95766, _95768], 561 ^ [_95766, _95768], _95766))]], -(nevera(_95768, _95766))], (569 ^ _75026) ^ [_96177, _96179] : [nevera(_96179, _96177), 572 ^ _75026 : [(573 ^ _75026) ^ [_96337, _96339] : [status(_96339, _96337, _96179), status(_96339, _96337, _96177)]]], (597 ^ _75026) ^ [_97220, _97222] : [xora(_97222, _97220), 600 ^ _75026 : [(601 ^ _75026) ^ [_97389, _97391] : [602 ^ _75026 : [(603 ^ _75026) ^ [] : [-(status(_97391, _97389, _97222))], (605 ^ _75026) ^ [] : [status(_97391, _97389, _97220)]], 606 ^ _75026 : [(607 ^ _75026) ^ [] : [-(status(_97391, _97389, _97220))], (609 ^ _75026) ^ [] : [status(_97391, _97389, _97222)]]]]], (579 ^ _75026) ^ [_96604, _96606] : [-(xora(_96606, _96604)), 582 ^ _75026 : [(583 ^ _75026) ^ [] : [status(580 ^ [_96604, _96606], 581 ^ [_96604, _96606], _96606), -(status(580 ^ [_96604, _96606], 581 ^ [_96604, _96606], _96604))], (589 ^ _75026) ^ [] : [status(580 ^ [_96604, _96606], 581 ^ [_96604, _96606], _96604), -(status(580 ^ [_96604, _96606], 581 ^ [_96604, _96606], _96606))]]], (611 ^ _75026) ^ [_97796, _97798] : [612 ^ _75026 : [(613 ^ _75026) ^ [] : [-(model(_97798, _97796))], (615 ^ _75026) ^ [] : [model(_97798, not _97796)]], 616 ^ _75026 : [(617 ^ _75026) ^ [] : [-(model(_97798, not _97796))], (619 ^ _75026) ^ [] : [model(_97798, _97796)]]], (621 ^ _75026) ^ [_98192, _98194] : [model(_98194, _98192), model(_98194, not _98192)], (627 ^ _75026) ^ [_98359, _98361] : [-(model(_98361, not _98359)), -(model(_98361, _98359))], (634 ^ _75026) ^ [_98591] : [-(model(_98591, 632 ^ []))], (638 ^ _75026) ^ [] : [-(model(636 ^ [], 635 ^ []))], (641 ^ _75026) ^ [] : [model(639 ^ [], 635 ^ [])], (644 ^ _75026) ^ [_98950] : [model(_98950, 642 ^ [])], (649 ^ _75026) ^ [] : [-(model(647 ^ [], 645 ^ []))], (651 ^ _75026) ^ [] : [-(model(647 ^ [], 646 ^ []))], (654 ^ _75026) ^ [] : [model(652 ^ [], 645 ^ []), model(652 ^ [], 646 ^ [])], (682 ^ _75026) ^ [] : [-(model(678 ^ [], 679 ^ []))], (684 ^ _75026) ^ [] : [model(678 ^ [], 680 ^ [])], (687 ^ _75026) ^ [] : [-(model(685 ^ [], 680 ^ []))], (663 ^ _75026) ^ [] : [-(model(661 ^ [], 659 ^ []))], (672 ^ _75026) ^ [] : [model(670 ^ [], 659 ^ [])], (674 ^ _75026) ^ [] : [-(model(670 ^ [], 660 ^ []))], (677 ^ _75026) ^ [] : [model(675 ^ [], 660 ^ [])], (665 ^ _75026) ^ [_99803] : [model(_99803, 659 ^ []), -(model(_99803, 660 ^ []))], (2 ^ _75026) ^ [_75188, _75190] : [3 ^ _75026 : [(4 ^ _75026) ^ [_75294] : [model(_75294, _75190)], (7 ^ _75026) ^ [] : [-(model(5 ^ [_75188, _75190], _75188))]], -(status(_75190, _75188, unp))], (11 ^ _75026) ^ [_75509, _75511] : [status(_75511, _75509, unp), -(model(16 ^ [_75509, _75511], _75511)), 19 ^ _75026 : [(20 ^ _75026) ^ [_75773] : [model(_75773, _75509)]]], (22 ^ _75026) ^ [_75924, _75926] : [24 ^ _75026 : [(25 ^ _75026) ^ [] : [-(model(23 ^ [_75924, _75926], _75926))], (27 ^ _75026) ^ [_76124] : [model(_76124, _75924)]], -(status(_75926, _75924, sap))], (31 ^ _75026) ^ [_76241, _76243] : [status(_76243, _76241, sap), 36 ^ _75026 : [(37 ^ _75026) ^ [_76403] : [model(_76403, _76243)]], -(model(38 ^ [_76241, _76243], _76241))], (42 ^ _75026) ^ [_76652, _76654] : [-(status(_76654, _76652, esa)), 46 ^ _75026 : [(47 ^ _75026) ^ [] : [-(model(45 ^ [_76652, _76654], _76654))], (49 ^ _75026) ^ [_76895] : [model(_76895, _76652)]], 51 ^ _75026 : [(52 ^ _75026) ^ [] : [-(model(50 ^ [_76652, _76654], _76652))], (54 ^ _75026) ^ [_77076] : [model(_77076, _76654)]]], (58 ^ _75026) ^ [_77198, _77200] : [status(_77200, _77198, esa), 61 ^ _75026 : [(62 ^ _75026) ^ [] : [63 ^ _75026 : [(64 ^ _75026) ^ [_77389] : [model(_77389, _77200)]], -(model(65 ^ [_77198, _77200], _77198))], (69 ^ _75026) ^ [] : [70 ^ _75026 : [(71 ^ _75026) ^ [_77587] : [model(_77587, _77198)]], -(model(72 ^ [_77198, _77200], _77200))]]], (86 ^ _75026) ^ [_78155, _78157] : [status(_78157, _78155, sat), 90 ^ _75026 : [(91 ^ _75026) ^ [] : [-(model(89 ^ [_78155, _78157], _78157))], (93 ^ _75026) ^ [] : [-(model(89 ^ [_78155, _78157], _78155))]]], (76 ^ _75026) ^ [_77839, _77841] : [-(status(_77841, _77839, sat)), 77 ^ _75026 : [(78 ^ _75026) ^ [_77932] : [model(_77932, _77841), model(_77932, _77839)]]], (95 ^ _75026) ^ [_78543, _78545] : [97 ^ _75026 : [(98 ^ _75026) ^ [] : [-(model(96 ^ [_78543, _78545], _78545))], (100 ^ _75026) ^ [] : [model(96 ^ [_78543, _78545], _78543)]], -(status(_78545, _78543, thm))], (104 ^ _75026) ^ [_78852, _78854] : [status(_78854, _78852, thm), 107 ^ _75026 : [(108 ^ _75026) ^ [_78991] : [model(_78991, _78854), -(model(_78991, _78852))]]], (114 ^ _75026) ^ [_79247, _79249] : [-(status(_79249, _79247, eqv)), 117 ^ _75026 : [(118 ^ _75026) ^ [_79369] : [model(_79369, _79249)]], 122 ^ _75026 : [(123 ^ _75026) ^ [] : [-(model(119 ^ [_79247, _79249], _79249))], (125 ^ _75026) ^ [] : [model(119 ^ [_79247, _79249], _79247)]], 126 ^ _75026 : [(127 ^ _75026) ^ [] : [-(model(119 ^ [_79247, _79249], _79247))], (129 ^ _75026) ^ [] : [model(119 ^ [_79247, _79249], _79249)]]], (133 ^ _75026) ^ [_79842, _79844] : [status(_79844, _79842, eqv), 137 ^ _75026 : [(138 ^ _75026) ^ [] : [-(model(136 ^ [_79842, _79844], _79844))], (140 ^ _75026) ^ [_80139] : [model(_80139, _79844), -(model(_80139, _79842))], (146 ^ _75026) ^ [_80311] : [model(_80311, _79842), -(model(_80311, _79844))]]], (163 ^ _75026) ^ [_80903, _80905] : [status(_80905, _80903, tac), 167 ^ _75026 : [(168 ^ _75026) ^ [] : [-(model(166 ^ [_80903, _80905], _80905))], (170 ^ _75026) ^ [_81150] : [-(model(_81150, _80903))]]], (152 ^ _75026) ^ [_80571, _80573] : [-(status(_80573, _80571, tac)), 155 ^ _75026 : [(156 ^ _75026) ^ [_80687] : [model(_80687, _80573)]], model(157 ^ [_80571, _80573], _80571)], (193 ^ _75026) ^ [_81965, _81967] : [status(_81967, _81965, wec), 197 ^ _75026 : [(198 ^ _75026) ^ [] : [-(model(196 ^ [_81965, _81967], _81967))], (207 ^ _75026) ^ [] : [-(model(205 ^ [_81965, _81967], _81965))], (209 ^ _75026) ^ [] : [model(205 ^ [_81965, _81967], _81967)], (200 ^ _75026) ^ [_82272] : [model(_82272, _81967), -(model(_82272, _81965))]]], (172 ^ _75026) ^ [_81299, _81301] : [-(status(_81301, _81299, wec)), 175 ^ _75026 : [(176 ^ _75026) ^ [_81440] : [model(_81440, _81301)]], 180 ^ _75026 : [(181 ^ _75026) ^ [] : [-(model(179 ^ [_81299, _81301], _81301))], (183 ^ _75026) ^ [] : [model(179 ^ [_81299, _81301], _81299)]], 184 ^ _75026 : [(185 ^ _75026) ^ [_81729] : [model(_81729, _81299), -(model(_81729, _81301))]]], (211 ^ _75026) ^ [_82714, _82716] : [-(status(_82716, _82714, eth)), 214 ^ _75026 : [(215 ^ _75026) ^ [_82849] : [model(_82849, _82716)]], 218 ^ _75026 : [(219 ^ _75026) ^ [_82945] : [-(model(_82945, _82716))]], 223 ^ _75026 : [(224 ^ _75026) ^ [] : [-(model(220 ^ [_82714, _82716], _82716))], (226 ^ _75026) ^ [] : [model(220 ^ [_82714, _82716], _82714)]], 227 ^ _75026 : [(228 ^ _75026) ^ [] : [-(model(220 ^ [_82714, _82716], _82714))], (230 ^ _75026) ^ [] : [model(220 ^ [_82714, _82716], _82716)]]], (234 ^ _75026) ^ [_83423, _83425] : [status(_83425, _83423, eth), 238 ^ _75026 : [(239 ^ _75026) ^ [] : [-(model(237 ^ [_83423, _83425], _83425))], (242 ^ _75026) ^ [] : [model(240 ^ [_83423, _83425], _83425)], (244 ^ _75026) ^ [_83852] : [model(_83852, _83425), -(model(_83852, _83423))], (250 ^ _75026) ^ [_84024] : [model(_84024, _83423), -(model(_84024, _83425))]]], (267 ^ _75026) ^ [_84609, _84611] : [status(_84611, _84609, tau), 270 ^ _75026 : [(271 ^ _75026) ^ [_84753] : [-(model(_84753, _84611))], (273 ^ _75026) ^ [_84801] : [-(model(_84801, _84609))]]], (256 ^ _75026) ^ [_84286, _84288] : [-(status(_84288, _84286, tau)), model(257 ^ [_84286, _84288], _84288), model(257 ^ [_84286, _84288], _84286)], (290 ^ _75026) ^ [_85396, _85398] : [status(_85398, _85396, wtc), 294 ^ _75026 : [(295 ^ _75026) ^ [] : [-(model(293 ^ [_85396, _85398], _85398))], (298 ^ _75026) ^ [] : [model(296 ^ [_85396, _85398], _85398)], (300 ^ _75026) ^ [_85775] : [-(model(_85775, _85396))]]], (275 ^ _75026) ^ [_84950, _84952] : [-(status(_84952, _84950, wtc)), 278 ^ _75026 : [(279 ^ _75026) ^ [_85079] : [model(_85079, _84952)]], 282 ^ _75026 : [(283 ^ _75026) ^ [_85175] : [-(model(_85175, _84952))]], model(284 ^ [_84950, _84952], _84950)], (327 ^ _75026) ^ [_86706, _86708] : [status(_86708, _86706, wth), 331 ^ _75026 : [(332 ^ _75026) ^ [] : [-(model(330 ^ [_86706, _86708], _86708))], (341 ^ _75026) ^ [] : [-(model(339 ^ [_86706, _86708], _86706))], (343 ^ _75026) ^ [] : [model(339 ^ [_86706, _86708], _86708)], (346 ^ _75026) ^ [] : [model(344 ^ [_86706, _86708], _86706)], (334 ^ _75026) ^ [_87026] : [model(_87026, _86708), -(model(_87026, _86706))]]], (302 ^ _75026) ^ [_85926, _85928] : [-(status(_85928, _85926, wth)), 305 ^ _75026 : [(306 ^ _75026) ^ [_86080] : [model(_86080, _85928)]], 310 ^ _75026 : [(311 ^ _75026) ^ [] : [-(model(309 ^ [_85926, _85928], _85928))], (313 ^ _75026) ^ [] : [model(309 ^ [_85926, _85928], _85926)]], 322 ^ _75026 : [(323 ^ _75026) ^ [_86576] : [-(model(_86576, _85926))]], 316 ^ _75026 : [(317 ^ _75026) ^ [_86403] : [model(_86403, _85926), -(model(_86403, _85928))]]], (348 ^ _75026) ^ [_87593, _87595] : [-(model(349 ^ [_87593, _87595], _87595)), -(status(_87595, _87593, cax))], (355 ^ _75026) ^ [_87817, _87819] : [status(_87819, _87817, cax), 358 ^ _75026 : [(359 ^ _75026) ^ [_87936] : [model(_87936, _87819)]]], (372 ^ _75026) ^ [_88418, _88420] : [status(_88420, _88418, sca), 375 ^ _75026 : [(376 ^ _75026) ^ [_88568] : [model(_88568, _88420)], (379 ^ _75026) ^ [] : [-(model(377 ^ [_88418, _88420], _88418))]]], (361 ^ _75026) ^ [_88083, _88085] : [-(status(_88085, _88083, sca)), -(model(364 ^ [_88083, _88085], _88085)), 367 ^ _75026 : [(368 ^ _75026) ^ [_88299] : [model(_88299, _88083)]]], (393 ^ _75026) ^ [_89185, _89187] : [status(_89187, _89185, tca), 396 ^ _75026 : [(397 ^ _75026) ^ [_89335] : [model(_89335, _89187)], (399 ^ _75026) ^ [_89397] : [-(model(_89397, _89185))]]], (381 ^ _75026) ^ [_88815, _88817] : [-(status(_88817, _88815, tca)), -(model(384 ^ [_88815, _88817], _88817)), model(387 ^ [_88815, _88817], _88815)], (416 ^ _75026) ^ [_89995, _89997] : [status(_89997, _89995, wca), 419 ^ _75026 : [(420 ^ _75026) ^ [_90158] : [model(_90158, _89997)], (423 ^ _75026) ^ [] : [-(model(421 ^ [_89995, _89997], _89995))], (426 ^ _75026) ^ [] : [model(424 ^ [_89995, _89997], _89995)]]], (401 ^ _75026) ^ [_89546, _89548] : [-(status(_89548, _89546, wca)), -(model(404 ^ [_89546, _89548], _89548)), 409 ^ _75026 : [(410 ^ _75026) ^ [_89809] : [model(_89809, _89546)]], 411 ^ _75026 : [(412 ^ _75026) ^ [_89871] : [-(model(_89871, _89546))]]], (438 ^ _75026) ^ [_90848, _90850] : [status(_90850, _90848, csa), 442 ^ _75026 : [(443 ^ _75026) ^ [] : [-(model(441 ^ [_90848, _90850], _90850))], (445 ^ _75026) ^ [] : [-(model(441 ^ [_90848, _90850], not _90848))]]], (428 ^ _75026) ^ [_90526, _90528] : [-(status(_90528, _90526, csa)), 429 ^ _75026 : [(430 ^ _75026) ^ [_90621] : [model(_90621, _90528), model(_90621, not _90526)]]], (459 ^ _75026) ^ [_91615, _91617] : [status(_91617, _91615, uns), 462 ^ _75026 : [(463 ^ _75026) ^ [_91766] : [-(model(_91766, _91617))], (465 ^ _75026) ^ [_91828] : [-(model(_91828, not _91615))]]], (447 ^ _75026) ^ [_91242, _91244] : [-(status(_91244, _91242, uns)), model(450 ^ [_91242, _91244], _91244), model(453 ^ [_91242, _91244], not _91242)], (485 ^ _75026) ^ [_92522, _92524] : [status(_92524, _92522, noc), 489 ^ _75026 : [(490 ^ _75026) ^ [] : [-(model(488 ^ [_92522, _92524], _92524))], (492 ^ _75026) ^ [] : [-(model(488 ^ [_92522, _92524], _92522))], (495 ^ _75026) ^ [] : [-(model(493 ^ [_92522, _92524], _92524))], (497 ^ _75026) ^ [] : [-(model(493 ^ [_92522, _92524], not _92522))]]], (467 ^ _75026) ^ [_91959, _91961] : [-(status(_91961, _91959, noc)), 470 ^ _75026 : [(471 ^ _75026) ^ [_92105] : [model(_92105, _91961), model(_92105, _91959)]], 476 ^ _75026 : [(477 ^ _75026) ^ [_92290] : [model(_92290, _91961), model(_92290, not _91959)]]]], input).
% 0.65/1.39 ncf('1',plain,[nota(wtc, thm), 557 : status(552 ^ [thm, wtc], 553 ^ [thm, wtc], thm)],start(549 ^ 0,bind([[_95278, _95280], [thm, wtc]]))).
% 0.65/1.39 ncf('1.1',plain,[-(nota(wtc, thm)), 541 : status(520 ^ [thm, wtc], 521 ^ [thm, wtc], wtc), 541 : -(status(520 ^ [thm, wtc], 521 ^ [thm, wtc], thm))],extension(539 ^ 1,bind([[_94928, _94930, _95043, _95045], [thm, wtc, 521 ^ [thm, wtc], 520 ^ [thm, wtc]]]))).
% 0.65/1.39 ncf('1.1.1',plain,[-(status(520 ^ [thm, wtc], 521 ^ [thm, wtc], wtc)), -(isa(wtc, thm))],extension(519 ^ 4,bind([[_94100, _94102], [thm, wtc]]))).
% 0.65/1.39 ncf('1.1.1.1',plain,[isa(wtc, thm)],extension(689 ^ 5)).
% 0.65/1.39 ncf('1.1.2',plain,[status(520 ^ [thm, wtc], 521 ^ [thm, wtc], thm), -(isa(wtc, thm))],extension(519 ^ 4,bind([[_94100, _94102], [thm, wtc]]))).
% 0.65/1.39 ncf('1.1.2.1',plain,[isa(wtc, thm)],extension(689 ^ 5)).
% 0.65/1.39 ncf('1.2',plain,[-(status(552 ^ [thm, wtc], 553 ^ [thm, wtc], thm)), 100 : model(96 ^ [553 ^ [thm, wtc], 552 ^ [thm, wtc]], 553 ^ [thm, wtc])],extension(95 ^ 3,bind([[_78543, _78545], [553 ^ [thm, wtc], 552 ^ [thm, wtc]]]))).
% 0.65/1.39 ncf('1.2.1',plain,[-(model(96 ^ [553 ^ [thm, wtc], 552 ^ [thm, wtc]], 553 ^ [thm, wtc])), status(552 ^ [thm, wtc], 553 ^ [thm, wtc], wtc)],extension(290 ^ 6,bind([[_85396, _85398, _85775], [553 ^ [thm, wtc], 552 ^ [thm, wtc], 96 ^ [553 ^ [thm, wtc], 552 ^ [thm, wtc]]]]))).
% 0.65/1.39 ncf('1.2.1.1',plain,[-(status(552 ^ [thm, wtc], 553 ^ [thm, wtc], wtc))],extension(555 ^ 7)).
% 0.65/1.39 %-----------------------------------------------------
% 0.65/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------