%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS187+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n005.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.78s 1.38s
% Output : Proof 0.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : KRS187+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n005.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:02:23 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.78/1.38
% 0.78/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.78/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.78/1.38 %-----------------------------------------------------
% 0.78/1.38 ncf(matrix, plain, [(689 ^ _74935) ^ [] : [isa(tac, thm)], (509 ^ _74935) ^ [_93526, _93528] : [mighta(_93528, _93526), 514 ^ _74935 : [(515 ^ _74935) ^ [] : [-(status(512 ^ [_93526, _93528], 513 ^ [_93526, _93528], _93528))], (517 ^ _74935) ^ [] : [-(status(512 ^ [_93526, _93528], 513 ^ [_93526, _93528], _93526))]]], (499 ^ _74935) ^ [_93181, _93183] : [-(mighta(_93183, _93181)), 500 ^ _74935 : [(501 ^ _74935) ^ [_93294, _93296] : [status(_93296, _93294, _93183), status(_93296, _93294, _93181)]]], (519 ^ _74935) ^ [_94009, _94011] : [522 ^ _74935 : [(523 ^ _74935) ^ [] : [-(status(520 ^ [_94009, _94011], 521 ^ [_94009, _94011], _94011))], (525 ^ _74935) ^ [] : [status(520 ^ [_94009, _94011], 521 ^ [_94009, _94011], _94009)]], -(isa(_94011, _94009))], (529 ^ _74935) ^ [_94413, _94415] : [isa(_94415, _94413), 532 ^ _74935 : [(533 ^ _74935) ^ [_94571, _94573] : [status(_94573, _94571, _94415), -(status(_94573, _94571, _94413))]]], (549 ^ _74935) ^ [_95187, _95189] : [nota(_95189, _95187), 554 ^ _74935 : [(555 ^ _74935) ^ [] : [-(status(552 ^ [_95187, _95189], 553 ^ [_95187, _95189], _95189))], (557 ^ _74935) ^ [] : [status(552 ^ [_95187, _95189], 553 ^ [_95187, _95189], _95187)]]], (539 ^ _74935) ^ [_94837, _94839] : [-(nota(_94839, _94837)), 540 ^ _74935 : [(541 ^ _74935) ^ [_94952, _94954] : [status(_94954, _94952, _94839), -(status(_94954, _94952, _94837))]]], (559 ^ _74935) ^ [_95675, _95677] : [562 ^ _74935 : [(563 ^ _74935) ^ [] : [-(status(560 ^ [_95675, _95677], 561 ^ [_95675, _95677], _95677))], (565 ^ _74935) ^ [] : [-(status(560 ^ [_95675, _95677], 561 ^ [_95675, _95677], _95675))]], -(nevera(_95677, _95675))], (569 ^ _74935) ^ [_96086, _96088] : [nevera(_96088, _96086), 572 ^ _74935 : [(573 ^ _74935) ^ [_96246, _96248] : [status(_96248, _96246, _96088), status(_96248, _96246, _96086)]]], (597 ^ _74935) ^ [_97129, _97131] : [xora(_97131, _97129), 600 ^ _74935 : [(601 ^ _74935) ^ [_97298, _97300] : [602 ^ _74935 : [(603 ^ _74935) ^ [] : [-(status(_97300, _97298, _97131))], (605 ^ _74935) ^ [] : [status(_97300, _97298, _97129)]], 606 ^ _74935 : [(607 ^ _74935) ^ [] : [-(status(_97300, _97298, _97129))], (609 ^ _74935) ^ [] : [status(_97300, _97298, _97131)]]]]], (579 ^ _74935) ^ [_96513, _96515] : [-(xora(_96515, _96513)), 582 ^ _74935 : [(583 ^ _74935) ^ [] : [status(580 ^ [_96513, _96515], 581 ^ [_96513, _96515], _96515), -(status(580 ^ [_96513, _96515], 581 ^ [_96513, _96515], _96513))], (589 ^ _74935) ^ [] : [status(580 ^ [_96513, _96515], 581 ^ [_96513, _96515], _96513), -(status(580 ^ [_96513, _96515], 581 ^ [_96513, _96515], _96515))]]], (611 ^ _74935) ^ [_97705, _97707] : [612 ^ _74935 : [(613 ^ _74935) ^ [] : [-(model(_97707, _97705))], (615 ^ _74935) ^ [] : [model(_97707, not _97705)]], 616 ^ _74935 : [(617 ^ _74935) ^ [] : [-(model(_97707, not _97705))], (619 ^ _74935) ^ [] : [model(_97707, _97705)]]], (621 ^ _74935) ^ [_98101, _98103] : [model(_98103, _98101), model(_98103, not _98101)], (627 ^ _74935) ^ [_98268, _98270] : [-(model(_98270, not _98268)), -(model(_98270, _98268))], (634 ^ _74935) ^ [_98500] : [-(model(_98500, 632 ^ []))], (638 ^ _74935) ^ [] : [-(model(636 ^ [], 635 ^ []))], (641 ^ _74935) ^ [] : [model(639 ^ [], 635 ^ [])], (644 ^ _74935) ^ [_98859] : [model(_98859, 642 ^ [])], (649 ^ _74935) ^ [] : [-(model(647 ^ [], 645 ^ []))], (651 ^ _74935) ^ [] : [-(model(647 ^ [], 646 ^ []))], (654 ^ _74935) ^ [] : [model(652 ^ [], 645 ^ []), model(652 ^ [], 646 ^ [])], (682 ^ _74935) ^ [] : [-(model(678 ^ [], 679 ^ []))], (684 ^ _74935) ^ [] : [model(678 ^ [], 680 ^ [])], (687 ^ _74935) ^ [] : [-(model(685 ^ [], 680 ^ []))], (663 ^ _74935) ^ [] : [-(model(661 ^ [], 659 ^ []))], (672 ^ _74935) ^ [] : [model(670 ^ [], 659 ^ [])], (674 ^ _74935) ^ [] : [-(model(670 ^ [], 660 ^ []))], (677 ^ _74935) ^ [] : [model(675 ^ [], 660 ^ [])], (665 ^ _74935) ^ [_99712] : [model(_99712, 659 ^ []), -(model(_99712, 660 ^ []))], (2 ^ _74935) ^ [_75097, _75099] : [3 ^ _74935 : [(4 ^ _74935) ^ [_75203] : [model(_75203, _75099)], (7 ^ _74935) ^ [] : [-(model(5 ^ [_75097, _75099], _75097))]], -(status(_75099, _75097, unp))], (11 ^ _74935) ^ [_75418, _75420] : [status(_75420, _75418, unp), -(model(16 ^ [_75418, _75420], _75420)), 19 ^ _74935 : [(20 ^ _74935) ^ [_75682] : [model(_75682, _75418)]]], (22 ^ _74935) ^ [_75833, _75835] : [24 ^ _74935 : [(25 ^ _74935) ^ [] : [-(model(23 ^ [_75833, _75835], _75835))], (27 ^ _74935) ^ [_76033] : [model(_76033, _75833)]], -(status(_75835, _75833, sap))], (31 ^ _74935) ^ [_76150, _76152] : [status(_76152, _76150, sap), 36 ^ _74935 : [(37 ^ _74935) ^ [_76312] : [model(_76312, _76152)]], -(model(38 ^ [_76150, _76152], _76150))], (42 ^ _74935) ^ [_76561, _76563] : [-(status(_76563, _76561, esa)), 46 ^ _74935 : [(47 ^ _74935) ^ [] : [-(model(45 ^ [_76561, _76563], _76563))], (49 ^ _74935) ^ [_76804] : [model(_76804, _76561)]], 51 ^ _74935 : [(52 ^ _74935) ^ [] : [-(model(50 ^ [_76561, _76563], _76561))], (54 ^ _74935) ^ [_76985] : [model(_76985, _76563)]]], (58 ^ _74935) ^ [_77107, _77109] : [status(_77109, _77107, esa), 61 ^ _74935 : [(62 ^ _74935) ^ [] : [63 ^ _74935 : [(64 ^ _74935) ^ [_77298] : [model(_77298, _77109)]], -(model(65 ^ [_77107, _77109], _77107))], (69 ^ _74935) ^ [] : [70 ^ _74935 : [(71 ^ _74935) ^ [_77496] : [model(_77496, _77107)]], -(model(72 ^ [_77107, _77109], _77109))]]], (86 ^ _74935) ^ [_78064, _78066] : [status(_78066, _78064, sat), 90 ^ _74935 : [(91 ^ _74935) ^ [] : [-(model(89 ^ [_78064, _78066], _78066))], (93 ^ _74935) ^ [] : [-(model(89 ^ [_78064, _78066], _78064))]]], (76 ^ _74935) ^ [_77748, _77750] : [-(status(_77750, _77748, sat)), 77 ^ _74935 : [(78 ^ _74935) ^ [_77841] : [model(_77841, _77750), model(_77841, _77748)]]], (95 ^ _74935) ^ [_78452, _78454] : [97 ^ _74935 : [(98 ^ _74935) ^ [] : [-(model(96 ^ [_78452, _78454], _78454))], (100 ^ _74935) ^ [] : [model(96 ^ [_78452, _78454], _78452)]], -(status(_78454, _78452, thm))], (104 ^ _74935) ^ [_78761, _78763] : [status(_78763, _78761, thm), 107 ^ _74935 : [(108 ^ _74935) ^ [_78900] : [model(_78900, _78763), -(model(_78900, _78761))]]], (114 ^ _74935) ^ [_79156, _79158] : [-(status(_79158, _79156, eqv)), 117 ^ _74935 : [(118 ^ _74935) ^ [_79278] : [model(_79278, _79158)]], 122 ^ _74935 : [(123 ^ _74935) ^ [] : [-(model(119 ^ [_79156, _79158], _79158))], (125 ^ _74935) ^ [] : [model(119 ^ [_79156, _79158], _79156)]], 126 ^ _74935 : [(127 ^ _74935) ^ [] : [-(model(119 ^ [_79156, _79158], _79156))], (129 ^ _74935) ^ [] : [model(119 ^ [_79156, _79158], _79158)]]], (133 ^ _74935) ^ [_79751, _79753] : [status(_79753, _79751, eqv), 137 ^ _74935 : [(138 ^ _74935) ^ [] : [-(model(136 ^ [_79751, _79753], _79753))], (140 ^ _74935) ^ [_80048] : [model(_80048, _79753), -(model(_80048, _79751))], (146 ^ _74935) ^ [_80220] : [model(_80220, _79751), -(model(_80220, _79753))]]], (163 ^ _74935) ^ [_80812, _80814] : [status(_80814, _80812, tac), 167 ^ _74935 : [(168 ^ _74935) ^ [] : [-(model(166 ^ [_80812, _80814], _80814))], (170 ^ _74935) ^ [_81059] : [-(model(_81059, _80812))]]], (152 ^ _74935) ^ [_80480, _80482] : [-(status(_80482, _80480, tac)), 155 ^ _74935 : [(156 ^ _74935) ^ [_80596] : [model(_80596, _80482)]], model(157 ^ [_80480, _80482], _80480)], (193 ^ _74935) ^ [_81874, _81876] : [status(_81876, _81874, wec), 197 ^ _74935 : [(198 ^ _74935) ^ [] : [-(model(196 ^ [_81874, _81876], _81876))], (207 ^ _74935) ^ [] : [-(model(205 ^ [_81874, _81876], _81874))], (209 ^ _74935) ^ [] : [model(205 ^ [_81874, _81876], _81876)], (200 ^ _74935) ^ [_82181] : [model(_82181, _81876), -(model(_82181, _81874))]]], (172 ^ _74935) ^ [_81208, _81210] : [-(status(_81210, _81208, wec)), 175 ^ _74935 : [(176 ^ _74935) ^ [_81349] : [model(_81349, _81210)]], 180 ^ _74935 : [(181 ^ _74935) ^ [] : [-(model(179 ^ [_81208, _81210], _81210))], (183 ^ _74935) ^ [] : [model(179 ^ [_81208, _81210], _81208)]], 184 ^ _74935 : [(185 ^ _74935) ^ [_81638] : [model(_81638, _81208), -(model(_81638, _81210))]]], (211 ^ _74935) ^ [_82623, _82625] : [-(status(_82625, _82623, eth)), 214 ^ _74935 : [(215 ^ _74935) ^ [_82758] : [model(_82758, _82625)]], 218 ^ _74935 : [(219 ^ _74935) ^ [_82854] : [-(model(_82854, _82625))]], 223 ^ _74935 : [(224 ^ _74935) ^ [] : [-(model(220 ^ [_82623, _82625], _82625))], (226 ^ _74935) ^ [] : [model(220 ^ [_82623, _82625], _82623)]], 227 ^ _74935 : [(228 ^ _74935) ^ [] : [-(model(220 ^ [_82623, _82625], _82623))], (230 ^ _74935) ^ [] : [model(220 ^ [_82623, _82625], _82625)]]], (234 ^ _74935) ^ [_83332, _83334] : [status(_83334, _83332, eth), 238 ^ _74935 : [(239 ^ _74935) ^ [] : [-(model(237 ^ [_83332, _83334], _83334))], (242 ^ _74935) ^ [] : [model(240 ^ [_83332, _83334], _83334)], (244 ^ _74935) ^ [_83761] : [model(_83761, _83334), -(model(_83761, _83332))], (250 ^ _74935) ^ [_83933] : [model(_83933, _83332), -(model(_83933, _83334))]]], (267 ^ _74935) ^ [_84518, _84520] : [status(_84520, _84518, tau), 270 ^ _74935 : [(271 ^ _74935) ^ [_84662] : [-(model(_84662, _84520))], (273 ^ _74935) ^ [_84710] : [-(model(_84710, _84518))]]], (256 ^ _74935) ^ [_84195, _84197] : [-(status(_84197, _84195, tau)), model(257 ^ [_84195, _84197], _84197), model(257 ^ [_84195, _84197], _84195)], (290 ^ _74935) ^ [_85305, _85307] : [status(_85307, _85305, wtc), 294 ^ _74935 : [(295 ^ _74935) ^ [] : [-(model(293 ^ [_85305, _85307], _85307))], (298 ^ _74935) ^ [] : [model(296 ^ [_85305, _85307], _85307)], (300 ^ _74935) ^ [_85684] : [-(model(_85684, _85305))]]], (275 ^ _74935) ^ [_84859, _84861] : [-(status(_84861, _84859, wtc)), 278 ^ _74935 : [(279 ^ _74935) ^ [_84988] : [model(_84988, _84861)]], 282 ^ _74935 : [(283 ^ _74935) ^ [_85084] : [-(model(_85084, _84861))]], model(284 ^ [_84859, _84861], _84859)], (327 ^ _74935) ^ [_86615, _86617] : [status(_86617, _86615, wth), 331 ^ _74935 : [(332 ^ _74935) ^ [] : [-(model(330 ^ [_86615, _86617], _86617))], (341 ^ _74935) ^ [] : [-(model(339 ^ [_86615, _86617], _86615))], (343 ^ _74935) ^ [] : [model(339 ^ [_86615, _86617], _86617)], (346 ^ _74935) ^ [] : [model(344 ^ [_86615, _86617], _86615)], (334 ^ _74935) ^ [_86935] : [model(_86935, _86617), -(model(_86935, _86615))]]], (302 ^ _74935) ^ [_85835, _85837] : [-(status(_85837, _85835, wth)), 305 ^ _74935 : [(306 ^ _74935) ^ [_85989] : [model(_85989, _85837)]], 310 ^ _74935 : [(311 ^ _74935) ^ [] : [-(model(309 ^ [_85835, _85837], _85837))], (313 ^ _74935) ^ [] : [model(309 ^ [_85835, _85837], _85835)]], 322 ^ _74935 : [(323 ^ _74935) ^ [_86485] : [-(model(_86485, _85835))]], 316 ^ _74935 : [(317 ^ _74935) ^ [_86312] : [model(_86312, _85835), -(model(_86312, _85837))]]], (348 ^ _74935) ^ [_87502, _87504] : [-(model(349 ^ [_87502, _87504], _87504)), -(status(_87504, _87502, cax))], (355 ^ _74935) ^ [_87726, _87728] : [status(_87728, _87726, cax), 358 ^ _74935 : [(359 ^ _74935) ^ [_87845] : [model(_87845, _87728)]]], (372 ^ _74935) ^ [_88327, _88329] : [status(_88329, _88327, sca), 375 ^ _74935 : [(376 ^ _74935) ^ [_88477] : [model(_88477, _88329)], (379 ^ _74935) ^ [] : [-(model(377 ^ [_88327, _88329], _88327))]]], (361 ^ _74935) ^ [_87992, _87994] : [-(status(_87994, _87992, sca)), -(model(364 ^ [_87992, _87994], _87994)), 367 ^ _74935 : [(368 ^ _74935) ^ [_88208] : [model(_88208, _87992)]]], (393 ^ _74935) ^ [_89094, _89096] : [status(_89096, _89094, tca), 396 ^ _74935 : [(397 ^ _74935) ^ [_89244] : [model(_89244, _89096)], (399 ^ _74935) ^ [_89306] : [-(model(_89306, _89094))]]], (381 ^ _74935) ^ [_88724, _88726] : [-(status(_88726, _88724, tca)), -(model(384 ^ [_88724, _88726], _88726)), model(387 ^ [_88724, _88726], _88724)], (416 ^ _74935) ^ [_89904, _89906] : [status(_89906, _89904, wca), 419 ^ _74935 : [(420 ^ _74935) ^ [_90067] : [model(_90067, _89906)], (423 ^ _74935) ^ [] : [-(model(421 ^ [_89904, _89906], _89904))], (426 ^ _74935) ^ [] : [model(424 ^ [_89904, _89906], _89904)]]], (401 ^ _74935) ^ [_89455, _89457] : [-(status(_89457, _89455, wca)), -(model(404 ^ [_89455, _89457], _89457)), 409 ^ _74935 : [(410 ^ _74935) ^ [_89718] : [model(_89718, _89455)]], 411 ^ _74935 : [(412 ^ _74935) ^ [_89780] : [-(model(_89780, _89455))]]], (438 ^ _74935) ^ [_90757, _90759] : [status(_90759, _90757, csa), 442 ^ _74935 : [(443 ^ _74935) ^ [] : [-(model(441 ^ [_90757, _90759], _90759))], (445 ^ _74935) ^ [] : [-(model(441 ^ [_90757, _90759], not _90757))]]], (428 ^ _74935) ^ [_90435, _90437] : [-(status(_90437, _90435, csa)), 429 ^ _74935 : [(430 ^ _74935) ^ [_90530] : [model(_90530, _90437), model(_90530, not _90435)]]], (459 ^ _74935) ^ [_91524, _91526] : [status(_91526, _91524, uns), 462 ^ _74935 : [(463 ^ _74935) ^ [_91675] : [-(model(_91675, _91526))], (465 ^ _74935) ^ [_91737] : [-(model(_91737, not _91524))]]], (447 ^ _74935) ^ [_91151, _91153] : [-(status(_91153, _91151, uns)), model(450 ^ [_91151, _91153], _91153), model(453 ^ [_91151, _91153], not _91151)], (485 ^ _74935) ^ [_92431, _92433] : [status(_92433, _92431, noc), 489 ^ _74935 : [(490 ^ _74935) ^ [] : [-(model(488 ^ [_92431, _92433], _92433))], (492 ^ _74935) ^ [] : [-(model(488 ^ [_92431, _92433], _92431))], (495 ^ _74935) ^ [] : [-(model(493 ^ [_92431, _92433], _92433))], (497 ^ _74935) ^ [] : [-(model(493 ^ [_92431, _92433], not _92431))]]], (467 ^ _74935) ^ [_91868, _91870] : [-(status(_91870, _91868, noc)), 470 ^ _74935 : [(471 ^ _74935) ^ [_92014] : [model(_92014, _91870), model(_92014, _91868)]], 476 ^ _74935 : [(477 ^ _74935) ^ [_92199] : [model(_92199, _91870), model(_92199, not _91868)]]]], input).
% 0.78/1.38 ncf('1',plain,[nota(tac, thm), 557 : status(552 ^ [thm, tac], 553 ^ [thm, tac], thm)],start(549 ^ 0,bind([[_95187, _95189], [thm, tac]]))).
% 0.78/1.38 ncf('1.1',plain,[-(nota(tac, thm)), 541 : status(520 ^ [thm, tac], 521 ^ [thm, tac], tac), 541 : -(status(520 ^ [thm, tac], 521 ^ [thm, tac], thm))],extension(539 ^ 1,bind([[_94837, _94839, _94952, _94954], [thm, tac, 521 ^ [thm, tac], 520 ^ [thm, tac]]]))).
% 0.78/1.38 ncf('1.1.1',plain,[-(status(520 ^ [thm, tac], 521 ^ [thm, tac], tac)), -(isa(tac, thm))],extension(519 ^ 4,bind([[_94009, _94011], [thm, tac]]))).
% 0.78/1.38 ncf('1.1.1.1',plain,[isa(tac, thm)],extension(689 ^ 5)).
% 0.78/1.38 ncf('1.1.2',plain,[status(520 ^ [thm, tac], 521 ^ [thm, tac], thm), -(isa(tac, thm))],extension(519 ^ 4,bind([[_94009, _94011], [thm, tac]]))).
% 0.78/1.38 ncf('1.1.2.1',plain,[isa(tac, thm)],extension(689 ^ 5)).
% 0.78/1.38 ncf('1.2',plain,[-(status(552 ^ [thm, tac], 553 ^ [thm, tac], thm)), 100 : model(96 ^ [553 ^ [thm, tac], 552 ^ [thm, tac]], 553 ^ [thm, tac])],extension(95 ^ 3,bind([[_78452, _78454], [553 ^ [thm, tac], 552 ^ [thm, tac]]]))).
% 0.78/1.38 ncf('1.2.1',plain,[-(model(96 ^ [553 ^ [thm, tac], 552 ^ [thm, tac]], 553 ^ [thm, tac])), status(552 ^ [thm, tac], 553 ^ [thm, tac], tac)],extension(163 ^ 6,bind([[_80812, _80814, _81059], [553 ^ [thm, tac], 552 ^ [thm, tac], 96 ^ [553 ^ [thm, tac], 552 ^ [thm, tac]]]]))).
% 0.78/1.38 ncf('1.2.1.1',plain,[-(status(552 ^ [thm, tac], 553 ^ [thm, tac], tac))],extension(555 ^ 7)).
% 0.78/1.38 %-----------------------------------------------------
% 0.78/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------