%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS196+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n029.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:28 EDT 2023
% Result : Theorem 0.68s 1.37s
% Output : Proof 0.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS196+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n029.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:18:13 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.68/1.37
% 0.68/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.68/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.68/1.37 %-----------------------------------------------------
% 0.68/1.37 ncf(matrix, plain, [(689 ^ _74159) ^ [] : [isa(wca, thm)], (509 ^ _74159) ^ [_92750, _92752] : [mighta(_92752, _92750), 514 ^ _74159 : [(515 ^ _74159) ^ [] : [-(status(512 ^ [_92750, _92752], 513 ^ [_92750, _92752], _92752))], (517 ^ _74159) ^ [] : [-(status(512 ^ [_92750, _92752], 513 ^ [_92750, _92752], _92750))]]], (499 ^ _74159) ^ [_92405, _92407] : [-(mighta(_92407, _92405)), 500 ^ _74159 : [(501 ^ _74159) ^ [_92518, _92520] : [status(_92520, _92518, _92407), status(_92520, _92518, _92405)]]], (519 ^ _74159) ^ [_93233, _93235] : [522 ^ _74159 : [(523 ^ _74159) ^ [] : [-(status(520 ^ [_93233, _93235], 521 ^ [_93233, _93235], _93235))], (525 ^ _74159) ^ [] : [status(520 ^ [_93233, _93235], 521 ^ [_93233, _93235], _93233)]], -(isa(_93235, _93233))], (529 ^ _74159) ^ [_93637, _93639] : [isa(_93639, _93637), 532 ^ _74159 : [(533 ^ _74159) ^ [_93795, _93797] : [status(_93797, _93795, _93639), -(status(_93797, _93795, _93637))]]], (549 ^ _74159) ^ [_94411, _94413] : [nota(_94413, _94411), 554 ^ _74159 : [(555 ^ _74159) ^ [] : [-(status(552 ^ [_94411, _94413], 553 ^ [_94411, _94413], _94413))], (557 ^ _74159) ^ [] : [status(552 ^ [_94411, _94413], 553 ^ [_94411, _94413], _94411)]]], (539 ^ _74159) ^ [_94061, _94063] : [-(nota(_94063, _94061)), 540 ^ _74159 : [(541 ^ _74159) ^ [_94176, _94178] : [status(_94178, _94176, _94063), -(status(_94178, _94176, _94061))]]], (559 ^ _74159) ^ [_94899, _94901] : [562 ^ _74159 : [(563 ^ _74159) ^ [] : [-(status(560 ^ [_94899, _94901], 561 ^ [_94899, _94901], _94901))], (565 ^ _74159) ^ [] : [-(status(560 ^ [_94899, _94901], 561 ^ [_94899, _94901], _94899))]], -(nevera(_94901, _94899))], (569 ^ _74159) ^ [_95310, _95312] : [nevera(_95312, _95310), 572 ^ _74159 : [(573 ^ _74159) ^ [_95470, _95472] : [status(_95472, _95470, _95312), status(_95472, _95470, _95310)]]], (597 ^ _74159) ^ [_96353, _96355] : [xora(_96355, _96353), 600 ^ _74159 : [(601 ^ _74159) ^ [_96522, _96524] : [602 ^ _74159 : [(603 ^ _74159) ^ [] : [-(status(_96524, _96522, _96355))], (605 ^ _74159) ^ [] : [status(_96524, _96522, _96353)]], 606 ^ _74159 : [(607 ^ _74159) ^ [] : [-(status(_96524, _96522, _96353))], (609 ^ _74159) ^ [] : [status(_96524, _96522, _96355)]]]]], (579 ^ _74159) ^ [_95737, _95739] : [-(xora(_95739, _95737)), 582 ^ _74159 : [(583 ^ _74159) ^ [] : [status(580 ^ [_95737, _95739], 581 ^ [_95737, _95739], _95739), -(status(580 ^ [_95737, _95739], 581 ^ [_95737, _95739], _95737))], (589 ^ _74159) ^ [] : [status(580 ^ [_95737, _95739], 581 ^ [_95737, _95739], _95737), -(status(580 ^ [_95737, _95739], 581 ^ [_95737, _95739], _95739))]]], (611 ^ _74159) ^ [_96929, _96931] : [612 ^ _74159 : [(613 ^ _74159) ^ [] : [-(model(_96931, _96929))], (615 ^ _74159) ^ [] : [model(_96931, not _96929)]], 616 ^ _74159 : [(617 ^ _74159) ^ [] : [-(model(_96931, not _96929))], (619 ^ _74159) ^ [] : [model(_96931, _96929)]]], (621 ^ _74159) ^ [_97325, _97327] : [model(_97327, _97325), model(_97327, not _97325)], (627 ^ _74159) ^ [_97492, _97494] : [-(model(_97494, not _97492)), -(model(_97494, _97492))], (634 ^ _74159) ^ [_97724] : [-(model(_97724, 632 ^ []))], (638 ^ _74159) ^ [] : [-(model(636 ^ [], 635 ^ []))], (641 ^ _74159) ^ [] : [model(639 ^ [], 635 ^ [])], (644 ^ _74159) ^ [_98083] : [model(_98083, 642 ^ [])], (649 ^ _74159) ^ [] : [-(model(647 ^ [], 645 ^ []))], (651 ^ _74159) ^ [] : [-(model(647 ^ [], 646 ^ []))], (654 ^ _74159) ^ [] : [model(652 ^ [], 645 ^ []), model(652 ^ [], 646 ^ [])], (682 ^ _74159) ^ [] : [-(model(678 ^ [], 679 ^ []))], (684 ^ _74159) ^ [] : [model(678 ^ [], 680 ^ [])], (687 ^ _74159) ^ [] : [-(model(685 ^ [], 680 ^ []))], (663 ^ _74159) ^ [] : [-(model(661 ^ [], 659 ^ []))], (672 ^ _74159) ^ [] : [model(670 ^ [], 659 ^ [])], (674 ^ _74159) ^ [] : [-(model(670 ^ [], 660 ^ []))], (677 ^ _74159) ^ [] : [model(675 ^ [], 660 ^ [])], (665 ^ _74159) ^ [_98936] : [model(_98936, 659 ^ []), -(model(_98936, 660 ^ []))], (2 ^ _74159) ^ [_74321, _74323] : [3 ^ _74159 : [(4 ^ _74159) ^ [_74427] : [model(_74427, _74323)], (7 ^ _74159) ^ [] : [-(model(5 ^ [_74321, _74323], _74321))]], -(status(_74323, _74321, unp))], (11 ^ _74159) ^ [_74642, _74644] : [status(_74644, _74642, unp), -(model(16 ^ [_74642, _74644], _74644)), 19 ^ _74159 : [(20 ^ _74159) ^ [_74906] : [model(_74906, _74642)]]], (22 ^ _74159) ^ [_75057, _75059] : [24 ^ _74159 : [(25 ^ _74159) ^ [] : [-(model(23 ^ [_75057, _75059], _75059))], (27 ^ _74159) ^ [_75257] : [model(_75257, _75057)]], -(status(_75059, _75057, sap))], (31 ^ _74159) ^ [_75374, _75376] : [status(_75376, _75374, sap), 36 ^ _74159 : [(37 ^ _74159) ^ [_75536] : [model(_75536, _75376)]], -(model(38 ^ [_75374, _75376], _75374))], (42 ^ _74159) ^ [_75785, _75787] : [-(status(_75787, _75785, esa)), 46 ^ _74159 : [(47 ^ _74159) ^ [] : [-(model(45 ^ [_75785, _75787], _75787))], (49 ^ _74159) ^ [_76028] : [model(_76028, _75785)]], 51 ^ _74159 : [(52 ^ _74159) ^ [] : [-(model(50 ^ [_75785, _75787], _75785))], (54 ^ _74159) ^ [_76209] : [model(_76209, _75787)]]], (58 ^ _74159) ^ [_76331, _76333] : [status(_76333, _76331, esa), 61 ^ _74159 : [(62 ^ _74159) ^ [] : [63 ^ _74159 : [(64 ^ _74159) ^ [_76522] : [model(_76522, _76333)]], -(model(65 ^ [_76331, _76333], _76331))], (69 ^ _74159) ^ [] : [70 ^ _74159 : [(71 ^ _74159) ^ [_76720] : [model(_76720, _76331)]], -(model(72 ^ [_76331, _76333], _76333))]]], (86 ^ _74159) ^ [_77288, _77290] : [status(_77290, _77288, sat), 90 ^ _74159 : [(91 ^ _74159) ^ [] : [-(model(89 ^ [_77288, _77290], _77290))], (93 ^ _74159) ^ [] : [-(model(89 ^ [_77288, _77290], _77288))]]], (76 ^ _74159) ^ [_76972, _76974] : [-(status(_76974, _76972, sat)), 77 ^ _74159 : [(78 ^ _74159) ^ [_77065] : [model(_77065, _76974), model(_77065, _76972)]]], (95 ^ _74159) ^ [_77676, _77678] : [97 ^ _74159 : [(98 ^ _74159) ^ [] : [-(model(96 ^ [_77676, _77678], _77678))], (100 ^ _74159) ^ [] : [model(96 ^ [_77676, _77678], _77676)]], -(status(_77678, _77676, thm))], (104 ^ _74159) ^ [_77985, _77987] : [status(_77987, _77985, thm), 107 ^ _74159 : [(108 ^ _74159) ^ [_78124] : [model(_78124, _77987), -(model(_78124, _77985))]]], (114 ^ _74159) ^ [_78380, _78382] : [-(status(_78382, _78380, eqv)), 117 ^ _74159 : [(118 ^ _74159) ^ [_78502] : [model(_78502, _78382)]], 122 ^ _74159 : [(123 ^ _74159) ^ [] : [-(model(119 ^ [_78380, _78382], _78382))], (125 ^ _74159) ^ [] : [model(119 ^ [_78380, _78382], _78380)]], 126 ^ _74159 : [(127 ^ _74159) ^ [] : [-(model(119 ^ [_78380, _78382], _78380))], (129 ^ _74159) ^ [] : [model(119 ^ [_78380, _78382], _78382)]]], (133 ^ _74159) ^ [_78975, _78977] : [status(_78977, _78975, eqv), 137 ^ _74159 : [(138 ^ _74159) ^ [] : [-(model(136 ^ [_78975, _78977], _78977))], (140 ^ _74159) ^ [_79272] : [model(_79272, _78977), -(model(_79272, _78975))], (146 ^ _74159) ^ [_79444] : [model(_79444, _78975), -(model(_79444, _78977))]]], (163 ^ _74159) ^ [_80036, _80038] : [status(_80038, _80036, tac), 167 ^ _74159 : [(168 ^ _74159) ^ [] : [-(model(166 ^ [_80036, _80038], _80038))], (170 ^ _74159) ^ [_80283] : [-(model(_80283, _80036))]]], (152 ^ _74159) ^ [_79704, _79706] : [-(status(_79706, _79704, tac)), 155 ^ _74159 : [(156 ^ _74159) ^ [_79820] : [model(_79820, _79706)]], model(157 ^ [_79704, _79706], _79704)], (193 ^ _74159) ^ [_81098, _81100] : [status(_81100, _81098, wec), 197 ^ _74159 : [(198 ^ _74159) ^ [] : [-(model(196 ^ [_81098, _81100], _81100))], (207 ^ _74159) ^ [] : [-(model(205 ^ [_81098, _81100], _81098))], (209 ^ _74159) ^ [] : [model(205 ^ [_81098, _81100], _81100)], (200 ^ _74159) ^ [_81405] : [model(_81405, _81100), -(model(_81405, _81098))]]], (172 ^ _74159) ^ [_80432, _80434] : [-(status(_80434, _80432, wec)), 175 ^ _74159 : [(176 ^ _74159) ^ [_80573] : [model(_80573, _80434)]], 180 ^ _74159 : [(181 ^ _74159) ^ [] : [-(model(179 ^ [_80432, _80434], _80434))], (183 ^ _74159) ^ [] : [model(179 ^ [_80432, _80434], _80432)]], 184 ^ _74159 : [(185 ^ _74159) ^ [_80862] : [model(_80862, _80432), -(model(_80862, _80434))]]], (211 ^ _74159) ^ [_81847, _81849] : [-(status(_81849, _81847, eth)), 214 ^ _74159 : [(215 ^ _74159) ^ [_81982] : [model(_81982, _81849)]], 218 ^ _74159 : [(219 ^ _74159) ^ [_82078] : [-(model(_82078, _81849))]], 223 ^ _74159 : [(224 ^ _74159) ^ [] : [-(model(220 ^ [_81847, _81849], _81849))], (226 ^ _74159) ^ [] : [model(220 ^ [_81847, _81849], _81847)]], 227 ^ _74159 : [(228 ^ _74159) ^ [] : [-(model(220 ^ [_81847, _81849], _81847))], (230 ^ _74159) ^ [] : [model(220 ^ [_81847, _81849], _81849)]]], (234 ^ _74159) ^ [_82556, _82558] : [status(_82558, _82556, eth), 238 ^ _74159 : [(239 ^ _74159) ^ [] : [-(model(237 ^ [_82556, _82558], _82558))], (242 ^ _74159) ^ [] : [model(240 ^ [_82556, _82558], _82558)], (244 ^ _74159) ^ [_82985] : [model(_82985, _82558), -(model(_82985, _82556))], (250 ^ _74159) ^ [_83157] : [model(_83157, _82556), -(model(_83157, _82558))]]], (267 ^ _74159) ^ [_83742, _83744] : [status(_83744, _83742, tau), 270 ^ _74159 : [(271 ^ _74159) ^ [_83886] : [-(model(_83886, _83744))], (273 ^ _74159) ^ [_83934] : [-(model(_83934, _83742))]]], (256 ^ _74159) ^ [_83419, _83421] : [-(status(_83421, _83419, tau)), model(257 ^ [_83419, _83421], _83421), model(257 ^ [_83419, _83421], _83419)], (290 ^ _74159) ^ [_84529, _84531] : [status(_84531, _84529, wtc), 294 ^ _74159 : [(295 ^ _74159) ^ [] : [-(model(293 ^ [_84529, _84531], _84531))], (298 ^ _74159) ^ [] : [model(296 ^ [_84529, _84531], _84531)], (300 ^ _74159) ^ [_84908] : [-(model(_84908, _84529))]]], (275 ^ _74159) ^ [_84083, _84085] : [-(status(_84085, _84083, wtc)), 278 ^ _74159 : [(279 ^ _74159) ^ [_84212] : [model(_84212, _84085)]], 282 ^ _74159 : [(283 ^ _74159) ^ [_84308] : [-(model(_84308, _84085))]], model(284 ^ [_84083, _84085], _84083)], (327 ^ _74159) ^ [_85839, _85841] : [status(_85841, _85839, wth), 331 ^ _74159 : [(332 ^ _74159) ^ [] : [-(model(330 ^ [_85839, _85841], _85841))], (341 ^ _74159) ^ [] : [-(model(339 ^ [_85839, _85841], _85839))], (343 ^ _74159) ^ [] : [model(339 ^ [_85839, _85841], _85841)], (346 ^ _74159) ^ [] : [model(344 ^ [_85839, _85841], _85839)], (334 ^ _74159) ^ [_86159] : [model(_86159, _85841), -(model(_86159, _85839))]]], (302 ^ _74159) ^ [_85059, _85061] : [-(status(_85061, _85059, wth)), 305 ^ _74159 : [(306 ^ _74159) ^ [_85213] : [model(_85213, _85061)]], 310 ^ _74159 : [(311 ^ _74159) ^ [] : [-(model(309 ^ [_85059, _85061], _85061))], (313 ^ _74159) ^ [] : [model(309 ^ [_85059, _85061], _85059)]], 322 ^ _74159 : [(323 ^ _74159) ^ [_85709] : [-(model(_85709, _85059))]], 316 ^ _74159 : [(317 ^ _74159) ^ [_85536] : [model(_85536, _85059), -(model(_85536, _85061))]]], (348 ^ _74159) ^ [_86726, _86728] : [-(model(349 ^ [_86726, _86728], _86728)), -(status(_86728, _86726, cax))], (355 ^ _74159) ^ [_86950, _86952] : [status(_86952, _86950, cax), 358 ^ _74159 : [(359 ^ _74159) ^ [_87069] : [model(_87069, _86952)]]], (372 ^ _74159) ^ [_87551, _87553] : [status(_87553, _87551, sca), 375 ^ _74159 : [(376 ^ _74159) ^ [_87701] : [model(_87701, _87553)], (379 ^ _74159) ^ [] : [-(model(377 ^ [_87551, _87553], _87551))]]], (361 ^ _74159) ^ [_87216, _87218] : [-(status(_87218, _87216, sca)), -(model(364 ^ [_87216, _87218], _87218)), 367 ^ _74159 : [(368 ^ _74159) ^ [_87432] : [model(_87432, _87216)]]], (393 ^ _74159) ^ [_88318, _88320] : [status(_88320, _88318, tca), 396 ^ _74159 : [(397 ^ _74159) ^ [_88468] : [model(_88468, _88320)], (399 ^ _74159) ^ [_88530] : [-(model(_88530, _88318))]]], (381 ^ _74159) ^ [_87948, _87950] : [-(status(_87950, _87948, tca)), -(model(384 ^ [_87948, _87950], _87950)), model(387 ^ [_87948, _87950], _87948)], (416 ^ _74159) ^ [_89128, _89130] : [status(_89130, _89128, wca), 419 ^ _74159 : [(420 ^ _74159) ^ [_89291] : [model(_89291, _89130)], (423 ^ _74159) ^ [] : [-(model(421 ^ [_89128, _89130], _89128))], (426 ^ _74159) ^ [] : [model(424 ^ [_89128, _89130], _89128)]]], (401 ^ _74159) ^ [_88679, _88681] : [-(status(_88681, _88679, wca)), -(model(404 ^ [_88679, _88681], _88681)), 409 ^ _74159 : [(410 ^ _74159) ^ [_88942] : [model(_88942, _88679)]], 411 ^ _74159 : [(412 ^ _74159) ^ [_89004] : [-(model(_89004, _88679))]]], (438 ^ _74159) ^ [_89981, _89983] : [status(_89983, _89981, csa), 442 ^ _74159 : [(443 ^ _74159) ^ [] : [-(model(441 ^ [_89981, _89983], _89983))], (445 ^ _74159) ^ [] : [-(model(441 ^ [_89981, _89983], not _89981))]]], (428 ^ _74159) ^ [_89659, _89661] : [-(status(_89661, _89659, csa)), 429 ^ _74159 : [(430 ^ _74159) ^ [_89754] : [model(_89754, _89661), model(_89754, not _89659)]]], (459 ^ _74159) ^ [_90748, _90750] : [status(_90750, _90748, uns), 462 ^ _74159 : [(463 ^ _74159) ^ [_90899] : [-(model(_90899, _90750))], (465 ^ _74159) ^ [_90961] : [-(model(_90961, not _90748))]]], (447 ^ _74159) ^ [_90375, _90377] : [-(status(_90377, _90375, uns)), model(450 ^ [_90375, _90377], _90377), model(453 ^ [_90375, _90377], not _90375)], (485 ^ _74159) ^ [_91655, _91657] : [status(_91657, _91655, noc), 489 ^ _74159 : [(490 ^ _74159) ^ [] : [-(model(488 ^ [_91655, _91657], _91657))], (492 ^ _74159) ^ [] : [-(model(488 ^ [_91655, _91657], _91655))], (495 ^ _74159) ^ [] : [-(model(493 ^ [_91655, _91657], _91657))], (497 ^ _74159) ^ [] : [-(model(493 ^ [_91655, _91657], not _91655))]]], (467 ^ _74159) ^ [_91092, _91094] : [-(status(_91094, _91092, noc)), 470 ^ _74159 : [(471 ^ _74159) ^ [_91238] : [model(_91238, _91094), model(_91238, _91092)]], 476 ^ _74159 : [(477 ^ _74159) ^ [_91423] : [model(_91423, _91094), model(_91423, not _91092)]]]], input).
% 0.68/1.37 ncf('1',plain,[status(520 ^ [thm, wca], 521 ^ [thm, wca], wca), 420 : model(96 ^ [521 ^ [thm, wca], 520 ^ [thm, wca]], 520 ^ [thm, wca])],start(416 ^ 0,bind([[_89128, _89130, _89291], [521 ^ [thm, wca], 520 ^ [thm, wca], 96 ^ [521 ^ [thm, wca], 520 ^ [thm, wca]]]]))).
% 0.68/1.37 ncf('1.1',plain,[-(status(520 ^ [thm, wca], 521 ^ [thm, wca], wca)), -(isa(wca, thm))],extension(519 ^ 1,bind([[_93233, _93235], [thm, wca]]))).
% 0.68/1.37 ncf('1.1.1',plain,[isa(wca, thm)],extension(689 ^ 2)).
% 0.68/1.37 ncf('1.2',plain,[-(model(96 ^ [521 ^ [thm, wca], 520 ^ [thm, wca]], 520 ^ [thm, wca])), -(status(520 ^ [thm, wca], 521 ^ [thm, wca], thm))],extension(95 ^ 3,bind([[_77676, _77678], [521 ^ [thm, wca], 520 ^ [thm, wca]]]))).
% 0.68/1.37 ncf('1.2.1',plain,[status(520 ^ [thm, wca], 521 ^ [thm, wca], thm), -(isa(wca, thm))],extension(519 ^ 4,bind([[_93233, _93235], [thm, wca]]))).
% 0.68/1.37 ncf('1.2.1.1',plain,[isa(wca, thm)],extension(689 ^ 5)).
% 0.68/1.37 %-----------------------------------------------------
% 0.68/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------