%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS265+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n020.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:34 EDT 2023
% Result : Theorem 0.74s 1.38s
% Output : Proof 0.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.12 % Problem : KRS265+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.09/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n020.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 23:07:17 EDT 2023
% 0.13/0.33 % CPUTime :
% 0.74/1.38
% 0.74/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.74/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.74/1.38 %-----------------------------------------------------
% 0.74/1.38 ncf(matrix, plain, [(689 ^ _74346) ^ [] : [mighta(cax, thm)], (509 ^ _74346) ^ [_92937, _92939] : [mighta(_92939, _92937), 514 ^ _74346 : [(515 ^ _74346) ^ [] : [-(status(512 ^ [_92937, _92939], 513 ^ [_92937, _92939], _92939))], (517 ^ _74346) ^ [] : [-(status(512 ^ [_92937, _92939], 513 ^ [_92937, _92939], _92937))]]], (499 ^ _74346) ^ [_92592, _92594] : [-(mighta(_92594, _92592)), 500 ^ _74346 : [(501 ^ _74346) ^ [_92705, _92707] : [status(_92707, _92705, _92594), status(_92707, _92705, _92592)]]], (519 ^ _74346) ^ [_93420, _93422] : [522 ^ _74346 : [(523 ^ _74346) ^ [] : [-(status(520 ^ [_93420, _93422], 521 ^ [_93420, _93422], _93422))], (525 ^ _74346) ^ [] : [status(520 ^ [_93420, _93422], 521 ^ [_93420, _93422], _93420)]], -(isa(_93422, _93420))], (529 ^ _74346) ^ [_93824, _93826] : [isa(_93826, _93824), 532 ^ _74346 : [(533 ^ _74346) ^ [_93982, _93984] : [status(_93984, _93982, _93826), -(status(_93984, _93982, _93824))]]], (549 ^ _74346) ^ [_94598, _94600] : [nota(_94600, _94598), 554 ^ _74346 : [(555 ^ _74346) ^ [] : [-(status(552 ^ [_94598, _94600], 553 ^ [_94598, _94600], _94600))], (557 ^ _74346) ^ [] : [status(552 ^ [_94598, _94600], 553 ^ [_94598, _94600], _94598)]]], (539 ^ _74346) ^ [_94248, _94250] : [-(nota(_94250, _94248)), 540 ^ _74346 : [(541 ^ _74346) ^ [_94363, _94365] : [status(_94365, _94363, _94250), -(status(_94365, _94363, _94248))]]], (559 ^ _74346) ^ [_95086, _95088] : [562 ^ _74346 : [(563 ^ _74346) ^ [] : [-(status(560 ^ [_95086, _95088], 561 ^ [_95086, _95088], _95088))], (565 ^ _74346) ^ [] : [-(status(560 ^ [_95086, _95088], 561 ^ [_95086, _95088], _95086))]], -(nevera(_95088, _95086))], (569 ^ _74346) ^ [_95497, _95499] : [nevera(_95499, _95497), 572 ^ _74346 : [(573 ^ _74346) ^ [_95657, _95659] : [status(_95659, _95657, _95499), status(_95659, _95657, _95497)]]], (597 ^ _74346) ^ [_96540, _96542] : [xora(_96542, _96540), 600 ^ _74346 : [(601 ^ _74346) ^ [_96709, _96711] : [602 ^ _74346 : [(603 ^ _74346) ^ [] : [-(status(_96711, _96709, _96542))], (605 ^ _74346) ^ [] : [status(_96711, _96709, _96540)]], 606 ^ _74346 : [(607 ^ _74346) ^ [] : [-(status(_96711, _96709, _96540))], (609 ^ _74346) ^ [] : [status(_96711, _96709, _96542)]]]]], (579 ^ _74346) ^ [_95924, _95926] : [-(xora(_95926, _95924)), 582 ^ _74346 : [(583 ^ _74346) ^ [] : [status(580 ^ [_95924, _95926], 581 ^ [_95924, _95926], _95926), -(status(580 ^ [_95924, _95926], 581 ^ [_95924, _95926], _95924))], (589 ^ _74346) ^ [] : [status(580 ^ [_95924, _95926], 581 ^ [_95924, _95926], _95924), -(status(580 ^ [_95924, _95926], 581 ^ [_95924, _95926], _95926))]]], (611 ^ _74346) ^ [_97116, _97118] : [612 ^ _74346 : [(613 ^ _74346) ^ [] : [-(model(_97118, _97116))], (615 ^ _74346) ^ [] : [model(_97118, not _97116)]], 616 ^ _74346 : [(617 ^ _74346) ^ [] : [-(model(_97118, not _97116))], (619 ^ _74346) ^ [] : [model(_97118, _97116)]]], (621 ^ _74346) ^ [_97512, _97514] : [model(_97514, _97512), model(_97514, not _97512)], (627 ^ _74346) ^ [_97679, _97681] : [-(model(_97681, not _97679)), -(model(_97681, _97679))], (634 ^ _74346) ^ [_97911] : [-(model(_97911, 632 ^ []))], (638 ^ _74346) ^ [] : [-(model(636 ^ [], 635 ^ []))], (641 ^ _74346) ^ [] : [model(639 ^ [], 635 ^ [])], (644 ^ _74346) ^ [_98270] : [model(_98270, 642 ^ [])], (649 ^ _74346) ^ [] : [-(model(647 ^ [], 645 ^ []))], (651 ^ _74346) ^ [] : [-(model(647 ^ [], 646 ^ []))], (654 ^ _74346) ^ [] : [model(652 ^ [], 645 ^ []), model(652 ^ [], 646 ^ [])], (682 ^ _74346) ^ [] : [-(model(678 ^ [], 679 ^ []))], (684 ^ _74346) ^ [] : [model(678 ^ [], 680 ^ [])], (687 ^ _74346) ^ [] : [-(model(685 ^ [], 680 ^ []))], (663 ^ _74346) ^ [] : [-(model(661 ^ [], 659 ^ []))], (672 ^ _74346) ^ [] : [model(670 ^ [], 659 ^ [])], (674 ^ _74346) ^ [] : [-(model(670 ^ [], 660 ^ []))], (677 ^ _74346) ^ [] : [model(675 ^ [], 660 ^ [])], (665 ^ _74346) ^ [_99123] : [model(_99123, 659 ^ []), -(model(_99123, 660 ^ []))], (2 ^ _74346) ^ [_74508, _74510] : [3 ^ _74346 : [(4 ^ _74346) ^ [_74614] : [model(_74614, _74510)], (7 ^ _74346) ^ [] : [-(model(5 ^ [_74508, _74510], _74508))]], -(status(_74510, _74508, unp))], (11 ^ _74346) ^ [_74829, _74831] : [status(_74831, _74829, unp), -(model(16 ^ [_74829, _74831], _74831)), 19 ^ _74346 : [(20 ^ _74346) ^ [_75093] : [model(_75093, _74829)]]], (22 ^ _74346) ^ [_75244, _75246] : [24 ^ _74346 : [(25 ^ _74346) ^ [] : [-(model(23 ^ [_75244, _75246], _75246))], (27 ^ _74346) ^ [_75444] : [model(_75444, _75244)]], -(status(_75246, _75244, sap))], (31 ^ _74346) ^ [_75561, _75563] : [status(_75563, _75561, sap), 36 ^ _74346 : [(37 ^ _74346) ^ [_75723] : [model(_75723, _75563)]], -(model(38 ^ [_75561, _75563], _75561))], (42 ^ _74346) ^ [_75972, _75974] : [-(status(_75974, _75972, esa)), 46 ^ _74346 : [(47 ^ _74346) ^ [] : [-(model(45 ^ [_75972, _75974], _75974))], (49 ^ _74346) ^ [_76215] : [model(_76215, _75972)]], 51 ^ _74346 : [(52 ^ _74346) ^ [] : [-(model(50 ^ [_75972, _75974], _75972))], (54 ^ _74346) ^ [_76396] : [model(_76396, _75974)]]], (58 ^ _74346) ^ [_76518, _76520] : [status(_76520, _76518, esa), 61 ^ _74346 : [(62 ^ _74346) ^ [] : [63 ^ _74346 : [(64 ^ _74346) ^ [_76709] : [model(_76709, _76520)]], -(model(65 ^ [_76518, _76520], _76518))], (69 ^ _74346) ^ [] : [70 ^ _74346 : [(71 ^ _74346) ^ [_76907] : [model(_76907, _76518)]], -(model(72 ^ [_76518, _76520], _76520))]]], (86 ^ _74346) ^ [_77475, _77477] : [status(_77477, _77475, sat), 90 ^ _74346 : [(91 ^ _74346) ^ [] : [-(model(89 ^ [_77475, _77477], _77477))], (93 ^ _74346) ^ [] : [-(model(89 ^ [_77475, _77477], _77475))]]], (76 ^ _74346) ^ [_77159, _77161] : [-(status(_77161, _77159, sat)), 77 ^ _74346 : [(78 ^ _74346) ^ [_77252] : [model(_77252, _77161), model(_77252, _77159)]]], (95 ^ _74346) ^ [_77863, _77865] : [97 ^ _74346 : [(98 ^ _74346) ^ [] : [-(model(96 ^ [_77863, _77865], _77865))], (100 ^ _74346) ^ [] : [model(96 ^ [_77863, _77865], _77863)]], -(status(_77865, _77863, thm))], (104 ^ _74346) ^ [_78172, _78174] : [status(_78174, _78172, thm), 107 ^ _74346 : [(108 ^ _74346) ^ [_78311] : [model(_78311, _78174), -(model(_78311, _78172))]]], (114 ^ _74346) ^ [_78567, _78569] : [-(status(_78569, _78567, eqv)), 117 ^ _74346 : [(118 ^ _74346) ^ [_78689] : [model(_78689, _78569)]], 122 ^ _74346 : [(123 ^ _74346) ^ [] : [-(model(119 ^ [_78567, _78569], _78569))], (125 ^ _74346) ^ [] : [model(119 ^ [_78567, _78569], _78567)]], 126 ^ _74346 : [(127 ^ _74346) ^ [] : [-(model(119 ^ [_78567, _78569], _78567))], (129 ^ _74346) ^ [] : [model(119 ^ [_78567, _78569], _78569)]]], (133 ^ _74346) ^ [_79162, _79164] : [status(_79164, _79162, eqv), 137 ^ _74346 : [(138 ^ _74346) ^ [] : [-(model(136 ^ [_79162, _79164], _79164))], (140 ^ _74346) ^ [_79459] : [model(_79459, _79164), -(model(_79459, _79162))], (146 ^ _74346) ^ [_79631] : [model(_79631, _79162), -(model(_79631, _79164))]]], (163 ^ _74346) ^ [_80223, _80225] : [status(_80225, _80223, tac), 167 ^ _74346 : [(168 ^ _74346) ^ [] : [-(model(166 ^ [_80223, _80225], _80225))], (170 ^ _74346) ^ [_80470] : [-(model(_80470, _80223))]]], (152 ^ _74346) ^ [_79891, _79893] : [-(status(_79893, _79891, tac)), 155 ^ _74346 : [(156 ^ _74346) ^ [_80007] : [model(_80007, _79893)]], model(157 ^ [_79891, _79893], _79891)], (193 ^ _74346) ^ [_81285, _81287] : [status(_81287, _81285, wec), 197 ^ _74346 : [(198 ^ _74346) ^ [] : [-(model(196 ^ [_81285, _81287], _81287))], (207 ^ _74346) ^ [] : [-(model(205 ^ [_81285, _81287], _81285))], (209 ^ _74346) ^ [] : [model(205 ^ [_81285, _81287], _81287)], (200 ^ _74346) ^ [_81592] : [model(_81592, _81287), -(model(_81592, _81285))]]], (172 ^ _74346) ^ [_80619, _80621] : [-(status(_80621, _80619, wec)), 175 ^ _74346 : [(176 ^ _74346) ^ [_80760] : [model(_80760, _80621)]], 180 ^ _74346 : [(181 ^ _74346) ^ [] : [-(model(179 ^ [_80619, _80621], _80621))], (183 ^ _74346) ^ [] : [model(179 ^ [_80619, _80621], _80619)]], 184 ^ _74346 : [(185 ^ _74346) ^ [_81049] : [model(_81049, _80619), -(model(_81049, _80621))]]], (211 ^ _74346) ^ [_82034, _82036] : [-(status(_82036, _82034, eth)), 214 ^ _74346 : [(215 ^ _74346) ^ [_82169] : [model(_82169, _82036)]], 218 ^ _74346 : [(219 ^ _74346) ^ [_82265] : [-(model(_82265, _82036))]], 223 ^ _74346 : [(224 ^ _74346) ^ [] : [-(model(220 ^ [_82034, _82036], _82036))], (226 ^ _74346) ^ [] : [model(220 ^ [_82034, _82036], _82034)]], 227 ^ _74346 : [(228 ^ _74346) ^ [] : [-(model(220 ^ [_82034, _82036], _82034))], (230 ^ _74346) ^ [] : [model(220 ^ [_82034, _82036], _82036)]]], (234 ^ _74346) ^ [_82743, _82745] : [status(_82745, _82743, eth), 238 ^ _74346 : [(239 ^ _74346) ^ [] : [-(model(237 ^ [_82743, _82745], _82745))], (242 ^ _74346) ^ [] : [model(240 ^ [_82743, _82745], _82745)], (244 ^ _74346) ^ [_83172] : [model(_83172, _82745), -(model(_83172, _82743))], (250 ^ _74346) ^ [_83344] : [model(_83344, _82743), -(model(_83344, _82745))]]], (267 ^ _74346) ^ [_83929, _83931] : [status(_83931, _83929, tau), 270 ^ _74346 : [(271 ^ _74346) ^ [_84073] : [-(model(_84073, _83931))], (273 ^ _74346) ^ [_84121] : [-(model(_84121, _83929))]]], (256 ^ _74346) ^ [_83606, _83608] : [-(status(_83608, _83606, tau)), model(257 ^ [_83606, _83608], _83608), model(257 ^ [_83606, _83608], _83606)], (290 ^ _74346) ^ [_84716, _84718] : [status(_84718, _84716, wtc), 294 ^ _74346 : [(295 ^ _74346) ^ [] : [-(model(293 ^ [_84716, _84718], _84718))], (298 ^ _74346) ^ [] : [model(296 ^ [_84716, _84718], _84718)], (300 ^ _74346) ^ [_85095] : [-(model(_85095, _84716))]]], (275 ^ _74346) ^ [_84270, _84272] : [-(status(_84272, _84270, wtc)), 278 ^ _74346 : [(279 ^ _74346) ^ [_84399] : [model(_84399, _84272)]], 282 ^ _74346 : [(283 ^ _74346) ^ [_84495] : [-(model(_84495, _84272))]], model(284 ^ [_84270, _84272], _84270)], (327 ^ _74346) ^ [_86026, _86028] : [status(_86028, _86026, wth), 331 ^ _74346 : [(332 ^ _74346) ^ [] : [-(model(330 ^ [_86026, _86028], _86028))], (341 ^ _74346) ^ [] : [-(model(339 ^ [_86026, _86028], _86026))], (343 ^ _74346) ^ [] : [model(339 ^ [_86026, _86028], _86028)], (346 ^ _74346) ^ [] : [model(344 ^ [_86026, _86028], _86026)], (334 ^ _74346) ^ [_86346] : [model(_86346, _86028), -(model(_86346, _86026))]]], (302 ^ _74346) ^ [_85246, _85248] : [-(status(_85248, _85246, wth)), 305 ^ _74346 : [(306 ^ _74346) ^ [_85400] : [model(_85400, _85248)]], 310 ^ _74346 : [(311 ^ _74346) ^ [] : [-(model(309 ^ [_85246, _85248], _85248))], (313 ^ _74346) ^ [] : [model(309 ^ [_85246, _85248], _85246)]], 322 ^ _74346 : [(323 ^ _74346) ^ [_85896] : [-(model(_85896, _85246))]], 316 ^ _74346 : [(317 ^ _74346) ^ [_85723] : [model(_85723, _85246), -(model(_85723, _85248))]]], (348 ^ _74346) ^ [_86913, _86915] : [-(model(349 ^ [_86913, _86915], _86915)), -(status(_86915, _86913, cax))], (355 ^ _74346) ^ [_87137, _87139] : [status(_87139, _87137, cax), 358 ^ _74346 : [(359 ^ _74346) ^ [_87256] : [model(_87256, _87139)]]], (372 ^ _74346) ^ [_87738, _87740] : [status(_87740, _87738, sca), 375 ^ _74346 : [(376 ^ _74346) ^ [_87888] : [model(_87888, _87740)], (379 ^ _74346) ^ [] : [-(model(377 ^ [_87738, _87740], _87738))]]], (361 ^ _74346) ^ [_87403, _87405] : [-(status(_87405, _87403, sca)), -(model(364 ^ [_87403, _87405], _87405)), 367 ^ _74346 : [(368 ^ _74346) ^ [_87619] : [model(_87619, _87403)]]], (393 ^ _74346) ^ [_88505, _88507] : [status(_88507, _88505, tca), 396 ^ _74346 : [(397 ^ _74346) ^ [_88655] : [model(_88655, _88507)], (399 ^ _74346) ^ [_88717] : [-(model(_88717, _88505))]]], (381 ^ _74346) ^ [_88135, _88137] : [-(status(_88137, _88135, tca)), -(model(384 ^ [_88135, _88137], _88137)), model(387 ^ [_88135, _88137], _88135)], (416 ^ _74346) ^ [_89315, _89317] : [status(_89317, _89315, wca), 419 ^ _74346 : [(420 ^ _74346) ^ [_89478] : [model(_89478, _89317)], (423 ^ _74346) ^ [] : [-(model(421 ^ [_89315, _89317], _89315))], (426 ^ _74346) ^ [] : [model(424 ^ [_89315, _89317], _89315)]]], (401 ^ _74346) ^ [_88866, _88868] : [-(status(_88868, _88866, wca)), -(model(404 ^ [_88866, _88868], _88868)), 409 ^ _74346 : [(410 ^ _74346) ^ [_89129] : [model(_89129, _88866)]], 411 ^ _74346 : [(412 ^ _74346) ^ [_89191] : [-(model(_89191, _88866))]]], (438 ^ _74346) ^ [_90168, _90170] : [status(_90170, _90168, csa), 442 ^ _74346 : [(443 ^ _74346) ^ [] : [-(model(441 ^ [_90168, _90170], _90170))], (445 ^ _74346) ^ [] : [-(model(441 ^ [_90168, _90170], not _90168))]]], (428 ^ _74346) ^ [_89846, _89848] : [-(status(_89848, _89846, csa)), 429 ^ _74346 : [(430 ^ _74346) ^ [_89941] : [model(_89941, _89848), model(_89941, not _89846)]]], (459 ^ _74346) ^ [_90935, _90937] : [status(_90937, _90935, uns), 462 ^ _74346 : [(463 ^ _74346) ^ [_91086] : [-(model(_91086, _90937))], (465 ^ _74346) ^ [_91148] : [-(model(_91148, not _90935))]]], (447 ^ _74346) ^ [_90562, _90564] : [-(status(_90564, _90562, uns)), model(450 ^ [_90562, _90564], _90564), model(453 ^ [_90562, _90564], not _90562)], (485 ^ _74346) ^ [_91842, _91844] : [status(_91844, _91842, noc), 489 ^ _74346 : [(490 ^ _74346) ^ [] : [-(model(488 ^ [_91842, _91844], _91844))], (492 ^ _74346) ^ [] : [-(model(488 ^ [_91842, _91844], _91842))], (495 ^ _74346) ^ [] : [-(model(493 ^ [_91842, _91844], _91844))], (497 ^ _74346) ^ [] : [-(model(493 ^ [_91842, _91844], not _91842))]]], (467 ^ _74346) ^ [_91279, _91281] : [-(status(_91281, _91279, noc)), 470 ^ _74346 : [(471 ^ _74346) ^ [_91425] : [model(_91425, _91281), model(_91425, _91279)]], 476 ^ _74346 : [(477 ^ _74346) ^ [_91610] : [model(_91610, _91281), model(_91610, not _91279)]]]], input).
% 0.74/1.38 ncf('1',plain,[mighta(cax, thm)],start(689 ^ 0)).
% 0.74/1.38 ncf('1.1',plain,[-(mighta(cax, thm)), 501 : status(642 ^ [], _55990, cax), 501 : status(642 ^ [], _55990, thm)],extension(499 ^ 1,bind([[_92592, _92594, _92705, _92707], [thm, cax, _55990, 642 ^ []]]))).
% 0.74/1.38 ncf('1.1.1',plain,[-(status(642 ^ [], _55990, cax)), -(model(349 ^ [_55990, 642 ^ []], 642 ^ []))],extension(348 ^ 4,bind([[_86913, _86915], [_55990, 642 ^ []]]))).
% 0.74/1.38 ncf('1.1.1.1',plain,[model(349 ^ [_55990, 642 ^ []], 642 ^ [])],extension(644 ^ 5,bind([[_98270], [349 ^ [_55990, 642 ^ []]]]))).
% 0.74/1.38 ncf('1.1.2',plain,[-(status(642 ^ [], _55990, thm)), 98 : -(model(96 ^ [_55990, 642 ^ []], 642 ^ []))],extension(95 ^ 4,bind([[_77863, _77865], [_55990, 642 ^ []]]))).
% 0.74/1.38 ncf('1.1.2.1',plain,[model(96 ^ [_55990, 642 ^ []], 642 ^ [])],extension(644 ^ 7,bind([[_98270], [96 ^ [_55990, 642 ^ []]]]))).
% 0.74/1.38 %-----------------------------------------------------
% 0.74/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------