%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS190+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n022.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.76s 1.38s
% Output : Proof 0.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS190+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n022.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:03:02 EDT 2023
% 0.13/0.33 % CPUTime :
% 0.76/1.38
% 0.76/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.76/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.76/1.38 %-----------------------------------------------------
% 0.76/1.38 ncf(matrix, plain, [(689 ^ _74990) ^ [] : [isa(tau, thm)], (509 ^ _74990) ^ [_93581, _93583] : [mighta(_93583, _93581), 514 ^ _74990 : [(515 ^ _74990) ^ [] : [-(status(512 ^ [_93581, _93583], 513 ^ [_93581, _93583], _93583))], (517 ^ _74990) ^ [] : [-(status(512 ^ [_93581, _93583], 513 ^ [_93581, _93583], _93581))]]], (499 ^ _74990) ^ [_93236, _93238] : [-(mighta(_93238, _93236)), 500 ^ _74990 : [(501 ^ _74990) ^ [_93349, _93351] : [status(_93351, _93349, _93238), status(_93351, _93349, _93236)]]], (519 ^ _74990) ^ [_94064, _94066] : [522 ^ _74990 : [(523 ^ _74990) ^ [] : [-(status(520 ^ [_94064, _94066], 521 ^ [_94064, _94066], _94066))], (525 ^ _74990) ^ [] : [status(520 ^ [_94064, _94066], 521 ^ [_94064, _94066], _94064)]], -(isa(_94066, _94064))], (529 ^ _74990) ^ [_94468, _94470] : [isa(_94470, _94468), 532 ^ _74990 : [(533 ^ _74990) ^ [_94626, _94628] : [status(_94628, _94626, _94470), -(status(_94628, _94626, _94468))]]], (549 ^ _74990) ^ [_95242, _95244] : [nota(_95244, _95242), 554 ^ _74990 : [(555 ^ _74990) ^ [] : [-(status(552 ^ [_95242, _95244], 553 ^ [_95242, _95244], _95244))], (557 ^ _74990) ^ [] : [status(552 ^ [_95242, _95244], 553 ^ [_95242, _95244], _95242)]]], (539 ^ _74990) ^ [_94892, _94894] : [-(nota(_94894, _94892)), 540 ^ _74990 : [(541 ^ _74990) ^ [_95007, _95009] : [status(_95009, _95007, _94894), -(status(_95009, _95007, _94892))]]], (559 ^ _74990) ^ [_95730, _95732] : [562 ^ _74990 : [(563 ^ _74990) ^ [] : [-(status(560 ^ [_95730, _95732], 561 ^ [_95730, _95732], _95732))], (565 ^ _74990) ^ [] : [-(status(560 ^ [_95730, _95732], 561 ^ [_95730, _95732], _95730))]], -(nevera(_95732, _95730))], (569 ^ _74990) ^ [_96141, _96143] : [nevera(_96143, _96141), 572 ^ _74990 : [(573 ^ _74990) ^ [_96301, _96303] : [status(_96303, _96301, _96143), status(_96303, _96301, _96141)]]], (597 ^ _74990) ^ [_97184, _97186] : [xora(_97186, _97184), 600 ^ _74990 : [(601 ^ _74990) ^ [_97353, _97355] : [602 ^ _74990 : [(603 ^ _74990) ^ [] : [-(status(_97355, _97353, _97186))], (605 ^ _74990) ^ [] : [status(_97355, _97353, _97184)]], 606 ^ _74990 : [(607 ^ _74990) ^ [] : [-(status(_97355, _97353, _97184))], (609 ^ _74990) ^ [] : [status(_97355, _97353, _97186)]]]]], (579 ^ _74990) ^ [_96568, _96570] : [-(xora(_96570, _96568)), 582 ^ _74990 : [(583 ^ _74990) ^ [] : [status(580 ^ [_96568, _96570], 581 ^ [_96568, _96570], _96570), -(status(580 ^ [_96568, _96570], 581 ^ [_96568, _96570], _96568))], (589 ^ _74990) ^ [] : [status(580 ^ [_96568, _96570], 581 ^ [_96568, _96570], _96568), -(status(580 ^ [_96568, _96570], 581 ^ [_96568, _96570], _96570))]]], (611 ^ _74990) ^ [_97760, _97762] : [612 ^ _74990 : [(613 ^ _74990) ^ [] : [-(model(_97762, _97760))], (615 ^ _74990) ^ [] : [model(_97762, not _97760)]], 616 ^ _74990 : [(617 ^ _74990) ^ [] : [-(model(_97762, not _97760))], (619 ^ _74990) ^ [] : [model(_97762, _97760)]]], (621 ^ _74990) ^ [_98156, _98158] : [model(_98158, _98156), model(_98158, not _98156)], (627 ^ _74990) ^ [_98323, _98325] : [-(model(_98325, not _98323)), -(model(_98325, _98323))], (634 ^ _74990) ^ [_98555] : [-(model(_98555, 632 ^ []))], (638 ^ _74990) ^ [] : [-(model(636 ^ [], 635 ^ []))], (641 ^ _74990) ^ [] : [model(639 ^ [], 635 ^ [])], (644 ^ _74990) ^ [_98914] : [model(_98914, 642 ^ [])], (649 ^ _74990) ^ [] : [-(model(647 ^ [], 645 ^ []))], (651 ^ _74990) ^ [] : [-(model(647 ^ [], 646 ^ []))], (654 ^ _74990) ^ [] : [model(652 ^ [], 645 ^ []), model(652 ^ [], 646 ^ [])], (682 ^ _74990) ^ [] : [-(model(678 ^ [], 679 ^ []))], (684 ^ _74990) ^ [] : [model(678 ^ [], 680 ^ [])], (687 ^ _74990) ^ [] : [-(model(685 ^ [], 680 ^ []))], (663 ^ _74990) ^ [] : [-(model(661 ^ [], 659 ^ []))], (672 ^ _74990) ^ [] : [model(670 ^ [], 659 ^ [])], (674 ^ _74990) ^ [] : [-(model(670 ^ [], 660 ^ []))], (677 ^ _74990) ^ [] : [model(675 ^ [], 660 ^ [])], (665 ^ _74990) ^ [_99767] : [model(_99767, 659 ^ []), -(model(_99767, 660 ^ []))], (2 ^ _74990) ^ [_75152, _75154] : [3 ^ _74990 : [(4 ^ _74990) ^ [_75258] : [model(_75258, _75154)], (7 ^ _74990) ^ [] : [-(model(5 ^ [_75152, _75154], _75152))]], -(status(_75154, _75152, unp))], (11 ^ _74990) ^ [_75473, _75475] : [status(_75475, _75473, unp), -(model(16 ^ [_75473, _75475], _75475)), 19 ^ _74990 : [(20 ^ _74990) ^ [_75737] : [model(_75737, _75473)]]], (22 ^ _74990) ^ [_75888, _75890] : [24 ^ _74990 : [(25 ^ _74990) ^ [] : [-(model(23 ^ [_75888, _75890], _75890))], (27 ^ _74990) ^ [_76088] : [model(_76088, _75888)]], -(status(_75890, _75888, sap))], (31 ^ _74990) ^ [_76205, _76207] : [status(_76207, _76205, sap), 36 ^ _74990 : [(37 ^ _74990) ^ [_76367] : [model(_76367, _76207)]], -(model(38 ^ [_76205, _76207], _76205))], (42 ^ _74990) ^ [_76616, _76618] : [-(status(_76618, _76616, esa)), 46 ^ _74990 : [(47 ^ _74990) ^ [] : [-(model(45 ^ [_76616, _76618], _76618))], (49 ^ _74990) ^ [_76859] : [model(_76859, _76616)]], 51 ^ _74990 : [(52 ^ _74990) ^ [] : [-(model(50 ^ [_76616, _76618], _76616))], (54 ^ _74990) ^ [_77040] : [model(_77040, _76618)]]], (58 ^ _74990) ^ [_77162, _77164] : [status(_77164, _77162, esa), 61 ^ _74990 : [(62 ^ _74990) ^ [] : [63 ^ _74990 : [(64 ^ _74990) ^ [_77353] : [model(_77353, _77164)]], -(model(65 ^ [_77162, _77164], _77162))], (69 ^ _74990) ^ [] : [70 ^ _74990 : [(71 ^ _74990) ^ [_77551] : [model(_77551, _77162)]], -(model(72 ^ [_77162, _77164], _77164))]]], (86 ^ _74990) ^ [_78119, _78121] : [status(_78121, _78119, sat), 90 ^ _74990 : [(91 ^ _74990) ^ [] : [-(model(89 ^ [_78119, _78121], _78121))], (93 ^ _74990) ^ [] : [-(model(89 ^ [_78119, _78121], _78119))]]], (76 ^ _74990) ^ [_77803, _77805] : [-(status(_77805, _77803, sat)), 77 ^ _74990 : [(78 ^ _74990) ^ [_77896] : [model(_77896, _77805), model(_77896, _77803)]]], (95 ^ _74990) ^ [_78507, _78509] : [97 ^ _74990 : [(98 ^ _74990) ^ [] : [-(model(96 ^ [_78507, _78509], _78509))], (100 ^ _74990) ^ [] : [model(96 ^ [_78507, _78509], _78507)]], -(status(_78509, _78507, thm))], (104 ^ _74990) ^ [_78816, _78818] : [status(_78818, _78816, thm), 107 ^ _74990 : [(108 ^ _74990) ^ [_78955] : [model(_78955, _78818), -(model(_78955, _78816))]]], (114 ^ _74990) ^ [_79211, _79213] : [-(status(_79213, _79211, eqv)), 117 ^ _74990 : [(118 ^ _74990) ^ [_79333] : [model(_79333, _79213)]], 122 ^ _74990 : [(123 ^ _74990) ^ [] : [-(model(119 ^ [_79211, _79213], _79213))], (125 ^ _74990) ^ [] : [model(119 ^ [_79211, _79213], _79211)]], 126 ^ _74990 : [(127 ^ _74990) ^ [] : [-(model(119 ^ [_79211, _79213], _79211))], (129 ^ _74990) ^ [] : [model(119 ^ [_79211, _79213], _79213)]]], (133 ^ _74990) ^ [_79806, _79808] : [status(_79808, _79806, eqv), 137 ^ _74990 : [(138 ^ _74990) ^ [] : [-(model(136 ^ [_79806, _79808], _79808))], (140 ^ _74990) ^ [_80103] : [model(_80103, _79808), -(model(_80103, _79806))], (146 ^ _74990) ^ [_80275] : [model(_80275, _79806), -(model(_80275, _79808))]]], (163 ^ _74990) ^ [_80867, _80869] : [status(_80869, _80867, tac), 167 ^ _74990 : [(168 ^ _74990) ^ [] : [-(model(166 ^ [_80867, _80869], _80869))], (170 ^ _74990) ^ [_81114] : [-(model(_81114, _80867))]]], (152 ^ _74990) ^ [_80535, _80537] : [-(status(_80537, _80535, tac)), 155 ^ _74990 : [(156 ^ _74990) ^ [_80651] : [model(_80651, _80537)]], model(157 ^ [_80535, _80537], _80535)], (193 ^ _74990) ^ [_81929, _81931] : [status(_81931, _81929, wec), 197 ^ _74990 : [(198 ^ _74990) ^ [] : [-(model(196 ^ [_81929, _81931], _81931))], (207 ^ _74990) ^ [] : [-(model(205 ^ [_81929, _81931], _81929))], (209 ^ _74990) ^ [] : [model(205 ^ [_81929, _81931], _81931)], (200 ^ _74990) ^ [_82236] : [model(_82236, _81931), -(model(_82236, _81929))]]], (172 ^ _74990) ^ [_81263, _81265] : [-(status(_81265, _81263, wec)), 175 ^ _74990 : [(176 ^ _74990) ^ [_81404] : [model(_81404, _81265)]], 180 ^ _74990 : [(181 ^ _74990) ^ [] : [-(model(179 ^ [_81263, _81265], _81265))], (183 ^ _74990) ^ [] : [model(179 ^ [_81263, _81265], _81263)]], 184 ^ _74990 : [(185 ^ _74990) ^ [_81693] : [model(_81693, _81263), -(model(_81693, _81265))]]], (211 ^ _74990) ^ [_82678, _82680] : [-(status(_82680, _82678, eth)), 214 ^ _74990 : [(215 ^ _74990) ^ [_82813] : [model(_82813, _82680)]], 218 ^ _74990 : [(219 ^ _74990) ^ [_82909] : [-(model(_82909, _82680))]], 223 ^ _74990 : [(224 ^ _74990) ^ [] : [-(model(220 ^ [_82678, _82680], _82680))], (226 ^ _74990) ^ [] : [model(220 ^ [_82678, _82680], _82678)]], 227 ^ _74990 : [(228 ^ _74990) ^ [] : [-(model(220 ^ [_82678, _82680], _82678))], (230 ^ _74990) ^ [] : [model(220 ^ [_82678, _82680], _82680)]]], (234 ^ _74990) ^ [_83387, _83389] : [status(_83389, _83387, eth), 238 ^ _74990 : [(239 ^ _74990) ^ [] : [-(model(237 ^ [_83387, _83389], _83389))], (242 ^ _74990) ^ [] : [model(240 ^ [_83387, _83389], _83389)], (244 ^ _74990) ^ [_83816] : [model(_83816, _83389), -(model(_83816, _83387))], (250 ^ _74990) ^ [_83988] : [model(_83988, _83387), -(model(_83988, _83389))]]], (267 ^ _74990) ^ [_84573, _84575] : [status(_84575, _84573, tau), 270 ^ _74990 : [(271 ^ _74990) ^ [_84717] : [-(model(_84717, _84575))], (273 ^ _74990) ^ [_84765] : [-(model(_84765, _84573))]]], (256 ^ _74990) ^ [_84250, _84252] : [-(status(_84252, _84250, tau)), model(257 ^ [_84250, _84252], _84252), model(257 ^ [_84250, _84252], _84250)], (290 ^ _74990) ^ [_85360, _85362] : [status(_85362, _85360, wtc), 294 ^ _74990 : [(295 ^ _74990) ^ [] : [-(model(293 ^ [_85360, _85362], _85362))], (298 ^ _74990) ^ [] : [model(296 ^ [_85360, _85362], _85362)], (300 ^ _74990) ^ [_85739] : [-(model(_85739, _85360))]]], (275 ^ _74990) ^ [_84914, _84916] : [-(status(_84916, _84914, wtc)), 278 ^ _74990 : [(279 ^ _74990) ^ [_85043] : [model(_85043, _84916)]], 282 ^ _74990 : [(283 ^ _74990) ^ [_85139] : [-(model(_85139, _84916))]], model(284 ^ [_84914, _84916], _84914)], (327 ^ _74990) ^ [_86670, _86672] : [status(_86672, _86670, wth), 331 ^ _74990 : [(332 ^ _74990) ^ [] : [-(model(330 ^ [_86670, _86672], _86672))], (341 ^ _74990) ^ [] : [-(model(339 ^ [_86670, _86672], _86670))], (343 ^ _74990) ^ [] : [model(339 ^ [_86670, _86672], _86672)], (346 ^ _74990) ^ [] : [model(344 ^ [_86670, _86672], _86670)], (334 ^ _74990) ^ [_86990] : [model(_86990, _86672), -(model(_86990, _86670))]]], (302 ^ _74990) ^ [_85890, _85892] : [-(status(_85892, _85890, wth)), 305 ^ _74990 : [(306 ^ _74990) ^ [_86044] : [model(_86044, _85892)]], 310 ^ _74990 : [(311 ^ _74990) ^ [] : [-(model(309 ^ [_85890, _85892], _85892))], (313 ^ _74990) ^ [] : [model(309 ^ [_85890, _85892], _85890)]], 322 ^ _74990 : [(323 ^ _74990) ^ [_86540] : [-(model(_86540, _85890))]], 316 ^ _74990 : [(317 ^ _74990) ^ [_86367] : [model(_86367, _85890), -(model(_86367, _85892))]]], (348 ^ _74990) ^ [_87557, _87559] : [-(model(349 ^ [_87557, _87559], _87559)), -(status(_87559, _87557, cax))], (355 ^ _74990) ^ [_87781, _87783] : [status(_87783, _87781, cax), 358 ^ _74990 : [(359 ^ _74990) ^ [_87900] : [model(_87900, _87783)]]], (372 ^ _74990) ^ [_88382, _88384] : [status(_88384, _88382, sca), 375 ^ _74990 : [(376 ^ _74990) ^ [_88532] : [model(_88532, _88384)], (379 ^ _74990) ^ [] : [-(model(377 ^ [_88382, _88384], _88382))]]], (361 ^ _74990) ^ [_88047, _88049] : [-(status(_88049, _88047, sca)), -(model(364 ^ [_88047, _88049], _88049)), 367 ^ _74990 : [(368 ^ _74990) ^ [_88263] : [model(_88263, _88047)]]], (393 ^ _74990) ^ [_89149, _89151] : [status(_89151, _89149, tca), 396 ^ _74990 : [(397 ^ _74990) ^ [_89299] : [model(_89299, _89151)], (399 ^ _74990) ^ [_89361] : [-(model(_89361, _89149))]]], (381 ^ _74990) ^ [_88779, _88781] : [-(status(_88781, _88779, tca)), -(model(384 ^ [_88779, _88781], _88781)), model(387 ^ [_88779, _88781], _88779)], (416 ^ _74990) ^ [_89959, _89961] : [status(_89961, _89959, wca), 419 ^ _74990 : [(420 ^ _74990) ^ [_90122] : [model(_90122, _89961)], (423 ^ _74990) ^ [] : [-(model(421 ^ [_89959, _89961], _89959))], (426 ^ _74990) ^ [] : [model(424 ^ [_89959, _89961], _89959)]]], (401 ^ _74990) ^ [_89510, _89512] : [-(status(_89512, _89510, wca)), -(model(404 ^ [_89510, _89512], _89512)), 409 ^ _74990 : [(410 ^ _74990) ^ [_89773] : [model(_89773, _89510)]], 411 ^ _74990 : [(412 ^ _74990) ^ [_89835] : [-(model(_89835, _89510))]]], (438 ^ _74990) ^ [_90812, _90814] : [status(_90814, _90812, csa), 442 ^ _74990 : [(443 ^ _74990) ^ [] : [-(model(441 ^ [_90812, _90814], _90814))], (445 ^ _74990) ^ [] : [-(model(441 ^ [_90812, _90814], not _90812))]]], (428 ^ _74990) ^ [_90490, _90492] : [-(status(_90492, _90490, csa)), 429 ^ _74990 : [(430 ^ _74990) ^ [_90585] : [model(_90585, _90492), model(_90585, not _90490)]]], (459 ^ _74990) ^ [_91579, _91581] : [status(_91581, _91579, uns), 462 ^ _74990 : [(463 ^ _74990) ^ [_91730] : [-(model(_91730, _91581))], (465 ^ _74990) ^ [_91792] : [-(model(_91792, not _91579))]]], (447 ^ _74990) ^ [_91206, _91208] : [-(status(_91208, _91206, uns)), model(450 ^ [_91206, _91208], _91208), model(453 ^ [_91206, _91208], not _91206)], (485 ^ _74990) ^ [_92486, _92488] : [status(_92488, _92486, noc), 489 ^ _74990 : [(490 ^ _74990) ^ [] : [-(model(488 ^ [_92486, _92488], _92488))], (492 ^ _74990) ^ [] : [-(model(488 ^ [_92486, _92488], _92486))], (495 ^ _74990) ^ [] : [-(model(493 ^ [_92486, _92488], _92488))], (497 ^ _74990) ^ [] : [-(model(493 ^ [_92486, _92488], not _92486))]]], (467 ^ _74990) ^ [_91923, _91925] : [-(status(_91925, _91923, noc)), 470 ^ _74990 : [(471 ^ _74990) ^ [_92069] : [model(_92069, _91925), model(_92069, _91923)]], 476 ^ _74990 : [(477 ^ _74990) ^ [_92254] : [model(_92254, _91925), model(_92254, not _91923)]]]], input).
% 0.76/1.38 ncf('1',plain,[nota(tau, thm), 557 : status(552 ^ [thm, tau], 553 ^ [thm, tau], thm)],start(549 ^ 0,bind([[_95242, _95244], [thm, tau]]))).
% 0.76/1.38 ncf('1.1',plain,[-(nota(tau, thm)), 541 : status(520 ^ [thm, tau], 521 ^ [thm, tau], tau), 541 : -(status(520 ^ [thm, tau], 521 ^ [thm, tau], thm))],extension(539 ^ 1,bind([[_94892, _94894, _95007, _95009], [thm, tau, 521 ^ [thm, tau], 520 ^ [thm, tau]]]))).
% 0.76/1.38 ncf('1.1.1',plain,[-(status(520 ^ [thm, tau], 521 ^ [thm, tau], tau)), -(isa(tau, thm))],extension(519 ^ 4,bind([[_94064, _94066], [thm, tau]]))).
% 0.76/1.38 ncf('1.1.1.1',plain,[isa(tau, thm)],extension(689 ^ 5)).
% 0.76/1.38 ncf('1.1.2',plain,[status(520 ^ [thm, tau], 521 ^ [thm, tau], thm), -(isa(tau, thm))],extension(519 ^ 4,bind([[_94064, _94066], [thm, tau]]))).
% 0.76/1.38 ncf('1.1.2.1',plain,[isa(tau, thm)],extension(689 ^ 5)).
% 0.76/1.38 ncf('1.2',plain,[-(status(552 ^ [thm, tau], 553 ^ [thm, tau], thm)), 100 : model(96 ^ [553 ^ [thm, tau], 552 ^ [thm, tau]], 553 ^ [thm, tau])],extension(95 ^ 3,bind([[_78507, _78509], [553 ^ [thm, tau], 552 ^ [thm, tau]]]))).
% 0.76/1.38 ncf('1.2.1',plain,[-(model(96 ^ [553 ^ [thm, tau], 552 ^ [thm, tau]], 553 ^ [thm, tau])), status(552 ^ [thm, tau], 553 ^ [thm, tau], tau)],extension(267 ^ 6,bind([[_84573, _84575, _84765], [553 ^ [thm, tau], 552 ^ [thm, tau], 96 ^ [553 ^ [thm, tau], 552 ^ [thm, tau]]]]))).
% 0.76/1.38 ncf('1.2.1.1',plain,[-(status(552 ^ [thm, tau], 553 ^ [thm, tau], tau))],extension(555 ^ 7)).
% 0.76/1.38 %-----------------------------------------------------
% 0.76/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------