%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS255+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n013.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:33 EDT 2023
% Result : Theorem 0.75s 1.39s
% Output : Proof 0.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : KRS255+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.11/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n013.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:53:35 EDT 2023
% 0.12/0.35 % CPUTime :
% 0.75/1.39
% 0.75/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.75/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.75/1.39 %-----------------------------------------------------
% 0.75/1.39 ncf(matrix, plain, [(689 ^ _74355) ^ [] : [mighta(sap, thm)], (509 ^ _74355) ^ [_92946, _92948] : [mighta(_92948, _92946), 514 ^ _74355 : [(515 ^ _74355) ^ [] : [-(status(512 ^ [_92946, _92948], 513 ^ [_92946, _92948], _92948))], (517 ^ _74355) ^ [] : [-(status(512 ^ [_92946, _92948], 513 ^ [_92946, _92948], _92946))]]], (499 ^ _74355) ^ [_92601, _92603] : [-(mighta(_92603, _92601)), 500 ^ _74355 : [(501 ^ _74355) ^ [_92714, _92716] : [status(_92716, _92714, _92603), status(_92716, _92714, _92601)]]], (519 ^ _74355) ^ [_93429, _93431] : [522 ^ _74355 : [(523 ^ _74355) ^ [] : [-(status(520 ^ [_93429, _93431], 521 ^ [_93429, _93431], _93431))], (525 ^ _74355) ^ [] : [status(520 ^ [_93429, _93431], 521 ^ [_93429, _93431], _93429)]], -(isa(_93431, _93429))], (529 ^ _74355) ^ [_93833, _93835] : [isa(_93835, _93833), 532 ^ _74355 : [(533 ^ _74355) ^ [_93991, _93993] : [status(_93993, _93991, _93835), -(status(_93993, _93991, _93833))]]], (549 ^ _74355) ^ [_94607, _94609] : [nota(_94609, _94607), 554 ^ _74355 : [(555 ^ _74355) ^ [] : [-(status(552 ^ [_94607, _94609], 553 ^ [_94607, _94609], _94609))], (557 ^ _74355) ^ [] : [status(552 ^ [_94607, _94609], 553 ^ [_94607, _94609], _94607)]]], (539 ^ _74355) ^ [_94257, _94259] : [-(nota(_94259, _94257)), 540 ^ _74355 : [(541 ^ _74355) ^ [_94372, _94374] : [status(_94374, _94372, _94259), -(status(_94374, _94372, _94257))]]], (559 ^ _74355) ^ [_95095, _95097] : [562 ^ _74355 : [(563 ^ _74355) ^ [] : [-(status(560 ^ [_95095, _95097], 561 ^ [_95095, _95097], _95097))], (565 ^ _74355) ^ [] : [-(status(560 ^ [_95095, _95097], 561 ^ [_95095, _95097], _95095))]], -(nevera(_95097, _95095))], (569 ^ _74355) ^ [_95506, _95508] : [nevera(_95508, _95506), 572 ^ _74355 : [(573 ^ _74355) ^ [_95666, _95668] : [status(_95668, _95666, _95508), status(_95668, _95666, _95506)]]], (597 ^ _74355) ^ [_96549, _96551] : [xora(_96551, _96549), 600 ^ _74355 : [(601 ^ _74355) ^ [_96718, _96720] : [602 ^ _74355 : [(603 ^ _74355) ^ [] : [-(status(_96720, _96718, _96551))], (605 ^ _74355) ^ [] : [status(_96720, _96718, _96549)]], 606 ^ _74355 : [(607 ^ _74355) ^ [] : [-(status(_96720, _96718, _96549))], (609 ^ _74355) ^ [] : [status(_96720, _96718, _96551)]]]]], (579 ^ _74355) ^ [_95933, _95935] : [-(xora(_95935, _95933)), 582 ^ _74355 : [(583 ^ _74355) ^ [] : [status(580 ^ [_95933, _95935], 581 ^ [_95933, _95935], _95935), -(status(580 ^ [_95933, _95935], 581 ^ [_95933, _95935], _95933))], (589 ^ _74355) ^ [] : [status(580 ^ [_95933, _95935], 581 ^ [_95933, _95935], _95933), -(status(580 ^ [_95933, _95935], 581 ^ [_95933, _95935], _95935))]]], (611 ^ _74355) ^ [_97125, _97127] : [612 ^ _74355 : [(613 ^ _74355) ^ [] : [-(model(_97127, _97125))], (615 ^ _74355) ^ [] : [model(_97127, not _97125)]], 616 ^ _74355 : [(617 ^ _74355) ^ [] : [-(model(_97127, not _97125))], (619 ^ _74355) ^ [] : [model(_97127, _97125)]]], (621 ^ _74355) ^ [_97521, _97523] : [model(_97523, _97521), model(_97523, not _97521)], (627 ^ _74355) ^ [_97688, _97690] : [-(model(_97690, not _97688)), -(model(_97690, _97688))], (634 ^ _74355) ^ [_97920] : [-(model(_97920, 632 ^ []))], (638 ^ _74355) ^ [] : [-(model(636 ^ [], 635 ^ []))], (641 ^ _74355) ^ [] : [model(639 ^ [], 635 ^ [])], (644 ^ _74355) ^ [_98279] : [model(_98279, 642 ^ [])], (649 ^ _74355) ^ [] : [-(model(647 ^ [], 645 ^ []))], (651 ^ _74355) ^ [] : [-(model(647 ^ [], 646 ^ []))], (654 ^ _74355) ^ [] : [model(652 ^ [], 645 ^ []), model(652 ^ [], 646 ^ [])], (682 ^ _74355) ^ [] : [-(model(678 ^ [], 679 ^ []))], (684 ^ _74355) ^ [] : [model(678 ^ [], 680 ^ [])], (687 ^ _74355) ^ [] : [-(model(685 ^ [], 680 ^ []))], (663 ^ _74355) ^ [] : [-(model(661 ^ [], 659 ^ []))], (672 ^ _74355) ^ [] : [model(670 ^ [], 659 ^ [])], (674 ^ _74355) ^ [] : [-(model(670 ^ [], 660 ^ []))], (677 ^ _74355) ^ [] : [model(675 ^ [], 660 ^ [])], (665 ^ _74355) ^ [_99132] : [model(_99132, 659 ^ []), -(model(_99132, 660 ^ []))], (2 ^ _74355) ^ [_74517, _74519] : [3 ^ _74355 : [(4 ^ _74355) ^ [_74623] : [model(_74623, _74519)], (7 ^ _74355) ^ [] : [-(model(5 ^ [_74517, _74519], _74517))]], -(status(_74519, _74517, unp))], (11 ^ _74355) ^ [_74838, _74840] : [status(_74840, _74838, unp), -(model(16 ^ [_74838, _74840], _74840)), 19 ^ _74355 : [(20 ^ _74355) ^ [_75102] : [model(_75102, _74838)]]], (22 ^ _74355) ^ [_75253, _75255] : [24 ^ _74355 : [(25 ^ _74355) ^ [] : [-(model(23 ^ [_75253, _75255], _75255))], (27 ^ _74355) ^ [_75453] : [model(_75453, _75253)]], -(status(_75255, _75253, sap))], (31 ^ _74355) ^ [_75570, _75572] : [status(_75572, _75570, sap), 36 ^ _74355 : [(37 ^ _74355) ^ [_75732] : [model(_75732, _75572)]], -(model(38 ^ [_75570, _75572], _75570))], (42 ^ _74355) ^ [_75981, _75983] : [-(status(_75983, _75981, esa)), 46 ^ _74355 : [(47 ^ _74355) ^ [] : [-(model(45 ^ [_75981, _75983], _75983))], (49 ^ _74355) ^ [_76224] : [model(_76224, _75981)]], 51 ^ _74355 : [(52 ^ _74355) ^ [] : [-(model(50 ^ [_75981, _75983], _75981))], (54 ^ _74355) ^ [_76405] : [model(_76405, _75983)]]], (58 ^ _74355) ^ [_76527, _76529] : [status(_76529, _76527, esa), 61 ^ _74355 : [(62 ^ _74355) ^ [] : [63 ^ _74355 : [(64 ^ _74355) ^ [_76718] : [model(_76718, _76529)]], -(model(65 ^ [_76527, _76529], _76527))], (69 ^ _74355) ^ [] : [70 ^ _74355 : [(71 ^ _74355) ^ [_76916] : [model(_76916, _76527)]], -(model(72 ^ [_76527, _76529], _76529))]]], (86 ^ _74355) ^ [_77484, _77486] : [status(_77486, _77484, sat), 90 ^ _74355 : [(91 ^ _74355) ^ [] : [-(model(89 ^ [_77484, _77486], _77486))], (93 ^ _74355) ^ [] : [-(model(89 ^ [_77484, _77486], _77484))]]], (76 ^ _74355) ^ [_77168, _77170] : [-(status(_77170, _77168, sat)), 77 ^ _74355 : [(78 ^ _74355) ^ [_77261] : [model(_77261, _77170), model(_77261, _77168)]]], (95 ^ _74355) ^ [_77872, _77874] : [97 ^ _74355 : [(98 ^ _74355) ^ [] : [-(model(96 ^ [_77872, _77874], _77874))], (100 ^ _74355) ^ [] : [model(96 ^ [_77872, _77874], _77872)]], -(status(_77874, _77872, thm))], (104 ^ _74355) ^ [_78181, _78183] : [status(_78183, _78181, thm), 107 ^ _74355 : [(108 ^ _74355) ^ [_78320] : [model(_78320, _78183), -(model(_78320, _78181))]]], (114 ^ _74355) ^ [_78576, _78578] : [-(status(_78578, _78576, eqv)), 117 ^ _74355 : [(118 ^ _74355) ^ [_78698] : [model(_78698, _78578)]], 122 ^ _74355 : [(123 ^ _74355) ^ [] : [-(model(119 ^ [_78576, _78578], _78578))], (125 ^ _74355) ^ [] : [model(119 ^ [_78576, _78578], _78576)]], 126 ^ _74355 : [(127 ^ _74355) ^ [] : [-(model(119 ^ [_78576, _78578], _78576))], (129 ^ _74355) ^ [] : [model(119 ^ [_78576, _78578], _78578)]]], (133 ^ _74355) ^ [_79171, _79173] : [status(_79173, _79171, eqv), 137 ^ _74355 : [(138 ^ _74355) ^ [] : [-(model(136 ^ [_79171, _79173], _79173))], (140 ^ _74355) ^ [_79468] : [model(_79468, _79173), -(model(_79468, _79171))], (146 ^ _74355) ^ [_79640] : [model(_79640, _79171), -(model(_79640, _79173))]]], (163 ^ _74355) ^ [_80232, _80234] : [status(_80234, _80232, tac), 167 ^ _74355 : [(168 ^ _74355) ^ [] : [-(model(166 ^ [_80232, _80234], _80234))], (170 ^ _74355) ^ [_80479] : [-(model(_80479, _80232))]]], (152 ^ _74355) ^ [_79900, _79902] : [-(status(_79902, _79900, tac)), 155 ^ _74355 : [(156 ^ _74355) ^ [_80016] : [model(_80016, _79902)]], model(157 ^ [_79900, _79902], _79900)], (193 ^ _74355) ^ [_81294, _81296] : [status(_81296, _81294, wec), 197 ^ _74355 : [(198 ^ _74355) ^ [] : [-(model(196 ^ [_81294, _81296], _81296))], (207 ^ _74355) ^ [] : [-(model(205 ^ [_81294, _81296], _81294))], (209 ^ _74355) ^ [] : [model(205 ^ [_81294, _81296], _81296)], (200 ^ _74355) ^ [_81601] : [model(_81601, _81296), -(model(_81601, _81294))]]], (172 ^ _74355) ^ [_80628, _80630] : [-(status(_80630, _80628, wec)), 175 ^ _74355 : [(176 ^ _74355) ^ [_80769] : [model(_80769, _80630)]], 180 ^ _74355 : [(181 ^ _74355) ^ [] : [-(model(179 ^ [_80628, _80630], _80630))], (183 ^ _74355) ^ [] : [model(179 ^ [_80628, _80630], _80628)]], 184 ^ _74355 : [(185 ^ _74355) ^ [_81058] : [model(_81058, _80628), -(model(_81058, _80630))]]], (211 ^ _74355) ^ [_82043, _82045] : [-(status(_82045, _82043, eth)), 214 ^ _74355 : [(215 ^ _74355) ^ [_82178] : [model(_82178, _82045)]], 218 ^ _74355 : [(219 ^ _74355) ^ [_82274] : [-(model(_82274, _82045))]], 223 ^ _74355 : [(224 ^ _74355) ^ [] : [-(model(220 ^ [_82043, _82045], _82045))], (226 ^ _74355) ^ [] : [model(220 ^ [_82043, _82045], _82043)]], 227 ^ _74355 : [(228 ^ _74355) ^ [] : [-(model(220 ^ [_82043, _82045], _82043))], (230 ^ _74355) ^ [] : [model(220 ^ [_82043, _82045], _82045)]]], (234 ^ _74355) ^ [_82752, _82754] : [status(_82754, _82752, eth), 238 ^ _74355 : [(239 ^ _74355) ^ [] : [-(model(237 ^ [_82752, _82754], _82754))], (242 ^ _74355) ^ [] : [model(240 ^ [_82752, _82754], _82754)], (244 ^ _74355) ^ [_83181] : [model(_83181, _82754), -(model(_83181, _82752))], (250 ^ _74355) ^ [_83353] : [model(_83353, _82752), -(model(_83353, _82754))]]], (267 ^ _74355) ^ [_83938, _83940] : [status(_83940, _83938, tau), 270 ^ _74355 : [(271 ^ _74355) ^ [_84082] : [-(model(_84082, _83940))], (273 ^ _74355) ^ [_84130] : [-(model(_84130, _83938))]]], (256 ^ _74355) ^ [_83615, _83617] : [-(status(_83617, _83615, tau)), model(257 ^ [_83615, _83617], _83617), model(257 ^ [_83615, _83617], _83615)], (290 ^ _74355) ^ [_84725, _84727] : [status(_84727, _84725, wtc), 294 ^ _74355 : [(295 ^ _74355) ^ [] : [-(model(293 ^ [_84725, _84727], _84727))], (298 ^ _74355) ^ [] : [model(296 ^ [_84725, _84727], _84727)], (300 ^ _74355) ^ [_85104] : [-(model(_85104, _84725))]]], (275 ^ _74355) ^ [_84279, _84281] : [-(status(_84281, _84279, wtc)), 278 ^ _74355 : [(279 ^ _74355) ^ [_84408] : [model(_84408, _84281)]], 282 ^ _74355 : [(283 ^ _74355) ^ [_84504] : [-(model(_84504, _84281))]], model(284 ^ [_84279, _84281], _84279)], (327 ^ _74355) ^ [_86035, _86037] : [status(_86037, _86035, wth), 331 ^ _74355 : [(332 ^ _74355) ^ [] : [-(model(330 ^ [_86035, _86037], _86037))], (341 ^ _74355) ^ [] : [-(model(339 ^ [_86035, _86037], _86035))], (343 ^ _74355) ^ [] : [model(339 ^ [_86035, _86037], _86037)], (346 ^ _74355) ^ [] : [model(344 ^ [_86035, _86037], _86035)], (334 ^ _74355) ^ [_86355] : [model(_86355, _86037), -(model(_86355, _86035))]]], (302 ^ _74355) ^ [_85255, _85257] : [-(status(_85257, _85255, wth)), 305 ^ _74355 : [(306 ^ _74355) ^ [_85409] : [model(_85409, _85257)]], 310 ^ _74355 : [(311 ^ _74355) ^ [] : [-(model(309 ^ [_85255, _85257], _85257))], (313 ^ _74355) ^ [] : [model(309 ^ [_85255, _85257], _85255)]], 322 ^ _74355 : [(323 ^ _74355) ^ [_85905] : [-(model(_85905, _85255))]], 316 ^ _74355 : [(317 ^ _74355) ^ [_85732] : [model(_85732, _85255), -(model(_85732, _85257))]]], (348 ^ _74355) ^ [_86922, _86924] : [-(model(349 ^ [_86922, _86924], _86924)), -(status(_86924, _86922, cax))], (355 ^ _74355) ^ [_87146, _87148] : [status(_87148, _87146, cax), 358 ^ _74355 : [(359 ^ _74355) ^ [_87265] : [model(_87265, _87148)]]], (372 ^ _74355) ^ [_87747, _87749] : [status(_87749, _87747, sca), 375 ^ _74355 : [(376 ^ _74355) ^ [_87897] : [model(_87897, _87749)], (379 ^ _74355) ^ [] : [-(model(377 ^ [_87747, _87749], _87747))]]], (361 ^ _74355) ^ [_87412, _87414] : [-(status(_87414, _87412, sca)), -(model(364 ^ [_87412, _87414], _87414)), 367 ^ _74355 : [(368 ^ _74355) ^ [_87628] : [model(_87628, _87412)]]], (393 ^ _74355) ^ [_88514, _88516] : [status(_88516, _88514, tca), 396 ^ _74355 : [(397 ^ _74355) ^ [_88664] : [model(_88664, _88516)], (399 ^ _74355) ^ [_88726] : [-(model(_88726, _88514))]]], (381 ^ _74355) ^ [_88144, _88146] : [-(status(_88146, _88144, tca)), -(model(384 ^ [_88144, _88146], _88146)), model(387 ^ [_88144, _88146], _88144)], (416 ^ _74355) ^ [_89324, _89326] : [status(_89326, _89324, wca), 419 ^ _74355 : [(420 ^ _74355) ^ [_89487] : [model(_89487, _89326)], (423 ^ _74355) ^ [] : [-(model(421 ^ [_89324, _89326], _89324))], (426 ^ _74355) ^ [] : [model(424 ^ [_89324, _89326], _89324)]]], (401 ^ _74355) ^ [_88875, _88877] : [-(status(_88877, _88875, wca)), -(model(404 ^ [_88875, _88877], _88877)), 409 ^ _74355 : [(410 ^ _74355) ^ [_89138] : [model(_89138, _88875)]], 411 ^ _74355 : [(412 ^ _74355) ^ [_89200] : [-(model(_89200, _88875))]]], (438 ^ _74355) ^ [_90177, _90179] : [status(_90179, _90177, csa), 442 ^ _74355 : [(443 ^ _74355) ^ [] : [-(model(441 ^ [_90177, _90179], _90179))], (445 ^ _74355) ^ [] : [-(model(441 ^ [_90177, _90179], not _90177))]]], (428 ^ _74355) ^ [_89855, _89857] : [-(status(_89857, _89855, csa)), 429 ^ _74355 : [(430 ^ _74355) ^ [_89950] : [model(_89950, _89857), model(_89950, not _89855)]]], (459 ^ _74355) ^ [_90944, _90946] : [status(_90946, _90944, uns), 462 ^ _74355 : [(463 ^ _74355) ^ [_91095] : [-(model(_91095, _90946))], (465 ^ _74355) ^ [_91157] : [-(model(_91157, not _90944))]]], (447 ^ _74355) ^ [_90571, _90573] : [-(status(_90573, _90571, uns)), model(450 ^ [_90571, _90573], _90573), model(453 ^ [_90571, _90573], not _90571)], (485 ^ _74355) ^ [_91851, _91853] : [status(_91853, _91851, noc), 489 ^ _74355 : [(490 ^ _74355) ^ [] : [-(model(488 ^ [_91851, _91853], _91853))], (492 ^ _74355) ^ [] : [-(model(488 ^ [_91851, _91853], _91851))], (495 ^ _74355) ^ [] : [-(model(493 ^ [_91851, _91853], _91853))], (497 ^ _74355) ^ [] : [-(model(493 ^ [_91851, _91853], not _91851))]]], (467 ^ _74355) ^ [_91288, _91290] : [-(status(_91290, _91288, noc)), 470 ^ _74355 : [(471 ^ _74355) ^ [_91434] : [model(_91434, _91290), model(_91434, _91288)]], 476 ^ _74355 : [(477 ^ _74355) ^ [_91619] : [model(_91619, _91290), model(_91619, not _91288)]]]], input).
% 0.75/1.39 ncf('1',plain,[mighta(sap, thm)],start(689 ^ 0)).
% 0.75/1.39 ncf('1.1',plain,[-(mighta(sap, thm)), 501 : status(642 ^ [], _55990, sap), 501 : status(642 ^ [], _55990, thm)],extension(499 ^ 1,bind([[_92601, _92603, _92714, _92716], [thm, sap, _55990, 642 ^ []]]))).
% 0.75/1.39 ncf('1.1.1',plain,[-(status(642 ^ [], _55990, sap)), 25 : -(model(23 ^ [_55990, 642 ^ []], 642 ^ []))],extension(22 ^ 4,bind([[_75253, _75255], [_55990, 642 ^ []]]))).
% 0.75/1.39 ncf('1.1.1.1',plain,[model(23 ^ [_55990, 642 ^ []], 642 ^ [])],extension(644 ^ 7,bind([[_98279], [23 ^ [_55990, 642 ^ []]]]))).
% 0.75/1.39 ncf('1.1.2',plain,[-(status(642 ^ [], _55990, thm)), 98 : -(model(96 ^ [_55990, 642 ^ []], 642 ^ []))],extension(95 ^ 4,bind([[_77872, _77874], [_55990, 642 ^ []]]))).
% 0.75/1.39 ncf('1.1.2.1',plain,[model(96 ^ [_55990, 642 ^ []], 642 ^ [])],extension(644 ^ 7,bind([[_98279], [96 ^ [_55990, 642 ^ []]]]))).
% 0.75/1.39 %-----------------------------------------------------
% 0.75/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------