%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS186+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n015.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.85s 9.64s
% Output : Proof 8.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS186+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n015.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:17:07 EDT 2023
% 0.12/0.33 % CPUTime :
% 8.85/9.64
% 8.85/9.64 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 8.85/9.64 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.85/9.64 %-----------------------------------------------------
% 8.85/9.64 ncf(matrix, plain, [(689 ^ _75038) ^ [] : [isa(eqv, thm)], (509 ^ _75038) ^ [_93629, _93631] : [mighta(_93631, _93629), 514 ^ _75038 : [(515 ^ _75038) ^ [] : [-(status(512 ^ [_93629, _93631], 513 ^ [_93629, _93631], _93631))], (517 ^ _75038) ^ [] : [-(status(512 ^ [_93629, _93631], 513 ^ [_93629, _93631], _93629))]]], (499 ^ _75038) ^ [_93284, _93286] : [-(mighta(_93286, _93284)), 500 ^ _75038 : [(501 ^ _75038) ^ [_93397, _93399] : [status(_93399, _93397, _93286), status(_93399, _93397, _93284)]]], (519 ^ _75038) ^ [_94112, _94114] : [522 ^ _75038 : [(523 ^ _75038) ^ [] : [-(status(520 ^ [_94112, _94114], 521 ^ [_94112, _94114], _94114))], (525 ^ _75038) ^ [] : [status(520 ^ [_94112, _94114], 521 ^ [_94112, _94114], _94112)]], -(isa(_94114, _94112))], (529 ^ _75038) ^ [_94516, _94518] : [isa(_94518, _94516), 532 ^ _75038 : [(533 ^ _75038) ^ [_94674, _94676] : [status(_94676, _94674, _94518), -(status(_94676, _94674, _94516))]]], (549 ^ _75038) ^ [_95290, _95292] : [nota(_95292, _95290), 554 ^ _75038 : [(555 ^ _75038) ^ [] : [-(status(552 ^ [_95290, _95292], 553 ^ [_95290, _95292], _95292))], (557 ^ _75038) ^ [] : [status(552 ^ [_95290, _95292], 553 ^ [_95290, _95292], _95290)]]], (539 ^ _75038) ^ [_94940, _94942] : [-(nota(_94942, _94940)), 540 ^ _75038 : [(541 ^ _75038) ^ [_95055, _95057] : [status(_95057, _95055, _94942), -(status(_95057, _95055, _94940))]]], (559 ^ _75038) ^ [_95778, _95780] : [562 ^ _75038 : [(563 ^ _75038) ^ [] : [-(status(560 ^ [_95778, _95780], 561 ^ [_95778, _95780], _95780))], (565 ^ _75038) ^ [] : [-(status(560 ^ [_95778, _95780], 561 ^ [_95778, _95780], _95778))]], -(nevera(_95780, _95778))], (569 ^ _75038) ^ [_96189, _96191] : [nevera(_96191, _96189), 572 ^ _75038 : [(573 ^ _75038) ^ [_96349, _96351] : [status(_96351, _96349, _96191), status(_96351, _96349, _96189)]]], (597 ^ _75038) ^ [_97232, _97234] : [xora(_97234, _97232), 600 ^ _75038 : [(601 ^ _75038) ^ [_97401, _97403] : [602 ^ _75038 : [(603 ^ _75038) ^ [] : [-(status(_97403, _97401, _97234))], (605 ^ _75038) ^ [] : [status(_97403, _97401, _97232)]], 606 ^ _75038 : [(607 ^ _75038) ^ [] : [-(status(_97403, _97401, _97232))], (609 ^ _75038) ^ [] : [status(_97403, _97401, _97234)]]]]], (579 ^ _75038) ^ [_96616, _96618] : [-(xora(_96618, _96616)), 582 ^ _75038 : [(583 ^ _75038) ^ [] : [status(580 ^ [_96616, _96618], 581 ^ [_96616, _96618], _96618), -(status(580 ^ [_96616, _96618], 581 ^ [_96616, _96618], _96616))], (589 ^ _75038) ^ [] : [status(580 ^ [_96616, _96618], 581 ^ [_96616, _96618], _96616), -(status(580 ^ [_96616, _96618], 581 ^ [_96616, _96618], _96618))]]], (611 ^ _75038) ^ [_97808, _97810] : [612 ^ _75038 : [(613 ^ _75038) ^ [] : [-(model(_97810, _97808))], (615 ^ _75038) ^ [] : [model(_97810, not _97808)]], 616 ^ _75038 : [(617 ^ _75038) ^ [] : [-(model(_97810, not _97808))], (619 ^ _75038) ^ [] : [model(_97810, _97808)]]], (621 ^ _75038) ^ [_98204, _98206] : [model(_98206, _98204), model(_98206, not _98204)], (627 ^ _75038) ^ [_98371, _98373] : [-(model(_98373, not _98371)), -(model(_98373, _98371))], (634 ^ _75038) ^ [_98603] : [-(model(_98603, 632 ^ []))], (638 ^ _75038) ^ [] : [-(model(636 ^ [], 635 ^ []))], (641 ^ _75038) ^ [] : [model(639 ^ [], 635 ^ [])], (644 ^ _75038) ^ [_98962] : [model(_98962, 642 ^ [])], (649 ^ _75038) ^ [] : [-(model(647 ^ [], 645 ^ []))], (651 ^ _75038) ^ [] : [-(model(647 ^ [], 646 ^ []))], (654 ^ _75038) ^ [] : [model(652 ^ [], 645 ^ []), model(652 ^ [], 646 ^ [])], (682 ^ _75038) ^ [] : [-(model(678 ^ [], 679 ^ []))], (684 ^ _75038) ^ [] : [model(678 ^ [], 680 ^ [])], (687 ^ _75038) ^ [] : [-(model(685 ^ [], 680 ^ []))], (663 ^ _75038) ^ [] : [-(model(661 ^ [], 659 ^ []))], (672 ^ _75038) ^ [] : [model(670 ^ [], 659 ^ [])], (674 ^ _75038) ^ [] : [-(model(670 ^ [], 660 ^ []))], (677 ^ _75038) ^ [] : [model(675 ^ [], 660 ^ [])], (665 ^ _75038) ^ [_99815] : [model(_99815, 659 ^ []), -(model(_99815, 660 ^ []))], (2 ^ _75038) ^ [_75200, _75202] : [3 ^ _75038 : [(4 ^ _75038) ^ [_75306] : [model(_75306, _75202)], (7 ^ _75038) ^ [] : [-(model(5 ^ [_75200, _75202], _75200))]], -(status(_75202, _75200, unp))], (11 ^ _75038) ^ [_75521, _75523] : [status(_75523, _75521, unp), -(model(16 ^ [_75521, _75523], _75523)), 19 ^ _75038 : [(20 ^ _75038) ^ [_75785] : [model(_75785, _75521)]]], (22 ^ _75038) ^ [_75936, _75938] : [24 ^ _75038 : [(25 ^ _75038) ^ [] : [-(model(23 ^ [_75936, _75938], _75938))], (27 ^ _75038) ^ [_76136] : [model(_76136, _75936)]], -(status(_75938, _75936, sap))], (31 ^ _75038) ^ [_76253, _76255] : [status(_76255, _76253, sap), 36 ^ _75038 : [(37 ^ _75038) ^ [_76415] : [model(_76415, _76255)]], -(model(38 ^ [_76253, _76255], _76253))], (42 ^ _75038) ^ [_76664, _76666] : [-(status(_76666, _76664, esa)), 46 ^ _75038 : [(47 ^ _75038) ^ [] : [-(model(45 ^ [_76664, _76666], _76666))], (49 ^ _75038) ^ [_76907] : [model(_76907, _76664)]], 51 ^ _75038 : [(52 ^ _75038) ^ [] : [-(model(50 ^ [_76664, _76666], _76664))], (54 ^ _75038) ^ [_77088] : [model(_77088, _76666)]]], (58 ^ _75038) ^ [_77210, _77212] : [status(_77212, _77210, esa), 61 ^ _75038 : [(62 ^ _75038) ^ [] : [63 ^ _75038 : [(64 ^ _75038) ^ [_77401] : [model(_77401, _77212)]], -(model(65 ^ [_77210, _77212], _77210))], (69 ^ _75038) ^ [] : [70 ^ _75038 : [(71 ^ _75038) ^ [_77599] : [model(_77599, _77210)]], -(model(72 ^ [_77210, _77212], _77212))]]], (86 ^ _75038) ^ [_78167, _78169] : [status(_78169, _78167, sat), 90 ^ _75038 : [(91 ^ _75038) ^ [] : [-(model(89 ^ [_78167, _78169], _78169))], (93 ^ _75038) ^ [] : [-(model(89 ^ [_78167, _78169], _78167))]]], (76 ^ _75038) ^ [_77851, _77853] : [-(status(_77853, _77851, sat)), 77 ^ _75038 : [(78 ^ _75038) ^ [_77944] : [model(_77944, _77853), model(_77944, _77851)]]], (95 ^ _75038) ^ [_78555, _78557] : [97 ^ _75038 : [(98 ^ _75038) ^ [] : [-(model(96 ^ [_78555, _78557], _78557))], (100 ^ _75038) ^ [] : [model(96 ^ [_78555, _78557], _78555)]], -(status(_78557, _78555, thm))], (104 ^ _75038) ^ [_78864, _78866] : [status(_78866, _78864, thm), 107 ^ _75038 : [(108 ^ _75038) ^ [_79003] : [model(_79003, _78866), -(model(_79003, _78864))]]], (114 ^ _75038) ^ [_79259, _79261] : [-(status(_79261, _79259, eqv)), 117 ^ _75038 : [(118 ^ _75038) ^ [_79381] : [model(_79381, _79261)]], 122 ^ _75038 : [(123 ^ _75038) ^ [] : [-(model(119 ^ [_79259, _79261], _79261))], (125 ^ _75038) ^ [] : [model(119 ^ [_79259, _79261], _79259)]], 126 ^ _75038 : [(127 ^ _75038) ^ [] : [-(model(119 ^ [_79259, _79261], _79259))], (129 ^ _75038) ^ [] : [model(119 ^ [_79259, _79261], _79261)]]], (133 ^ _75038) ^ [_79854, _79856] : [status(_79856, _79854, eqv), 137 ^ _75038 : [(138 ^ _75038) ^ [] : [-(model(136 ^ [_79854, _79856], _79856))], (140 ^ _75038) ^ [_80151] : [model(_80151, _79856), -(model(_80151, _79854))], (146 ^ _75038) ^ [_80323] : [model(_80323, _79854), -(model(_80323, _79856))]]], (163 ^ _75038) ^ [_80915, _80917] : [status(_80917, _80915, tac), 167 ^ _75038 : [(168 ^ _75038) ^ [] : [-(model(166 ^ [_80915, _80917], _80917))], (170 ^ _75038) ^ [_81162] : [-(model(_81162, _80915))]]], (152 ^ _75038) ^ [_80583, _80585] : [-(status(_80585, _80583, tac)), 155 ^ _75038 : [(156 ^ _75038) ^ [_80699] : [model(_80699, _80585)]], model(157 ^ [_80583, _80585], _80583)], (193 ^ _75038) ^ [_81977, _81979] : [status(_81979, _81977, wec), 197 ^ _75038 : [(198 ^ _75038) ^ [] : [-(model(196 ^ [_81977, _81979], _81979))], (207 ^ _75038) ^ [] : [-(model(205 ^ [_81977, _81979], _81977))], (209 ^ _75038) ^ [] : [model(205 ^ [_81977, _81979], _81979)], (200 ^ _75038) ^ [_82284] : [model(_82284, _81979), -(model(_82284, _81977))]]], (172 ^ _75038) ^ [_81311, _81313] : [-(status(_81313, _81311, wec)), 175 ^ _75038 : [(176 ^ _75038) ^ [_81452] : [model(_81452, _81313)]], 180 ^ _75038 : [(181 ^ _75038) ^ [] : [-(model(179 ^ [_81311, _81313], _81313))], (183 ^ _75038) ^ [] : [model(179 ^ [_81311, _81313], _81311)]], 184 ^ _75038 : [(185 ^ _75038) ^ [_81741] : [model(_81741, _81311), -(model(_81741, _81313))]]], (211 ^ _75038) ^ [_82726, _82728] : [-(status(_82728, _82726, eth)), 214 ^ _75038 : [(215 ^ _75038) ^ [_82861] : [model(_82861, _82728)]], 218 ^ _75038 : [(219 ^ _75038) ^ [_82957] : [-(model(_82957, _82728))]], 223 ^ _75038 : [(224 ^ _75038) ^ [] : [-(model(220 ^ [_82726, _82728], _82728))], (226 ^ _75038) ^ [] : [model(220 ^ [_82726, _82728], _82726)]], 227 ^ _75038 : [(228 ^ _75038) ^ [] : [-(model(220 ^ [_82726, _82728], _82726))], (230 ^ _75038) ^ [] : [model(220 ^ [_82726, _82728], _82728)]]], (234 ^ _75038) ^ [_83435, _83437] : [status(_83437, _83435, eth), 238 ^ _75038 : [(239 ^ _75038) ^ [] : [-(model(237 ^ [_83435, _83437], _83437))], (242 ^ _75038) ^ [] : [model(240 ^ [_83435, _83437], _83437)], (244 ^ _75038) ^ [_83864] : [model(_83864, _83437), -(model(_83864, _83435))], (250 ^ _75038) ^ [_84036] : [model(_84036, _83435), -(model(_84036, _83437))]]], (267 ^ _75038) ^ [_84621, _84623] : [status(_84623, _84621, tau), 270 ^ _75038 : [(271 ^ _75038) ^ [_84765] : [-(model(_84765, _84623))], (273 ^ _75038) ^ [_84813] : [-(model(_84813, _84621))]]], (256 ^ _75038) ^ [_84298, _84300] : [-(status(_84300, _84298, tau)), model(257 ^ [_84298, _84300], _84300), model(257 ^ [_84298, _84300], _84298)], (290 ^ _75038) ^ [_85408, _85410] : [status(_85410, _85408, wtc), 294 ^ _75038 : [(295 ^ _75038) ^ [] : [-(model(293 ^ [_85408, _85410], _85410))], (298 ^ _75038) ^ [] : [model(296 ^ [_85408, _85410], _85410)], (300 ^ _75038) ^ [_85787] : [-(model(_85787, _85408))]]], (275 ^ _75038) ^ [_84962, _84964] : [-(status(_84964, _84962, wtc)), 278 ^ _75038 : [(279 ^ _75038) ^ [_85091] : [model(_85091, _84964)]], 282 ^ _75038 : [(283 ^ _75038) ^ [_85187] : [-(model(_85187, _84964))]], model(284 ^ [_84962, _84964], _84962)], (327 ^ _75038) ^ [_86718, _86720] : [status(_86720, _86718, wth), 331 ^ _75038 : [(332 ^ _75038) ^ [] : [-(model(330 ^ [_86718, _86720], _86720))], (341 ^ _75038) ^ [] : [-(model(339 ^ [_86718, _86720], _86718))], (343 ^ _75038) ^ [] : [model(339 ^ [_86718, _86720], _86720)], (346 ^ _75038) ^ [] : [model(344 ^ [_86718, _86720], _86718)], (334 ^ _75038) ^ [_87038] : [model(_87038, _86720), -(model(_87038, _86718))]]], (302 ^ _75038) ^ [_85938, _85940] : [-(status(_85940, _85938, wth)), 305 ^ _75038 : [(306 ^ _75038) ^ [_86092] : [model(_86092, _85940)]], 310 ^ _75038 : [(311 ^ _75038) ^ [] : [-(model(309 ^ [_85938, _85940], _85940))], (313 ^ _75038) ^ [] : [model(309 ^ [_85938, _85940], _85938)]], 322 ^ _75038 : [(323 ^ _75038) ^ [_86588] : [-(model(_86588, _85938))]], 316 ^ _75038 : [(317 ^ _75038) ^ [_86415] : [model(_86415, _85938), -(model(_86415, _85940))]]], (348 ^ _75038) ^ [_87605, _87607] : [-(model(349 ^ [_87605, _87607], _87607)), -(status(_87607, _87605, cax))], (355 ^ _75038) ^ [_87829, _87831] : [status(_87831, _87829, cax), 358 ^ _75038 : [(359 ^ _75038) ^ [_87948] : [model(_87948, _87831)]]], (372 ^ _75038) ^ [_88430, _88432] : [status(_88432, _88430, sca), 375 ^ _75038 : [(376 ^ _75038) ^ [_88580] : [model(_88580, _88432)], (379 ^ _75038) ^ [] : [-(model(377 ^ [_88430, _88432], _88430))]]], (361 ^ _75038) ^ [_88095, _88097] : [-(status(_88097, _88095, sca)), -(model(364 ^ [_88095, _88097], _88097)), 367 ^ _75038 : [(368 ^ _75038) ^ [_88311] : [model(_88311, _88095)]]], (393 ^ _75038) ^ [_89197, _89199] : [status(_89199, _89197, tca), 396 ^ _75038 : [(397 ^ _75038) ^ [_89347] : [model(_89347, _89199)], (399 ^ _75038) ^ [_89409] : [-(model(_89409, _89197))]]], (381 ^ _75038) ^ [_88827, _88829] : [-(status(_88829, _88827, tca)), -(model(384 ^ [_88827, _88829], _88829)), model(387 ^ [_88827, _88829], _88827)], (416 ^ _75038) ^ [_90007, _90009] : [status(_90009, _90007, wca), 419 ^ _75038 : [(420 ^ _75038) ^ [_90170] : [model(_90170, _90009)], (423 ^ _75038) ^ [] : [-(model(421 ^ [_90007, _90009], _90007))], (426 ^ _75038) ^ [] : [model(424 ^ [_90007, _90009], _90007)]]], (401 ^ _75038) ^ [_89558, _89560] : [-(status(_89560, _89558, wca)), -(model(404 ^ [_89558, _89560], _89560)), 409 ^ _75038 : [(410 ^ _75038) ^ [_89821] : [model(_89821, _89558)]], 411 ^ _75038 : [(412 ^ _75038) ^ [_89883] : [-(model(_89883, _89558))]]], (438 ^ _75038) ^ [_90860, _90862] : [status(_90862, _90860, csa), 442 ^ _75038 : [(443 ^ _75038) ^ [] : [-(model(441 ^ [_90860, _90862], _90862))], (445 ^ _75038) ^ [] : [-(model(441 ^ [_90860, _90862], not _90860))]]], (428 ^ _75038) ^ [_90538, _90540] : [-(status(_90540, _90538, csa)), 429 ^ _75038 : [(430 ^ _75038) ^ [_90633] : [model(_90633, _90540), model(_90633, not _90538)]]], (459 ^ _75038) ^ [_91627, _91629] : [status(_91629, _91627, uns), 462 ^ _75038 : [(463 ^ _75038) ^ [_91778] : [-(model(_91778, _91629))], (465 ^ _75038) ^ [_91840] : [-(model(_91840, not _91627))]]], (447 ^ _75038) ^ [_91254, _91256] : [-(status(_91256, _91254, uns)), model(450 ^ [_91254, _91256], _91256), model(453 ^ [_91254, _91256], not _91254)], (485 ^ _75038) ^ [_92534, _92536] : [status(_92536, _92534, noc), 489 ^ _75038 : [(490 ^ _75038) ^ [] : [-(model(488 ^ [_92534, _92536], _92536))], (492 ^ _75038) ^ [] : [-(model(488 ^ [_92534, _92536], _92534))], (495 ^ _75038) ^ [] : [-(model(493 ^ [_92534, _92536], _92536))], (497 ^ _75038) ^ [] : [-(model(493 ^ [_92534, _92536], not _92534))]]], (467 ^ _75038) ^ [_91971, _91973] : [-(status(_91973, _91971, noc)), 470 ^ _75038 : [(471 ^ _75038) ^ [_92117] : [model(_92117, _91973), model(_92117, _91971)]], 476 ^ _75038 : [(477 ^ _75038) ^ [_92302] : [model(_92302, _91973), model(_92302, not _91971)]]]], input).
% 8.85/9.64 ncf('1',plain,[isa(eqv, thm)],start(689 ^ 0)).
% 8.85/9.64 ncf('1.1',plain,[-(isa(eqv, thm)), 523 : -(status(520 ^ [thm, eqv], 521 ^ [thm, eqv], eqv))],extension(519 ^ 1,bind([[_94112, _94114], [thm, eqv]]))).
% 8.85/9.64 ncf('1.1.1',plain,[status(520 ^ [thm, eqv], 521 ^ [thm, eqv], eqv), 140 : model(96 ^ [521 ^ [thm, eqv], 520 ^ [thm, eqv]], 520 ^ [thm, eqv]), 140 : -(model(96 ^ [521 ^ [thm, eqv], 520 ^ [thm, eqv]], 521 ^ [thm, eqv]))],extension(133 ^ 4,bind([[_79854, _79856, _80151], [521 ^ [thm, eqv], 520 ^ [thm, eqv], 96 ^ [521 ^ [thm, eqv], 520 ^ [thm, eqv]]]]))).
% 8.85/9.64 ncf('1.1.1.1',plain,[-(model(96 ^ [521 ^ [thm, eqv], 520 ^ [thm, eqv]], 520 ^ [thm, eqv])), -(status(520 ^ [thm, eqv], 521 ^ [thm, eqv], thm))],extension(95 ^ 7,bind([[_78555, _78557], [521 ^ [thm, eqv], 520 ^ [thm, eqv]]]))).
% 8.85/9.64 ncf('1.1.1.1.1',plain,[status(520 ^ [thm, eqv], 521 ^ [thm, eqv], thm)],extension(525 ^ 8)).
% 8.85/9.64 ncf('1.1.1.2',plain,[model(96 ^ [521 ^ [thm, eqv], 520 ^ [thm, eqv]], 521 ^ [thm, eqv]), -(status(520 ^ [thm, eqv], 521 ^ [thm, eqv], thm))],extension(95 ^ 7,bind([[_78555, _78557], [521 ^ [thm, eqv], 520 ^ [thm, eqv]]]))).
% 8.85/9.64 ncf('1.1.1.2.1',plain,[status(520 ^ [thm, eqv], 521 ^ [thm, eqv], thm)],extension(525 ^ 8)).
% 8.85/9.64 %-----------------------------------------------------
% 8.85/9.64 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------