%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS215+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n032.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:30 EDT 2023
% Result : Theorem 0.64s 1.33s
% Output : Proof 0.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.09 % Problem : KRS215+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.02/0.10 % Command : nanocop.sh %s %d
% 0.09/0.29 % Computer : n032.cluster.edu
% 0.09/0.29 % Model : x86_64 x86_64
% 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.29 % Memory : 8042.1875MB
% 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.29 % CPULimit : 300
% 0.09/0.29 % WCLimit : 300
% 0.09/0.30 % DateTime : Thu May 18 23:07:49 EDT 2023
% 0.09/0.30 % CPUTime :
% 0.64/1.33
% 0.64/1.33 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.64/1.33 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.64/1.33 %-----------------------------------------------------
% 0.64/1.33 ncf(matrix, plain, [(689 ^ _75807) ^ [] : [nota(csa, thm)], (509 ^ _75807) ^ [_94398, _94400] : [mighta(_94400, _94398), 514 ^ _75807 : [(515 ^ _75807) ^ [] : [-(status(512 ^ [_94398, _94400], 513 ^ [_94398, _94400], _94400))], (517 ^ _75807) ^ [] : [-(status(512 ^ [_94398, _94400], 513 ^ [_94398, _94400], _94398))]]], (499 ^ _75807) ^ [_94053, _94055] : [-(mighta(_94055, _94053)), 500 ^ _75807 : [(501 ^ _75807) ^ [_94166, _94168] : [status(_94168, _94166, _94055), status(_94168, _94166, _94053)]]], (519 ^ _75807) ^ [_94881, _94883] : [522 ^ _75807 : [(523 ^ _75807) ^ [] : [-(status(520 ^ [_94881, _94883], 521 ^ [_94881, _94883], _94883))], (525 ^ _75807) ^ [] : [status(520 ^ [_94881, _94883], 521 ^ [_94881, _94883], _94881)]], -(isa(_94883, _94881))], (529 ^ _75807) ^ [_95285, _95287] : [isa(_95287, _95285), 532 ^ _75807 : [(533 ^ _75807) ^ [_95443, _95445] : [status(_95445, _95443, _95287), -(status(_95445, _95443, _95285))]]], (549 ^ _75807) ^ [_96059, _96061] : [nota(_96061, _96059), 554 ^ _75807 : [(555 ^ _75807) ^ [] : [-(status(552 ^ [_96059, _96061], 553 ^ [_96059, _96061], _96061))], (557 ^ _75807) ^ [] : [status(552 ^ [_96059, _96061], 553 ^ [_96059, _96061], _96059)]]], (539 ^ _75807) ^ [_95709, _95711] : [-(nota(_95711, _95709)), 540 ^ _75807 : [(541 ^ _75807) ^ [_95824, _95826] : [status(_95826, _95824, _95711), -(status(_95826, _95824, _95709))]]], (559 ^ _75807) ^ [_96547, _96549] : [562 ^ _75807 : [(563 ^ _75807) ^ [] : [-(status(560 ^ [_96547, _96549], 561 ^ [_96547, _96549], _96549))], (565 ^ _75807) ^ [] : [-(status(560 ^ [_96547, _96549], 561 ^ [_96547, _96549], _96547))]], -(nevera(_96549, _96547))], (569 ^ _75807) ^ [_96958, _96960] : [nevera(_96960, _96958), 572 ^ _75807 : [(573 ^ _75807) ^ [_97118, _97120] : [status(_97120, _97118, _96960), status(_97120, _97118, _96958)]]], (597 ^ _75807) ^ [_98001, _98003] : [xora(_98003, _98001), 600 ^ _75807 : [(601 ^ _75807) ^ [_98170, _98172] : [602 ^ _75807 : [(603 ^ _75807) ^ [] : [-(status(_98172, _98170, _98003))], (605 ^ _75807) ^ [] : [status(_98172, _98170, _98001)]], 606 ^ _75807 : [(607 ^ _75807) ^ [] : [-(status(_98172, _98170, _98001))], (609 ^ _75807) ^ [] : [status(_98172, _98170, _98003)]]]]], (579 ^ _75807) ^ [_97385, _97387] : [-(xora(_97387, _97385)), 582 ^ _75807 : [(583 ^ _75807) ^ [] : [status(580 ^ [_97385, _97387], 581 ^ [_97385, _97387], _97387), -(status(580 ^ [_97385, _97387], 581 ^ [_97385, _97387], _97385))], (589 ^ _75807) ^ [] : [status(580 ^ [_97385, _97387], 581 ^ [_97385, _97387], _97385), -(status(580 ^ [_97385, _97387], 581 ^ [_97385, _97387], _97387))]]], (611 ^ _75807) ^ [_98577, _98579] : [612 ^ _75807 : [(613 ^ _75807) ^ [] : [-(model(_98579, _98577))], (615 ^ _75807) ^ [] : [model(_98579, not _98577)]], 616 ^ _75807 : [(617 ^ _75807) ^ [] : [-(model(_98579, not _98577))], (619 ^ _75807) ^ [] : [model(_98579, _98577)]]], (621 ^ _75807) ^ [_98973, _98975] : [model(_98975, _98973), model(_98975, not _98973)], (627 ^ _75807) ^ [_99140, _99142] : [-(model(_99142, not _99140)), -(model(_99142, _99140))], (634 ^ _75807) ^ [_99372] : [-(model(_99372, 632 ^ []))], (638 ^ _75807) ^ [] : [-(model(636 ^ [], 635 ^ []))], (641 ^ _75807) ^ [] : [model(639 ^ [], 635 ^ [])], (644 ^ _75807) ^ [_99731] : [model(_99731, 642 ^ [])], (649 ^ _75807) ^ [] : [-(model(647 ^ [], 645 ^ []))], (651 ^ _75807) ^ [] : [-(model(647 ^ [], 646 ^ []))], (654 ^ _75807) ^ [] : [model(652 ^ [], 645 ^ []), model(652 ^ [], 646 ^ [])], (682 ^ _75807) ^ [] : [-(model(678 ^ [], 679 ^ []))], (684 ^ _75807) ^ [] : [model(678 ^ [], 680 ^ [])], (687 ^ _75807) ^ [] : [-(model(685 ^ [], 680 ^ []))], (663 ^ _75807) ^ [] : [-(model(661 ^ [], 659 ^ []))], (672 ^ _75807) ^ [] : [model(670 ^ [], 659 ^ [])], (674 ^ _75807) ^ [] : [-(model(670 ^ [], 660 ^ []))], (677 ^ _75807) ^ [] : [model(675 ^ [], 660 ^ [])], (665 ^ _75807) ^ [_100584] : [model(_100584, 659 ^ []), -(model(_100584, 660 ^ []))], (2 ^ _75807) ^ [_75969, _75971] : [3 ^ _75807 : [(4 ^ _75807) ^ [_76075] : [model(_76075, _75971)], (7 ^ _75807) ^ [] : [-(model(5 ^ [_75969, _75971], _75969))]], -(status(_75971, _75969, unp))], (11 ^ _75807) ^ [_76290, _76292] : [status(_76292, _76290, unp), -(model(16 ^ [_76290, _76292], _76292)), 19 ^ _75807 : [(20 ^ _75807) ^ [_76554] : [model(_76554, _76290)]]], (22 ^ _75807) ^ [_76705, _76707] : [24 ^ _75807 : [(25 ^ _75807) ^ [] : [-(model(23 ^ [_76705, _76707], _76707))], (27 ^ _75807) ^ [_76905] : [model(_76905, _76705)]], -(status(_76707, _76705, sap))], (31 ^ _75807) ^ [_77022, _77024] : [status(_77024, _77022, sap), 36 ^ _75807 : [(37 ^ _75807) ^ [_77184] : [model(_77184, _77024)]], -(model(38 ^ [_77022, _77024], _77022))], (42 ^ _75807) ^ [_77433, _77435] : [-(status(_77435, _77433, esa)), 46 ^ _75807 : [(47 ^ _75807) ^ [] : [-(model(45 ^ [_77433, _77435], _77435))], (49 ^ _75807) ^ [_77676] : [model(_77676, _77433)]], 51 ^ _75807 : [(52 ^ _75807) ^ [] : [-(model(50 ^ [_77433, _77435], _77433))], (54 ^ _75807) ^ [_77857] : [model(_77857, _77435)]]], (58 ^ _75807) ^ [_77979, _77981] : [status(_77981, _77979, esa), 61 ^ _75807 : [(62 ^ _75807) ^ [] : [63 ^ _75807 : [(64 ^ _75807) ^ [_78170] : [model(_78170, _77981)]], -(model(65 ^ [_77979, _77981], _77979))], (69 ^ _75807) ^ [] : [70 ^ _75807 : [(71 ^ _75807) ^ [_78368] : [model(_78368, _77979)]], -(model(72 ^ [_77979, _77981], _77981))]]], (86 ^ _75807) ^ [_78936, _78938] : [status(_78938, _78936, sat), 90 ^ _75807 : [(91 ^ _75807) ^ [] : [-(model(89 ^ [_78936, _78938], _78938))], (93 ^ _75807) ^ [] : [-(model(89 ^ [_78936, _78938], _78936))]]], (76 ^ _75807) ^ [_78620, _78622] : [-(status(_78622, _78620, sat)), 77 ^ _75807 : [(78 ^ _75807) ^ [_78713] : [model(_78713, _78622), model(_78713, _78620)]]], (95 ^ _75807) ^ [_79324, _79326] : [97 ^ _75807 : [(98 ^ _75807) ^ [] : [-(model(96 ^ [_79324, _79326], _79326))], (100 ^ _75807) ^ [] : [model(96 ^ [_79324, _79326], _79324)]], -(status(_79326, _79324, thm))], (104 ^ _75807) ^ [_79633, _79635] : [status(_79635, _79633, thm), 107 ^ _75807 : [(108 ^ _75807) ^ [_79772] : [model(_79772, _79635), -(model(_79772, _79633))]]], (114 ^ _75807) ^ [_80028, _80030] : [-(status(_80030, _80028, eqv)), 117 ^ _75807 : [(118 ^ _75807) ^ [_80150] : [model(_80150, _80030)]], 122 ^ _75807 : [(123 ^ _75807) ^ [] : [-(model(119 ^ [_80028, _80030], _80030))], (125 ^ _75807) ^ [] : [model(119 ^ [_80028, _80030], _80028)]], 126 ^ _75807 : [(127 ^ _75807) ^ [] : [-(model(119 ^ [_80028, _80030], _80028))], (129 ^ _75807) ^ [] : [model(119 ^ [_80028, _80030], _80030)]]], (133 ^ _75807) ^ [_80623, _80625] : [status(_80625, _80623, eqv), 137 ^ _75807 : [(138 ^ _75807) ^ [] : [-(model(136 ^ [_80623, _80625], _80625))], (140 ^ _75807) ^ [_80920] : [model(_80920, _80625), -(model(_80920, _80623))], (146 ^ _75807) ^ [_81092] : [model(_81092, _80623), -(model(_81092, _80625))]]], (163 ^ _75807) ^ [_81684, _81686] : [status(_81686, _81684, tac), 167 ^ _75807 : [(168 ^ _75807) ^ [] : [-(model(166 ^ [_81684, _81686], _81686))], (170 ^ _75807) ^ [_81931] : [-(model(_81931, _81684))]]], (152 ^ _75807) ^ [_81352, _81354] : [-(status(_81354, _81352, tac)), 155 ^ _75807 : [(156 ^ _75807) ^ [_81468] : [model(_81468, _81354)]], model(157 ^ [_81352, _81354], _81352)], (193 ^ _75807) ^ [_82746, _82748] : [status(_82748, _82746, wec), 197 ^ _75807 : [(198 ^ _75807) ^ [] : [-(model(196 ^ [_82746, _82748], _82748))], (207 ^ _75807) ^ [] : [-(model(205 ^ [_82746, _82748], _82746))], (209 ^ _75807) ^ [] : [model(205 ^ [_82746, _82748], _82748)], (200 ^ _75807) ^ [_83053] : [model(_83053, _82748), -(model(_83053, _82746))]]], (172 ^ _75807) ^ [_82080, _82082] : [-(status(_82082, _82080, wec)), 175 ^ _75807 : [(176 ^ _75807) ^ [_82221] : [model(_82221, _82082)]], 180 ^ _75807 : [(181 ^ _75807) ^ [] : [-(model(179 ^ [_82080, _82082], _82082))], (183 ^ _75807) ^ [] : [model(179 ^ [_82080, _82082], _82080)]], 184 ^ _75807 : [(185 ^ _75807) ^ [_82510] : [model(_82510, _82080), -(model(_82510, _82082))]]], (211 ^ _75807) ^ [_83495, _83497] : [-(status(_83497, _83495, eth)), 214 ^ _75807 : [(215 ^ _75807) ^ [_83630] : [model(_83630, _83497)]], 218 ^ _75807 : [(219 ^ _75807) ^ [_83726] : [-(model(_83726, _83497))]], 223 ^ _75807 : [(224 ^ _75807) ^ [] : [-(model(220 ^ [_83495, _83497], _83497))], (226 ^ _75807) ^ [] : [model(220 ^ [_83495, _83497], _83495)]], 227 ^ _75807 : [(228 ^ _75807) ^ [] : [-(model(220 ^ [_83495, _83497], _83495))], (230 ^ _75807) ^ [] : [model(220 ^ [_83495, _83497], _83497)]]], (234 ^ _75807) ^ [_84204, _84206] : [status(_84206, _84204, eth), 238 ^ _75807 : [(239 ^ _75807) ^ [] : [-(model(237 ^ [_84204, _84206], _84206))], (242 ^ _75807) ^ [] : [model(240 ^ [_84204, _84206], _84206)], (244 ^ _75807) ^ [_84633] : [model(_84633, _84206), -(model(_84633, _84204))], (250 ^ _75807) ^ [_84805] : [model(_84805, _84204), -(model(_84805, _84206))]]], (267 ^ _75807) ^ [_85390, _85392] : [status(_85392, _85390, tau), 270 ^ _75807 : [(271 ^ _75807) ^ [_85534] : [-(model(_85534, _85392))], (273 ^ _75807) ^ [_85582] : [-(model(_85582, _85390))]]], (256 ^ _75807) ^ [_85067, _85069] : [-(status(_85069, _85067, tau)), model(257 ^ [_85067, _85069], _85069), model(257 ^ [_85067, _85069], _85067)], (290 ^ _75807) ^ [_86177, _86179] : [status(_86179, _86177, wtc), 294 ^ _75807 : [(295 ^ _75807) ^ [] : [-(model(293 ^ [_86177, _86179], _86179))], (298 ^ _75807) ^ [] : [model(296 ^ [_86177, _86179], _86179)], (300 ^ _75807) ^ [_86556] : [-(model(_86556, _86177))]]], (275 ^ _75807) ^ [_85731, _85733] : [-(status(_85733, _85731, wtc)), 278 ^ _75807 : [(279 ^ _75807) ^ [_85860] : [model(_85860, _85733)]], 282 ^ _75807 : [(283 ^ _75807) ^ [_85956] : [-(model(_85956, _85733))]], model(284 ^ [_85731, _85733], _85731)], (327 ^ _75807) ^ [_87487, _87489] : [status(_87489, _87487, wth), 331 ^ _75807 : [(332 ^ _75807) ^ [] : [-(model(330 ^ [_87487, _87489], _87489))], (341 ^ _75807) ^ [] : [-(model(339 ^ [_87487, _87489], _87487))], (343 ^ _75807) ^ [] : [model(339 ^ [_87487, _87489], _87489)], (346 ^ _75807) ^ [] : [model(344 ^ [_87487, _87489], _87487)], (334 ^ _75807) ^ [_87807] : [model(_87807, _87489), -(model(_87807, _87487))]]], (302 ^ _75807) ^ [_86707, _86709] : [-(status(_86709, _86707, wth)), 305 ^ _75807 : [(306 ^ _75807) ^ [_86861] : [model(_86861, _86709)]], 310 ^ _75807 : [(311 ^ _75807) ^ [] : [-(model(309 ^ [_86707, _86709], _86709))], (313 ^ _75807) ^ [] : [model(309 ^ [_86707, _86709], _86707)]], 322 ^ _75807 : [(323 ^ _75807) ^ [_87357] : [-(model(_87357, _86707))]], 316 ^ _75807 : [(317 ^ _75807) ^ [_87184] : [model(_87184, _86707), -(model(_87184, _86709))]]], (348 ^ _75807) ^ [_88374, _88376] : [-(model(349 ^ [_88374, _88376], _88376)), -(status(_88376, _88374, cax))], (355 ^ _75807) ^ [_88598, _88600] : [status(_88600, _88598, cax), 358 ^ _75807 : [(359 ^ _75807) ^ [_88717] : [model(_88717, _88600)]]], (372 ^ _75807) ^ [_89199, _89201] : [status(_89201, _89199, sca), 375 ^ _75807 : [(376 ^ _75807) ^ [_89349] : [model(_89349, _89201)], (379 ^ _75807) ^ [] : [-(model(377 ^ [_89199, _89201], _89199))]]], (361 ^ _75807) ^ [_88864, _88866] : [-(status(_88866, _88864, sca)), -(model(364 ^ [_88864, _88866], _88866)), 367 ^ _75807 : [(368 ^ _75807) ^ [_89080] : [model(_89080, _88864)]]], (393 ^ _75807) ^ [_89966, _89968] : [status(_89968, _89966, tca), 396 ^ _75807 : [(397 ^ _75807) ^ [_90116] : [model(_90116, _89968)], (399 ^ _75807) ^ [_90178] : [-(model(_90178, _89966))]]], (381 ^ _75807) ^ [_89596, _89598] : [-(status(_89598, _89596, tca)), -(model(384 ^ [_89596, _89598], _89598)), model(387 ^ [_89596, _89598], _89596)], (416 ^ _75807) ^ [_90776, _90778] : [status(_90778, _90776, wca), 419 ^ _75807 : [(420 ^ _75807) ^ [_90939] : [model(_90939, _90778)], (423 ^ _75807) ^ [] : [-(model(421 ^ [_90776, _90778], _90776))], (426 ^ _75807) ^ [] : [model(424 ^ [_90776, _90778], _90776)]]], (401 ^ _75807) ^ [_90327, _90329] : [-(status(_90329, _90327, wca)), -(model(404 ^ [_90327, _90329], _90329)), 409 ^ _75807 : [(410 ^ _75807) ^ [_90590] : [model(_90590, _90327)]], 411 ^ _75807 : [(412 ^ _75807) ^ [_90652] : [-(model(_90652, _90327))]]], (438 ^ _75807) ^ [_91629, _91631] : [status(_91631, _91629, csa), 442 ^ _75807 : [(443 ^ _75807) ^ [] : [-(model(441 ^ [_91629, _91631], _91631))], (445 ^ _75807) ^ [] : [-(model(441 ^ [_91629, _91631], not _91629))]]], (428 ^ _75807) ^ [_91307, _91309] : [-(status(_91309, _91307, csa)), 429 ^ _75807 : [(430 ^ _75807) ^ [_91402] : [model(_91402, _91309), model(_91402, not _91307)]]], (459 ^ _75807) ^ [_92396, _92398] : [status(_92398, _92396, uns), 462 ^ _75807 : [(463 ^ _75807) ^ [_92547] : [-(model(_92547, _92398))], (465 ^ _75807) ^ [_92609] : [-(model(_92609, not _92396))]]], (447 ^ _75807) ^ [_92023, _92025] : [-(status(_92025, _92023, uns)), model(450 ^ [_92023, _92025], _92025), model(453 ^ [_92023, _92025], not _92023)], (485 ^ _75807) ^ [_93303, _93305] : [status(_93305, _93303, noc), 489 ^ _75807 : [(490 ^ _75807) ^ [] : [-(model(488 ^ [_93303, _93305], _93305))], (492 ^ _75807) ^ [] : [-(model(488 ^ [_93303, _93305], _93303))], (495 ^ _75807) ^ [] : [-(model(493 ^ [_93303, _93305], _93305))], (497 ^ _75807) ^ [] : [-(model(493 ^ [_93303, _93305], not _93303))]]], (467 ^ _75807) ^ [_92740, _92742] : [-(status(_92742, _92740, noc)), 470 ^ _75807 : [(471 ^ _75807) ^ [_92886] : [model(_92886, _92742), model(_92886, _92740)]], 476 ^ _75807 : [(477 ^ _75807) ^ [_93071] : [model(_93071, _92742), model(_93071, not _92740)]]]], input).
% 0.64/1.33 ncf('1',plain,[nota(csa, thm)],start(689 ^ 0)).
% 0.64/1.33 ncf('1.1',plain,[-(nota(csa, thm)), 541 : status(not 635 ^ [], 635 ^ [], csa), 541 : -(status(not 635 ^ [], 635 ^ [], thm))],extension(539 ^ 1,bind([[_95709, _95711, _95824, _95826], [thm, csa, 635 ^ [], not 635 ^ []]]))).
% 0.64/1.33 ncf('1.1.1',plain,[-(status(not 635 ^ [], 635 ^ [], csa)), 430 : model(639 ^ [], not 635 ^ []), 430 : model(639 ^ [], not 635 ^ [])],extension(428 ^ 4,bind([[_91307, _91309, _91402], [635 ^ [], not 635 ^ [], 639 ^ []]]))).
% 0.64/1.33 ncf('1.1.1.1',plain,[-(model(639 ^ [], not 635 ^ [])), 613 : -(model(639 ^ [], 635 ^ []))],extension(611 ^ 7,bind([[_98577, _98579], [635 ^ [], 639 ^ []]]))).
% 0.64/1.33 ncf('1.1.1.1.1',plain,[model(639 ^ [], 635 ^ [])],extension(641 ^ 10)).
% 0.64/1.33 ncf('1.1.1.2',plain,[-(model(639 ^ [], not 635 ^ [])), 613 : -(model(639 ^ [], 635 ^ []))],extension(611 ^ 7,bind([[_98577, _98579], [635 ^ [], 639 ^ []]]))).
% 0.64/1.33 ncf('1.1.1.2.1',plain,[model(639 ^ [], 635 ^ [])],extension(641 ^ 10)).
% 0.64/1.33 ncf('1.1.2',plain,[status(not 635 ^ [], 635 ^ [], thm), 108 : model(639 ^ [], not 635 ^ []), 108 : -(model(639 ^ [], 635 ^ []))],extension(104 ^ 4,bind([[_79633, _79635, _79772], [635 ^ [], not 635 ^ [], 639 ^ []]]))).
% 0.64/1.33 ncf('1.1.2.1',plain,[-(model(639 ^ [], not 635 ^ [])), 613 : -(model(639 ^ [], 635 ^ []))],extension(611 ^ 7,bind([[_98577, _98579], [635 ^ [], 639 ^ []]]))).
% 0.64/1.33 ncf('1.1.2.1.1',plain,[model(639 ^ [], 635 ^ [])],extension(641 ^ 10)).
% 0.64/1.33 ncf('1.1.2.2',plain,[model(639 ^ [], 635 ^ []), 615 : model(639 ^ [], not 635 ^ [])],extension(611 ^ 7,bind([[_98577, _98579], [635 ^ [], 639 ^ []]]))).
% 0.64/1.33 ncf('1.1.2.2.1',plain,[-(model(639 ^ [], not 635 ^ []))],lemmata('[1, 1].x')).
% 0.64/1.33 %-----------------------------------------------------
% 0.64/1.33 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------