%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS201+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n010.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:29 EDT 2023
% Result : Theorem 0.97s 1.37s
% Output : Proof 0.97s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : KRS201+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.12/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n010.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 22:50:12 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.97/1.37
% 0.97/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.97/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.97/1.37 %-----------------------------------------------------
% 0.97/1.37 ncf(matrix, plain, [(689 ^ _76381) ^ [] : [nota(sap, thm)], (509 ^ _76381) ^ [_94972, _94974] : [mighta(_94974, _94972), 514 ^ _76381 : [(515 ^ _76381) ^ [] : [-(status(512 ^ [_94972, _94974], 513 ^ [_94972, _94974], _94974))], (517 ^ _76381) ^ [] : [-(status(512 ^ [_94972, _94974], 513 ^ [_94972, _94974], _94972))]]], (499 ^ _76381) ^ [_94627, _94629] : [-(mighta(_94629, _94627)), 500 ^ _76381 : [(501 ^ _76381) ^ [_94740, _94742] : [status(_94742, _94740, _94629), status(_94742, _94740, _94627)]]], (519 ^ _76381) ^ [_95455, _95457] : [522 ^ _76381 : [(523 ^ _76381) ^ [] : [-(status(520 ^ [_95455, _95457], 521 ^ [_95455, _95457], _95457))], (525 ^ _76381) ^ [] : [status(520 ^ [_95455, _95457], 521 ^ [_95455, _95457], _95455)]], -(isa(_95457, _95455))], (529 ^ _76381) ^ [_95859, _95861] : [isa(_95861, _95859), 532 ^ _76381 : [(533 ^ _76381) ^ [_96017, _96019] : [status(_96019, _96017, _95861), -(status(_96019, _96017, _95859))]]], (549 ^ _76381) ^ [_96633, _96635] : [nota(_96635, _96633), 554 ^ _76381 : [(555 ^ _76381) ^ [] : [-(status(552 ^ [_96633, _96635], 553 ^ [_96633, _96635], _96635))], (557 ^ _76381) ^ [] : [status(552 ^ [_96633, _96635], 553 ^ [_96633, _96635], _96633)]]], (539 ^ _76381) ^ [_96283, _96285] : [-(nota(_96285, _96283)), 540 ^ _76381 : [(541 ^ _76381) ^ [_96398, _96400] : [status(_96400, _96398, _96285), -(status(_96400, _96398, _96283))]]], (559 ^ _76381) ^ [_97121, _97123] : [562 ^ _76381 : [(563 ^ _76381) ^ [] : [-(status(560 ^ [_97121, _97123], 561 ^ [_97121, _97123], _97123))], (565 ^ _76381) ^ [] : [-(status(560 ^ [_97121, _97123], 561 ^ [_97121, _97123], _97121))]], -(nevera(_97123, _97121))], (569 ^ _76381) ^ [_97532, _97534] : [nevera(_97534, _97532), 572 ^ _76381 : [(573 ^ _76381) ^ [_97692, _97694] : [status(_97694, _97692, _97534), status(_97694, _97692, _97532)]]], (597 ^ _76381) ^ [_98575, _98577] : [xora(_98577, _98575), 600 ^ _76381 : [(601 ^ _76381) ^ [_98744, _98746] : [602 ^ _76381 : [(603 ^ _76381) ^ [] : [-(status(_98746, _98744, _98577))], (605 ^ _76381) ^ [] : [status(_98746, _98744, _98575)]], 606 ^ _76381 : [(607 ^ _76381) ^ [] : [-(status(_98746, _98744, _98575))], (609 ^ _76381) ^ [] : [status(_98746, _98744, _98577)]]]]], (579 ^ _76381) ^ [_97959, _97961] : [-(xora(_97961, _97959)), 582 ^ _76381 : [(583 ^ _76381) ^ [] : [status(580 ^ [_97959, _97961], 581 ^ [_97959, _97961], _97961), -(status(580 ^ [_97959, _97961], 581 ^ [_97959, _97961], _97959))], (589 ^ _76381) ^ [] : [status(580 ^ [_97959, _97961], 581 ^ [_97959, _97961], _97959), -(status(580 ^ [_97959, _97961], 581 ^ [_97959, _97961], _97961))]]], (611 ^ _76381) ^ [_99151, _99153] : [612 ^ _76381 : [(613 ^ _76381) ^ [] : [-(model(_99153, _99151))], (615 ^ _76381) ^ [] : [model(_99153, not _99151)]], 616 ^ _76381 : [(617 ^ _76381) ^ [] : [-(model(_99153, not _99151))], (619 ^ _76381) ^ [] : [model(_99153, _99151)]]], (621 ^ _76381) ^ [_99547, _99549] : [model(_99549, _99547), model(_99549, not _99547)], (627 ^ _76381) ^ [_99714, _99716] : [-(model(_99716, not _99714)), -(model(_99716, _99714))], (634 ^ _76381) ^ [_99946] : [-(model(_99946, 632 ^ []))], (638 ^ _76381) ^ [] : [-(model(636 ^ [], 635 ^ []))], (641 ^ _76381) ^ [] : [model(639 ^ [], 635 ^ [])], (644 ^ _76381) ^ [_100305] : [model(_100305, 642 ^ [])], (649 ^ _76381) ^ [] : [-(model(647 ^ [], 645 ^ []))], (651 ^ _76381) ^ [] : [-(model(647 ^ [], 646 ^ []))], (654 ^ _76381) ^ [] : [model(652 ^ [], 645 ^ []), model(652 ^ [], 646 ^ [])], (682 ^ _76381) ^ [] : [-(model(678 ^ [], 679 ^ []))], (684 ^ _76381) ^ [] : [model(678 ^ [], 680 ^ [])], (687 ^ _76381) ^ [] : [-(model(685 ^ [], 680 ^ []))], (663 ^ _76381) ^ [] : [-(model(661 ^ [], 659 ^ []))], (672 ^ _76381) ^ [] : [model(670 ^ [], 659 ^ [])], (674 ^ _76381) ^ [] : [-(model(670 ^ [], 660 ^ []))], (677 ^ _76381) ^ [] : [model(675 ^ [], 660 ^ [])], (665 ^ _76381) ^ [_101158] : [model(_101158, 659 ^ []), -(model(_101158, 660 ^ []))], (2 ^ _76381) ^ [_76543, _76545] : [3 ^ _76381 : [(4 ^ _76381) ^ [_76649] : [model(_76649, _76545)], (7 ^ _76381) ^ [] : [-(model(5 ^ [_76543, _76545], _76543))]], -(status(_76545, _76543, unp))], (11 ^ _76381) ^ [_76864, _76866] : [status(_76866, _76864, unp), -(model(16 ^ [_76864, _76866], _76866)), 19 ^ _76381 : [(20 ^ _76381) ^ [_77128] : [model(_77128, _76864)]]], (22 ^ _76381) ^ [_77279, _77281] : [24 ^ _76381 : [(25 ^ _76381) ^ [] : [-(model(23 ^ [_77279, _77281], _77281))], (27 ^ _76381) ^ [_77479] : [model(_77479, _77279)]], -(status(_77281, _77279, sap))], (31 ^ _76381) ^ [_77596, _77598] : [status(_77598, _77596, sap), 36 ^ _76381 : [(37 ^ _76381) ^ [_77758] : [model(_77758, _77598)]], -(model(38 ^ [_77596, _77598], _77596))], (42 ^ _76381) ^ [_78007, _78009] : [-(status(_78009, _78007, esa)), 46 ^ _76381 : [(47 ^ _76381) ^ [] : [-(model(45 ^ [_78007, _78009], _78009))], (49 ^ _76381) ^ [_78250] : [model(_78250, _78007)]], 51 ^ _76381 : [(52 ^ _76381) ^ [] : [-(model(50 ^ [_78007, _78009], _78007))], (54 ^ _76381) ^ [_78431] : [model(_78431, _78009)]]], (58 ^ _76381) ^ [_78553, _78555] : [status(_78555, _78553, esa), 61 ^ _76381 : [(62 ^ _76381) ^ [] : [63 ^ _76381 : [(64 ^ _76381) ^ [_78744] : [model(_78744, _78555)]], -(model(65 ^ [_78553, _78555], _78553))], (69 ^ _76381) ^ [] : [70 ^ _76381 : [(71 ^ _76381) ^ [_78942] : [model(_78942, _78553)]], -(model(72 ^ [_78553, _78555], _78555))]]], (86 ^ _76381) ^ [_79510, _79512] : [status(_79512, _79510, sat), 90 ^ _76381 : [(91 ^ _76381) ^ [] : [-(model(89 ^ [_79510, _79512], _79512))], (93 ^ _76381) ^ [] : [-(model(89 ^ [_79510, _79512], _79510))]]], (76 ^ _76381) ^ [_79194, _79196] : [-(status(_79196, _79194, sat)), 77 ^ _76381 : [(78 ^ _76381) ^ [_79287] : [model(_79287, _79196), model(_79287, _79194)]]], (95 ^ _76381) ^ [_79898, _79900] : [97 ^ _76381 : [(98 ^ _76381) ^ [] : [-(model(96 ^ [_79898, _79900], _79900))], (100 ^ _76381) ^ [] : [model(96 ^ [_79898, _79900], _79898)]], -(status(_79900, _79898, thm))], (104 ^ _76381) ^ [_80207, _80209] : [status(_80209, _80207, thm), 107 ^ _76381 : [(108 ^ _76381) ^ [_80346] : [model(_80346, _80209), -(model(_80346, _80207))]]], (114 ^ _76381) ^ [_80602, _80604] : [-(status(_80604, _80602, eqv)), 117 ^ _76381 : [(118 ^ _76381) ^ [_80724] : [model(_80724, _80604)]], 122 ^ _76381 : [(123 ^ _76381) ^ [] : [-(model(119 ^ [_80602, _80604], _80604))], (125 ^ _76381) ^ [] : [model(119 ^ [_80602, _80604], _80602)]], 126 ^ _76381 : [(127 ^ _76381) ^ [] : [-(model(119 ^ [_80602, _80604], _80602))], (129 ^ _76381) ^ [] : [model(119 ^ [_80602, _80604], _80604)]]], (133 ^ _76381) ^ [_81197, _81199] : [status(_81199, _81197, eqv), 137 ^ _76381 : [(138 ^ _76381) ^ [] : [-(model(136 ^ [_81197, _81199], _81199))], (140 ^ _76381) ^ [_81494] : [model(_81494, _81199), -(model(_81494, _81197))], (146 ^ _76381) ^ [_81666] : [model(_81666, _81197), -(model(_81666, _81199))]]], (163 ^ _76381) ^ [_82258, _82260] : [status(_82260, _82258, tac), 167 ^ _76381 : [(168 ^ _76381) ^ [] : [-(model(166 ^ [_82258, _82260], _82260))], (170 ^ _76381) ^ [_82505] : [-(model(_82505, _82258))]]], (152 ^ _76381) ^ [_81926, _81928] : [-(status(_81928, _81926, tac)), 155 ^ _76381 : [(156 ^ _76381) ^ [_82042] : [model(_82042, _81928)]], model(157 ^ [_81926, _81928], _81926)], (193 ^ _76381) ^ [_83320, _83322] : [status(_83322, _83320, wec), 197 ^ _76381 : [(198 ^ _76381) ^ [] : [-(model(196 ^ [_83320, _83322], _83322))], (207 ^ _76381) ^ [] : [-(model(205 ^ [_83320, _83322], _83320))], (209 ^ _76381) ^ [] : [model(205 ^ [_83320, _83322], _83322)], (200 ^ _76381) ^ [_83627] : [model(_83627, _83322), -(model(_83627, _83320))]]], (172 ^ _76381) ^ [_82654, _82656] : [-(status(_82656, _82654, wec)), 175 ^ _76381 : [(176 ^ _76381) ^ [_82795] : [model(_82795, _82656)]], 180 ^ _76381 : [(181 ^ _76381) ^ [] : [-(model(179 ^ [_82654, _82656], _82656))], (183 ^ _76381) ^ [] : [model(179 ^ [_82654, _82656], _82654)]], 184 ^ _76381 : [(185 ^ _76381) ^ [_83084] : [model(_83084, _82654), -(model(_83084, _82656))]]], (211 ^ _76381) ^ [_84069, _84071] : [-(status(_84071, _84069, eth)), 214 ^ _76381 : [(215 ^ _76381) ^ [_84204] : [model(_84204, _84071)]], 218 ^ _76381 : [(219 ^ _76381) ^ [_84300] : [-(model(_84300, _84071))]], 223 ^ _76381 : [(224 ^ _76381) ^ [] : [-(model(220 ^ [_84069, _84071], _84071))], (226 ^ _76381) ^ [] : [model(220 ^ [_84069, _84071], _84069)]], 227 ^ _76381 : [(228 ^ _76381) ^ [] : [-(model(220 ^ [_84069, _84071], _84069))], (230 ^ _76381) ^ [] : [model(220 ^ [_84069, _84071], _84071)]]], (234 ^ _76381) ^ [_84778, _84780] : [status(_84780, _84778, eth), 238 ^ _76381 : [(239 ^ _76381) ^ [] : [-(model(237 ^ [_84778, _84780], _84780))], (242 ^ _76381) ^ [] : [model(240 ^ [_84778, _84780], _84780)], (244 ^ _76381) ^ [_85207] : [model(_85207, _84780), -(model(_85207, _84778))], (250 ^ _76381) ^ [_85379] : [model(_85379, _84778), -(model(_85379, _84780))]]], (267 ^ _76381) ^ [_85964, _85966] : [status(_85966, _85964, tau), 270 ^ _76381 : [(271 ^ _76381) ^ [_86108] : [-(model(_86108, _85966))], (273 ^ _76381) ^ [_86156] : [-(model(_86156, _85964))]]], (256 ^ _76381) ^ [_85641, _85643] : [-(status(_85643, _85641, tau)), model(257 ^ [_85641, _85643], _85643), model(257 ^ [_85641, _85643], _85641)], (290 ^ _76381) ^ [_86751, _86753] : [status(_86753, _86751, wtc), 294 ^ _76381 : [(295 ^ _76381) ^ [] : [-(model(293 ^ [_86751, _86753], _86753))], (298 ^ _76381) ^ [] : [model(296 ^ [_86751, _86753], _86753)], (300 ^ _76381) ^ [_87130] : [-(model(_87130, _86751))]]], (275 ^ _76381) ^ [_86305, _86307] : [-(status(_86307, _86305, wtc)), 278 ^ _76381 : [(279 ^ _76381) ^ [_86434] : [model(_86434, _86307)]], 282 ^ _76381 : [(283 ^ _76381) ^ [_86530] : [-(model(_86530, _86307))]], model(284 ^ [_86305, _86307], _86305)], (327 ^ _76381) ^ [_88061, _88063] : [status(_88063, _88061, wth), 331 ^ _76381 : [(332 ^ _76381) ^ [] : [-(model(330 ^ [_88061, _88063], _88063))], (341 ^ _76381) ^ [] : [-(model(339 ^ [_88061, _88063], _88061))], (343 ^ _76381) ^ [] : [model(339 ^ [_88061, _88063], _88063)], (346 ^ _76381) ^ [] : [model(344 ^ [_88061, _88063], _88061)], (334 ^ _76381) ^ [_88381] : [model(_88381, _88063), -(model(_88381, _88061))]]], (302 ^ _76381) ^ [_87281, _87283] : [-(status(_87283, _87281, wth)), 305 ^ _76381 : [(306 ^ _76381) ^ [_87435] : [model(_87435, _87283)]], 310 ^ _76381 : [(311 ^ _76381) ^ [] : [-(model(309 ^ [_87281, _87283], _87283))], (313 ^ _76381) ^ [] : [model(309 ^ [_87281, _87283], _87281)]], 322 ^ _76381 : [(323 ^ _76381) ^ [_87931] : [-(model(_87931, _87281))]], 316 ^ _76381 : [(317 ^ _76381) ^ [_87758] : [model(_87758, _87281), -(model(_87758, _87283))]]], (348 ^ _76381) ^ [_88948, _88950] : [-(model(349 ^ [_88948, _88950], _88950)), -(status(_88950, _88948, cax))], (355 ^ _76381) ^ [_89172, _89174] : [status(_89174, _89172, cax), 358 ^ _76381 : [(359 ^ _76381) ^ [_89291] : [model(_89291, _89174)]]], (372 ^ _76381) ^ [_89773, _89775] : [status(_89775, _89773, sca), 375 ^ _76381 : [(376 ^ _76381) ^ [_89923] : [model(_89923, _89775)], (379 ^ _76381) ^ [] : [-(model(377 ^ [_89773, _89775], _89773))]]], (361 ^ _76381) ^ [_89438, _89440] : [-(status(_89440, _89438, sca)), -(model(364 ^ [_89438, _89440], _89440)), 367 ^ _76381 : [(368 ^ _76381) ^ [_89654] : [model(_89654, _89438)]]], (393 ^ _76381) ^ [_90540, _90542] : [status(_90542, _90540, tca), 396 ^ _76381 : [(397 ^ _76381) ^ [_90690] : [model(_90690, _90542)], (399 ^ _76381) ^ [_90752] : [-(model(_90752, _90540))]]], (381 ^ _76381) ^ [_90170, _90172] : [-(status(_90172, _90170, tca)), -(model(384 ^ [_90170, _90172], _90172)), model(387 ^ [_90170, _90172], _90170)], (416 ^ _76381) ^ [_91350, _91352] : [status(_91352, _91350, wca), 419 ^ _76381 : [(420 ^ _76381) ^ [_91513] : [model(_91513, _91352)], (423 ^ _76381) ^ [] : [-(model(421 ^ [_91350, _91352], _91350))], (426 ^ _76381) ^ [] : [model(424 ^ [_91350, _91352], _91350)]]], (401 ^ _76381) ^ [_90901, _90903] : [-(status(_90903, _90901, wca)), -(model(404 ^ [_90901, _90903], _90903)), 409 ^ _76381 : [(410 ^ _76381) ^ [_91164] : [model(_91164, _90901)]], 411 ^ _76381 : [(412 ^ _76381) ^ [_91226] : [-(model(_91226, _90901))]]], (438 ^ _76381) ^ [_92203, _92205] : [status(_92205, _92203, csa), 442 ^ _76381 : [(443 ^ _76381) ^ [] : [-(model(441 ^ [_92203, _92205], _92205))], (445 ^ _76381) ^ [] : [-(model(441 ^ [_92203, _92205], not _92203))]]], (428 ^ _76381) ^ [_91881, _91883] : [-(status(_91883, _91881, csa)), 429 ^ _76381 : [(430 ^ _76381) ^ [_91976] : [model(_91976, _91883), model(_91976, not _91881)]]], (459 ^ _76381) ^ [_92970, _92972] : [status(_92972, _92970, uns), 462 ^ _76381 : [(463 ^ _76381) ^ [_93121] : [-(model(_93121, _92972))], (465 ^ _76381) ^ [_93183] : [-(model(_93183, not _92970))]]], (447 ^ _76381) ^ [_92597, _92599] : [-(status(_92599, _92597, uns)), model(450 ^ [_92597, _92599], _92599), model(453 ^ [_92597, _92599], not _92597)], (485 ^ _76381) ^ [_93877, _93879] : [status(_93879, _93877, noc), 489 ^ _76381 : [(490 ^ _76381) ^ [] : [-(model(488 ^ [_93877, _93879], _93879))], (492 ^ _76381) ^ [] : [-(model(488 ^ [_93877, _93879], _93877))], (495 ^ _76381) ^ [] : [-(model(493 ^ [_93877, _93879], _93879))], (497 ^ _76381) ^ [] : [-(model(493 ^ [_93877, _93879], not _93877))]]], (467 ^ _76381) ^ [_93314, _93316] : [-(status(_93316, _93314, noc)), 470 ^ _76381 : [(471 ^ _76381) ^ [_93460] : [model(_93460, _93316), model(_93460, _93314)]], 476 ^ _76381 : [(477 ^ _76381) ^ [_93645] : [model(_93645, _93316), model(_93645, not _93314)]]]], input).
% 0.97/1.37 ncf('1',plain,[615 : model(72 ^ [not not 635 ^ [], not 635 ^ []], not 635 ^ []), 619 : model(72 ^ [not not 635 ^ [], not 635 ^ []], 635 ^ [])],start(611 ^ 0,bind([[_99151, _99153], [635 ^ [], 72 ^ [not not 635 ^ [], not 635 ^ []]]]))).
% 0.97/1.37 ncf('1.1',plain,[-(model(72 ^ [not not 635 ^ [], not 635 ^ []], not 635 ^ [])), 617 : -(model(72 ^ [not not 635 ^ [], not 635 ^ []], not not 635 ^ []))],extension(611 ^ 3,bind([[_99151, _99153], [not 635 ^ [], 72 ^ [not not 635 ^ [], not 635 ^ []]]]))).
% 0.97/1.37 ncf('1.1.1',plain,[model(72 ^ [not not 635 ^ [], not 635 ^ []], not not 635 ^ []), -(status(not 635 ^ [], not not 635 ^ [], esa)), 54 : model(639 ^ [], not 635 ^ [])],extension(42 ^ 6,bind([[_78007, _78009, _78250, _78431], [not not 635 ^ [], not 635 ^ [], 72 ^ [not not 635 ^ [], not 635 ^ []], 639 ^ []]]))).
% 0.97/1.37 ncf('1.1.1.1',plain,[status(not 635 ^ [], not not 635 ^ [], esa), 71 : model(72 ^ [not not 635 ^ [], not 635 ^ []], not not 635 ^ []), 71 : -(model(72 ^ [not not 635 ^ [], not 635 ^ []], not 635 ^ []))],extension(58 ^ 7,bind([[_78553, _78555, _78942], [not not 635 ^ [], not 635 ^ [], 72 ^ [not not 635 ^ [], not 635 ^ []]]]))).
% 0.97/1.37 ncf('1.1.1.1.1',plain,[-(model(72 ^ [not not 635 ^ [], not 635 ^ []], not not 635 ^ []))],reduction('1.1')).
% 0.97/1.37 ncf('1.1.1.1.2',plain,[model(72 ^ [not not 635 ^ [], not 635 ^ []], not 635 ^ [])],reduction('1')).
% 0.97/1.37 ncf('1.1.1.2',plain,[-(model(639 ^ [], not 635 ^ [])), 613 : -(model(639 ^ [], 635 ^ []))],extension(611 ^ 9,bind([[_99151, _99153], [635 ^ [], 639 ^ []]]))).
% 0.97/1.37 ncf('1.1.1.2.1',plain,[model(639 ^ [], 635 ^ [])],extension(641 ^ 12)).
% 0.97/1.37 ncf('1.2',plain,[-(model(72 ^ [not not 635 ^ [], not 635 ^ []], 635 ^ [])), 108 : model(72 ^ [not not 635 ^ [], not 635 ^ []], not 635 ^ []), 108 : status(not 635 ^ [], 635 ^ [], thm)],extension(104 ^ 3,bind([[_80207, _80209, _80346], [635 ^ [], not 635 ^ [], 72 ^ [not not 635 ^ [], not 635 ^ []]]]))).
% 0.97/1.37 ncf('1.2.1',plain,[-(model(72 ^ [not not 635 ^ [], not 635 ^ []], not 635 ^ []))],extension(617 ^ 6)).
% 0.97/1.37 ncf('1.2.2',plain,[-(status(not 635 ^ [], 635 ^ [], thm)), 541 : status(not 635 ^ [], 635 ^ [], sap), 541 : -(nota(sap, thm))],extension(539 ^ 4,bind([[_96283, _96285, _96398, _96400], [thm, sap, 635 ^ [], not 635 ^ []]]))).
% 0.97/1.37 ncf('1.2.2.1',plain,[-(status(not 635 ^ [], 635 ^ [], sap)), 27 : model(636 ^ [], 635 ^ [])],extension(22 ^ 7,bind([[_77279, _77281, _77479], [635 ^ [], not 635 ^ [], 636 ^ []]]))).
% 0.97/1.37 ncf('1.2.2.1.1',plain,[-(model(636 ^ [], 635 ^ []))],extension(638 ^ 10)).
% 0.97/1.37 ncf('1.2.2.2',plain,[nota(sap, thm)],extension(689 ^ 5)).
% 0.97/1.37 %-----------------------------------------------------
% 0.97/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------