%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS195+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n002.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.65s 1.38s
% Output : Proof 0.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS195+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n002.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:17:04 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.65/1.38
% 0.65/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.65/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.65/1.38 %-----------------------------------------------------
% 0.65/1.38 ncf(matrix, plain, [(689 ^ _74148) ^ [] : [isa(tca, thm)], (509 ^ _74148) ^ [_92739, _92741] : [mighta(_92741, _92739), 514 ^ _74148 : [(515 ^ _74148) ^ [] : [-(status(512 ^ [_92739, _92741], 513 ^ [_92739, _92741], _92741))], (517 ^ _74148) ^ [] : [-(status(512 ^ [_92739, _92741], 513 ^ [_92739, _92741], _92739))]]], (499 ^ _74148) ^ [_92394, _92396] : [-(mighta(_92396, _92394)), 500 ^ _74148 : [(501 ^ _74148) ^ [_92507, _92509] : [status(_92509, _92507, _92396), status(_92509, _92507, _92394)]]], (519 ^ _74148) ^ [_93222, _93224] : [522 ^ _74148 : [(523 ^ _74148) ^ [] : [-(status(520 ^ [_93222, _93224], 521 ^ [_93222, _93224], _93224))], (525 ^ _74148) ^ [] : [status(520 ^ [_93222, _93224], 521 ^ [_93222, _93224], _93222)]], -(isa(_93224, _93222))], (529 ^ _74148) ^ [_93626, _93628] : [isa(_93628, _93626), 532 ^ _74148 : [(533 ^ _74148) ^ [_93784, _93786] : [status(_93786, _93784, _93628), -(status(_93786, _93784, _93626))]]], (549 ^ _74148) ^ [_94400, _94402] : [nota(_94402, _94400), 554 ^ _74148 : [(555 ^ _74148) ^ [] : [-(status(552 ^ [_94400, _94402], 553 ^ [_94400, _94402], _94402))], (557 ^ _74148) ^ [] : [status(552 ^ [_94400, _94402], 553 ^ [_94400, _94402], _94400)]]], (539 ^ _74148) ^ [_94050, _94052] : [-(nota(_94052, _94050)), 540 ^ _74148 : [(541 ^ _74148) ^ [_94165, _94167] : [status(_94167, _94165, _94052), -(status(_94167, _94165, _94050))]]], (559 ^ _74148) ^ [_94888, _94890] : [562 ^ _74148 : [(563 ^ _74148) ^ [] : [-(status(560 ^ [_94888, _94890], 561 ^ [_94888, _94890], _94890))], (565 ^ _74148) ^ [] : [-(status(560 ^ [_94888, _94890], 561 ^ [_94888, _94890], _94888))]], -(nevera(_94890, _94888))], (569 ^ _74148) ^ [_95299, _95301] : [nevera(_95301, _95299), 572 ^ _74148 : [(573 ^ _74148) ^ [_95459, _95461] : [status(_95461, _95459, _95301), status(_95461, _95459, _95299)]]], (597 ^ _74148) ^ [_96342, _96344] : [xora(_96344, _96342), 600 ^ _74148 : [(601 ^ _74148) ^ [_96511, _96513] : [602 ^ _74148 : [(603 ^ _74148) ^ [] : [-(status(_96513, _96511, _96344))], (605 ^ _74148) ^ [] : [status(_96513, _96511, _96342)]], 606 ^ _74148 : [(607 ^ _74148) ^ [] : [-(status(_96513, _96511, _96342))], (609 ^ _74148) ^ [] : [status(_96513, _96511, _96344)]]]]], (579 ^ _74148) ^ [_95726, _95728] : [-(xora(_95728, _95726)), 582 ^ _74148 : [(583 ^ _74148) ^ [] : [status(580 ^ [_95726, _95728], 581 ^ [_95726, _95728], _95728), -(status(580 ^ [_95726, _95728], 581 ^ [_95726, _95728], _95726))], (589 ^ _74148) ^ [] : [status(580 ^ [_95726, _95728], 581 ^ [_95726, _95728], _95726), -(status(580 ^ [_95726, _95728], 581 ^ [_95726, _95728], _95728))]]], (611 ^ _74148) ^ [_96918, _96920] : [612 ^ _74148 : [(613 ^ _74148) ^ [] : [-(model(_96920, _96918))], (615 ^ _74148) ^ [] : [model(_96920, not _96918)]], 616 ^ _74148 : [(617 ^ _74148) ^ [] : [-(model(_96920, not _96918))], (619 ^ _74148) ^ [] : [model(_96920, _96918)]]], (621 ^ _74148) ^ [_97314, _97316] : [model(_97316, _97314), model(_97316, not _97314)], (627 ^ _74148) ^ [_97481, _97483] : [-(model(_97483, not _97481)), -(model(_97483, _97481))], (634 ^ _74148) ^ [_97713] : [-(model(_97713, 632 ^ []))], (638 ^ _74148) ^ [] : [-(model(636 ^ [], 635 ^ []))], (641 ^ _74148) ^ [] : [model(639 ^ [], 635 ^ [])], (644 ^ _74148) ^ [_98072] : [model(_98072, 642 ^ [])], (649 ^ _74148) ^ [] : [-(model(647 ^ [], 645 ^ []))], (651 ^ _74148) ^ [] : [-(model(647 ^ [], 646 ^ []))], (654 ^ _74148) ^ [] : [model(652 ^ [], 645 ^ []), model(652 ^ [], 646 ^ [])], (682 ^ _74148) ^ [] : [-(model(678 ^ [], 679 ^ []))], (684 ^ _74148) ^ [] : [model(678 ^ [], 680 ^ [])], (687 ^ _74148) ^ [] : [-(model(685 ^ [], 680 ^ []))], (663 ^ _74148) ^ [] : [-(model(661 ^ [], 659 ^ []))], (672 ^ _74148) ^ [] : [model(670 ^ [], 659 ^ [])], (674 ^ _74148) ^ [] : [-(model(670 ^ [], 660 ^ []))], (677 ^ _74148) ^ [] : [model(675 ^ [], 660 ^ [])], (665 ^ _74148) ^ [_98925] : [model(_98925, 659 ^ []), -(model(_98925, 660 ^ []))], (2 ^ _74148) ^ [_74310, _74312] : [3 ^ _74148 : [(4 ^ _74148) ^ [_74416] : [model(_74416, _74312)], (7 ^ _74148) ^ [] : [-(model(5 ^ [_74310, _74312], _74310))]], -(status(_74312, _74310, unp))], (11 ^ _74148) ^ [_74631, _74633] : [status(_74633, _74631, unp), -(model(16 ^ [_74631, _74633], _74633)), 19 ^ _74148 : [(20 ^ _74148) ^ [_74895] : [model(_74895, _74631)]]], (22 ^ _74148) ^ [_75046, _75048] : [24 ^ _74148 : [(25 ^ _74148) ^ [] : [-(model(23 ^ [_75046, _75048], _75048))], (27 ^ _74148) ^ [_75246] : [model(_75246, _75046)]], -(status(_75048, _75046, sap))], (31 ^ _74148) ^ [_75363, _75365] : [status(_75365, _75363, sap), 36 ^ _74148 : [(37 ^ _74148) ^ [_75525] : [model(_75525, _75365)]], -(model(38 ^ [_75363, _75365], _75363))], (42 ^ _74148) ^ [_75774, _75776] : [-(status(_75776, _75774, esa)), 46 ^ _74148 : [(47 ^ _74148) ^ [] : [-(model(45 ^ [_75774, _75776], _75776))], (49 ^ _74148) ^ [_76017] : [model(_76017, _75774)]], 51 ^ _74148 : [(52 ^ _74148) ^ [] : [-(model(50 ^ [_75774, _75776], _75774))], (54 ^ _74148) ^ [_76198] : [model(_76198, _75776)]]], (58 ^ _74148) ^ [_76320, _76322] : [status(_76322, _76320, esa), 61 ^ _74148 : [(62 ^ _74148) ^ [] : [63 ^ _74148 : [(64 ^ _74148) ^ [_76511] : [model(_76511, _76322)]], -(model(65 ^ [_76320, _76322], _76320))], (69 ^ _74148) ^ [] : [70 ^ _74148 : [(71 ^ _74148) ^ [_76709] : [model(_76709, _76320)]], -(model(72 ^ [_76320, _76322], _76322))]]], (86 ^ _74148) ^ [_77277, _77279] : [status(_77279, _77277, sat), 90 ^ _74148 : [(91 ^ _74148) ^ [] : [-(model(89 ^ [_77277, _77279], _77279))], (93 ^ _74148) ^ [] : [-(model(89 ^ [_77277, _77279], _77277))]]], (76 ^ _74148) ^ [_76961, _76963] : [-(status(_76963, _76961, sat)), 77 ^ _74148 : [(78 ^ _74148) ^ [_77054] : [model(_77054, _76963), model(_77054, _76961)]]], (95 ^ _74148) ^ [_77665, _77667] : [97 ^ _74148 : [(98 ^ _74148) ^ [] : [-(model(96 ^ [_77665, _77667], _77667))], (100 ^ _74148) ^ [] : [model(96 ^ [_77665, _77667], _77665)]], -(status(_77667, _77665, thm))], (104 ^ _74148) ^ [_77974, _77976] : [status(_77976, _77974, thm), 107 ^ _74148 : [(108 ^ _74148) ^ [_78113] : [model(_78113, _77976), -(model(_78113, _77974))]]], (114 ^ _74148) ^ [_78369, _78371] : [-(status(_78371, _78369, eqv)), 117 ^ _74148 : [(118 ^ _74148) ^ [_78491] : [model(_78491, _78371)]], 122 ^ _74148 : [(123 ^ _74148) ^ [] : [-(model(119 ^ [_78369, _78371], _78371))], (125 ^ _74148) ^ [] : [model(119 ^ [_78369, _78371], _78369)]], 126 ^ _74148 : [(127 ^ _74148) ^ [] : [-(model(119 ^ [_78369, _78371], _78369))], (129 ^ _74148) ^ [] : [model(119 ^ [_78369, _78371], _78371)]]], (133 ^ _74148) ^ [_78964, _78966] : [status(_78966, _78964, eqv), 137 ^ _74148 : [(138 ^ _74148) ^ [] : [-(model(136 ^ [_78964, _78966], _78966))], (140 ^ _74148) ^ [_79261] : [model(_79261, _78966), -(model(_79261, _78964))], (146 ^ _74148) ^ [_79433] : [model(_79433, _78964), -(model(_79433, _78966))]]], (163 ^ _74148) ^ [_80025, _80027] : [status(_80027, _80025, tac), 167 ^ _74148 : [(168 ^ _74148) ^ [] : [-(model(166 ^ [_80025, _80027], _80027))], (170 ^ _74148) ^ [_80272] : [-(model(_80272, _80025))]]], (152 ^ _74148) ^ [_79693, _79695] : [-(status(_79695, _79693, tac)), 155 ^ _74148 : [(156 ^ _74148) ^ [_79809] : [model(_79809, _79695)]], model(157 ^ [_79693, _79695], _79693)], (193 ^ _74148) ^ [_81087, _81089] : [status(_81089, _81087, wec), 197 ^ _74148 : [(198 ^ _74148) ^ [] : [-(model(196 ^ [_81087, _81089], _81089))], (207 ^ _74148) ^ [] : [-(model(205 ^ [_81087, _81089], _81087))], (209 ^ _74148) ^ [] : [model(205 ^ [_81087, _81089], _81089)], (200 ^ _74148) ^ [_81394] : [model(_81394, _81089), -(model(_81394, _81087))]]], (172 ^ _74148) ^ [_80421, _80423] : [-(status(_80423, _80421, wec)), 175 ^ _74148 : [(176 ^ _74148) ^ [_80562] : [model(_80562, _80423)]], 180 ^ _74148 : [(181 ^ _74148) ^ [] : [-(model(179 ^ [_80421, _80423], _80423))], (183 ^ _74148) ^ [] : [model(179 ^ [_80421, _80423], _80421)]], 184 ^ _74148 : [(185 ^ _74148) ^ [_80851] : [model(_80851, _80421), -(model(_80851, _80423))]]], (211 ^ _74148) ^ [_81836, _81838] : [-(status(_81838, _81836, eth)), 214 ^ _74148 : [(215 ^ _74148) ^ [_81971] : [model(_81971, _81838)]], 218 ^ _74148 : [(219 ^ _74148) ^ [_82067] : [-(model(_82067, _81838))]], 223 ^ _74148 : [(224 ^ _74148) ^ [] : [-(model(220 ^ [_81836, _81838], _81838))], (226 ^ _74148) ^ [] : [model(220 ^ [_81836, _81838], _81836)]], 227 ^ _74148 : [(228 ^ _74148) ^ [] : [-(model(220 ^ [_81836, _81838], _81836))], (230 ^ _74148) ^ [] : [model(220 ^ [_81836, _81838], _81838)]]], (234 ^ _74148) ^ [_82545, _82547] : [status(_82547, _82545, eth), 238 ^ _74148 : [(239 ^ _74148) ^ [] : [-(model(237 ^ [_82545, _82547], _82547))], (242 ^ _74148) ^ [] : [model(240 ^ [_82545, _82547], _82547)], (244 ^ _74148) ^ [_82974] : [model(_82974, _82547), -(model(_82974, _82545))], (250 ^ _74148) ^ [_83146] : [model(_83146, _82545), -(model(_83146, _82547))]]], (267 ^ _74148) ^ [_83731, _83733] : [status(_83733, _83731, tau), 270 ^ _74148 : [(271 ^ _74148) ^ [_83875] : [-(model(_83875, _83733))], (273 ^ _74148) ^ [_83923] : [-(model(_83923, _83731))]]], (256 ^ _74148) ^ [_83408, _83410] : [-(status(_83410, _83408, tau)), model(257 ^ [_83408, _83410], _83410), model(257 ^ [_83408, _83410], _83408)], (290 ^ _74148) ^ [_84518, _84520] : [status(_84520, _84518, wtc), 294 ^ _74148 : [(295 ^ _74148) ^ [] : [-(model(293 ^ [_84518, _84520], _84520))], (298 ^ _74148) ^ [] : [model(296 ^ [_84518, _84520], _84520)], (300 ^ _74148) ^ [_84897] : [-(model(_84897, _84518))]]], (275 ^ _74148) ^ [_84072, _84074] : [-(status(_84074, _84072, wtc)), 278 ^ _74148 : [(279 ^ _74148) ^ [_84201] : [model(_84201, _84074)]], 282 ^ _74148 : [(283 ^ _74148) ^ [_84297] : [-(model(_84297, _84074))]], model(284 ^ [_84072, _84074], _84072)], (327 ^ _74148) ^ [_85828, _85830] : [status(_85830, _85828, wth), 331 ^ _74148 : [(332 ^ _74148) ^ [] : [-(model(330 ^ [_85828, _85830], _85830))], (341 ^ _74148) ^ [] : [-(model(339 ^ [_85828, _85830], _85828))], (343 ^ _74148) ^ [] : [model(339 ^ [_85828, _85830], _85830)], (346 ^ _74148) ^ [] : [model(344 ^ [_85828, _85830], _85828)], (334 ^ _74148) ^ [_86148] : [model(_86148, _85830), -(model(_86148, _85828))]]], (302 ^ _74148) ^ [_85048, _85050] : [-(status(_85050, _85048, wth)), 305 ^ _74148 : [(306 ^ _74148) ^ [_85202] : [model(_85202, _85050)]], 310 ^ _74148 : [(311 ^ _74148) ^ [] : [-(model(309 ^ [_85048, _85050], _85050))], (313 ^ _74148) ^ [] : [model(309 ^ [_85048, _85050], _85048)]], 322 ^ _74148 : [(323 ^ _74148) ^ [_85698] : [-(model(_85698, _85048))]], 316 ^ _74148 : [(317 ^ _74148) ^ [_85525] : [model(_85525, _85048), -(model(_85525, _85050))]]], (348 ^ _74148) ^ [_86715, _86717] : [-(model(349 ^ [_86715, _86717], _86717)), -(status(_86717, _86715, cax))], (355 ^ _74148) ^ [_86939, _86941] : [status(_86941, _86939, cax), 358 ^ _74148 : [(359 ^ _74148) ^ [_87058] : [model(_87058, _86941)]]], (372 ^ _74148) ^ [_87540, _87542] : [status(_87542, _87540, sca), 375 ^ _74148 : [(376 ^ _74148) ^ [_87690] : [model(_87690, _87542)], (379 ^ _74148) ^ [] : [-(model(377 ^ [_87540, _87542], _87540))]]], (361 ^ _74148) ^ [_87205, _87207] : [-(status(_87207, _87205, sca)), -(model(364 ^ [_87205, _87207], _87207)), 367 ^ _74148 : [(368 ^ _74148) ^ [_87421] : [model(_87421, _87205)]]], (393 ^ _74148) ^ [_88307, _88309] : [status(_88309, _88307, tca), 396 ^ _74148 : [(397 ^ _74148) ^ [_88457] : [model(_88457, _88309)], (399 ^ _74148) ^ [_88519] : [-(model(_88519, _88307))]]], (381 ^ _74148) ^ [_87937, _87939] : [-(status(_87939, _87937, tca)), -(model(384 ^ [_87937, _87939], _87939)), model(387 ^ [_87937, _87939], _87937)], (416 ^ _74148) ^ [_89117, _89119] : [status(_89119, _89117, wca), 419 ^ _74148 : [(420 ^ _74148) ^ [_89280] : [model(_89280, _89119)], (423 ^ _74148) ^ [] : [-(model(421 ^ [_89117, _89119], _89117))], (426 ^ _74148) ^ [] : [model(424 ^ [_89117, _89119], _89117)]]], (401 ^ _74148) ^ [_88668, _88670] : [-(status(_88670, _88668, wca)), -(model(404 ^ [_88668, _88670], _88670)), 409 ^ _74148 : [(410 ^ _74148) ^ [_88931] : [model(_88931, _88668)]], 411 ^ _74148 : [(412 ^ _74148) ^ [_88993] : [-(model(_88993, _88668))]]], (438 ^ _74148) ^ [_89970, _89972] : [status(_89972, _89970, csa), 442 ^ _74148 : [(443 ^ _74148) ^ [] : [-(model(441 ^ [_89970, _89972], _89972))], (445 ^ _74148) ^ [] : [-(model(441 ^ [_89970, _89972], not _89970))]]], (428 ^ _74148) ^ [_89648, _89650] : [-(status(_89650, _89648, csa)), 429 ^ _74148 : [(430 ^ _74148) ^ [_89743] : [model(_89743, _89650), model(_89743, not _89648)]]], (459 ^ _74148) ^ [_90737, _90739] : [status(_90739, _90737, uns), 462 ^ _74148 : [(463 ^ _74148) ^ [_90888] : [-(model(_90888, _90739))], (465 ^ _74148) ^ [_90950] : [-(model(_90950, not _90737))]]], (447 ^ _74148) ^ [_90364, _90366] : [-(status(_90366, _90364, uns)), model(450 ^ [_90364, _90366], _90366), model(453 ^ [_90364, _90366], not _90364)], (485 ^ _74148) ^ [_91644, _91646] : [status(_91646, _91644, noc), 489 ^ _74148 : [(490 ^ _74148) ^ [] : [-(model(488 ^ [_91644, _91646], _91646))], (492 ^ _74148) ^ [] : [-(model(488 ^ [_91644, _91646], _91644))], (495 ^ _74148) ^ [] : [-(model(493 ^ [_91644, _91646], _91646))], (497 ^ _74148) ^ [] : [-(model(493 ^ [_91644, _91646], not _91644))]]], (467 ^ _74148) ^ [_91081, _91083] : [-(status(_91083, _91081, noc)), 470 ^ _74148 : [(471 ^ _74148) ^ [_91227] : [model(_91227, _91083), model(_91227, _91081)]], 476 ^ _74148 : [(477 ^ _74148) ^ [_91412] : [model(_91412, _91083), model(_91412, not _91081)]]]], input).
% 0.65/1.38 ncf('1',plain,[status(520 ^ [thm, tca], 521 ^ [thm, tca], tca), 397 : model(96 ^ [521 ^ [thm, tca], 520 ^ [thm, tca]], 520 ^ [thm, tca])],start(393 ^ 0,bind([[_88307, _88309, _88457], [521 ^ [thm, tca], 520 ^ [thm, tca], 96 ^ [521 ^ [thm, tca], 520 ^ [thm, tca]]]]))).
% 0.65/1.38 ncf('1.1',plain,[-(status(520 ^ [thm, tca], 521 ^ [thm, tca], tca)), -(isa(tca, thm))],extension(519 ^ 1,bind([[_93222, _93224], [thm, tca]]))).
% 0.65/1.38 ncf('1.1.1',plain,[isa(tca, thm)],extension(689 ^ 2)).
% 0.65/1.38 ncf('1.2',plain,[-(model(96 ^ [521 ^ [thm, tca], 520 ^ [thm, tca]], 520 ^ [thm, tca])), -(status(520 ^ [thm, tca], 521 ^ [thm, tca], thm))],extension(95 ^ 3,bind([[_77665, _77667], [521 ^ [thm, tca], 520 ^ [thm, tca]]]))).
% 0.65/1.38 ncf('1.2.1',plain,[status(520 ^ [thm, tca], 521 ^ [thm, tca], thm), -(isa(tca, thm))],extension(519 ^ 4,bind([[_93222, _93224], [thm, tca]]))).
% 0.65/1.38 ncf('1.2.1.1',plain,[isa(tca, thm)],extension(689 ^ 5)).
% 0.65/1.38 %-----------------------------------------------------
% 0.65/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------