%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS251+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n006.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:32 EDT 2023
% Result : Theorem 196.58s 190.47s
% Output : Proof 196.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : KRS251+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n006.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:02:06 EDT 2023
% 0.12/0.33 % CPUTime :
% 196.58/190.47
% 196.58/190.47 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 196.58/190.47 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 196.58/190.47 %-----------------------------------------------------
% 196.58/190.47 ncf(matrix, plain, [(689 ^ _112221) ^ [] : [xora(csa, thm)], !, (152 ^ _86652) ^ [_92177, _92179] : [-(status(_92179, _92177, tac)), 155 ^ _86652 : [(156 ^ _86652) ^ [_92293] : [model(_92293, _92179)]], model(157 ^ [_92177, _92179], _92177)], (569 ^ _86652) ^ [_107783, _107785] : [nevera(_107785, _107783), 572 ^ _86652 : [(573 ^ _86652) ^ [_107943, _107945] : [status(_107945, _107943, _107785), status(_107945, _107943, _107783)]]], (641 ^ _86652) ^ [] : [model(639 ^ [], 635 ^ [])], (361 ^ _86652) ^ [_99689, _99691] : [-(status(_99691, _99689, sca)), -(model(364 ^ [_99689, _99691], _99691)), 367 ^ _86652 : [(368 ^ _86652) ^ [_99905] : [model(_99905, _99689)]]], (58 ^ _86652) ^ [_88804, _88806] : [status(_88806, _88804, esa), 61 ^ _86652 : [(69 ^ _86652) ^ [] : [70 ^ _86652 : [(71 ^ _86652) ^ [_89193] : [model(_89193, _88804)]], -(model(72 ^ [_88804, _88806], _88806))], (62 ^ _86652) ^ [] : [63 ^ _86652 : [(64 ^ _86652) ^ [_88995] : [model(_88995, _88806)]], -(model(65 ^ [_88804, _88806], _88804))]]], (193 ^ _86652) ^ [_93571, _93573] : [status(_93573, _93571, wec), 197 ^ _86652 : [(200 ^ _86652) ^ [_93878] : [model(_93878, _93573), -(model(_93878, _93571))], (198 ^ _86652) ^ [] : [-(model(196 ^ [_93571, _93573], _93573))], (209 ^ _86652) ^ [] : [model(205 ^ [_93571, _93573], _93573)], (207 ^ _86652) ^ [] : [-(model(205 ^ [_93571, _93573], _93571))]]], (634 ^ _86652) ^ [_110197] : [-(model(_110197, 632 ^ []))], (114 ^ _86652) ^ [_90853, _90855] : [-(status(_90855, _90853, eqv)), 117 ^ _86652 : [(118 ^ _86652) ^ [_90975] : [model(_90975, _90855)]], 122 ^ _86652 : [(125 ^ _86652) ^ [] : [model(119 ^ [_90853, _90855], _90853)], (123 ^ _86652) ^ [] : [-(model(119 ^ [_90853, _90855], _90855))]], 126 ^ _86652 : [(129 ^ _86652) ^ [] : [model(119 ^ [_90853, _90855], _90855)], (127 ^ _86652) ^ [] : [-(model(119 ^ [_90853, _90855], _90853))]]], (597 ^ _86652) ^ [_108826, _108828] : [xora(_108828, _108826), 600 ^ _86652 : [(601 ^ _86652) ^ [_108995, _108997] : [602 ^ _86652 : [(605 ^ _86652) ^ [] : [status(_108997, _108995, _108826)], (603 ^ _86652) ^ [] : [-(status(_108997, _108995, _108828))]], 606 ^ _86652 : [(609 ^ _86652) ^ [] : [status(_108997, _108995, _108828)], (607 ^ _86652) ^ [] : [-(status(_108997, _108995, _108826))]]]]], (381 ^ _86652) ^ [_100421, _100423] : [-(status(_100423, _100421, tca)), -(model(384 ^ [_100421, _100423], _100423)), model(387 ^ [_100421, _100423], _100421)], (677 ^ _86652) ^ [] : [model(675 ^ [], 660 ^ [])], (428 ^ _86652) ^ [_102132, _102134] : [-(status(_102134, _102132, csa)), 429 ^ _86652 : [(430 ^ _86652) ^ [_102227] : [model(_102227, _102134), model(_102227, not _102132)]]], (86 ^ _86652) ^ [_89761, _89763] : [status(_89763, _89761, sat), 90 ^ _86652 : [(93 ^ _86652) ^ [] : [-(model(89 ^ [_89761, _89763], _89761))], (91 ^ _86652) ^ [] : [-(model(89 ^ [_89761, _89763], _89763))]]], (163 ^ _86652) ^ [_92509, _92511] : [status(_92511, _92509, tac), 167 ^ _86652 : [(170 ^ _86652) ^ [_92756] : [-(model(_92756, _92509))], (168 ^ _86652) ^ [] : [-(model(166 ^ [_92509, _92511], _92511))]]], (644 ^ _86652) ^ [_110556] : [model(_110556, 642 ^ [])], (649 ^ _86652) ^ [] : [-(model(647 ^ [], 645 ^ []))], (211 ^ _86652) ^ [_94320, _94322] : [-(status(_94322, _94320, eth)), 214 ^ _86652 : [(215 ^ _86652) ^ [_94455] : [model(_94455, _94322)]], 218 ^ _86652 : [(219 ^ _86652) ^ [_94551] : [-(model(_94551, _94322))]], 223 ^ _86652 : [(226 ^ _86652) ^ [] : [model(220 ^ [_94320, _94322], _94320)], (224 ^ _86652) ^ [] : [-(model(220 ^ [_94320, _94322], _94322))]], 227 ^ _86652 : [(230 ^ _86652) ^ [] : [model(220 ^ [_94320, _94322], _94322)], (228 ^ _86652) ^ [] : [-(model(220 ^ [_94320, _94322], _94320))]]], (302 ^ _86652) ^ [_97532, _97534] : [-(status(_97534, _97532, wth)), 305 ^ _86652 : [(306 ^ _86652) ^ [_97686] : [model(_97686, _97534)]], 310 ^ _86652 : [(313 ^ _86652) ^ [] : [model(309 ^ [_97532, _97534], _97532)], (311 ^ _86652) ^ [] : [-(model(309 ^ [_97532, _97534], _97534))]], 322 ^ _86652 : [(323 ^ _86652) ^ [_98182] : [-(model(_98182, _97532))]], 316 ^ _86652 : [(317 ^ _86652) ^ [_98009] : [model(_98009, _97532), -(model(_98009, _97534))]]], (485 ^ _86652) ^ [_104128, _104130] : [status(_104130, _104128, noc), 489 ^ _86652 : [(497 ^ _86652) ^ [] : [-(model(493 ^ [_104128, _104130], not _104128))], (490 ^ _86652) ^ [] : [-(model(488 ^ [_104128, _104130], _104130))], (495 ^ _86652) ^ [] : [-(model(493 ^ [_104128, _104130], _104130))], (492 ^ _86652) ^ [] : [-(model(488 ^ [_104128, _104130], _104128))]]], (133 ^ _86652) ^ [_91448, _91450] : [status(_91450, _91448, eqv), 137 ^ _86652 : [(146 ^ _86652) ^ [_91917] : [model(_91917, _91448), -(model(_91917, _91450))], (140 ^ _86652) ^ [_91745] : [model(_91745, _91450), -(model(_91745, _91448))], (138 ^ _86652) ^ [] : [-(model(136 ^ [_91448, _91450], _91450))]]], (42 ^ _86652) ^ [_88258, _88260] : [-(status(_88260, _88258, esa)), 46 ^ _86652 : [(49 ^ _86652) ^ [_88501] : [model(_88501, _88258)], (47 ^ _86652) ^ [] : [-(model(45 ^ [_88258, _88260], _88260))]], 51 ^ _86652 : [(54 ^ _86652) ^ [_88682] : [model(_88682, _88260)], (52 ^ _86652) ^ [] : [-(model(50 ^ [_88258, _88260], _88258))]]], (611 ^ _86652) ^ [_109402, _109404] : [612 ^ _86652 : [(615 ^ _86652) ^ [] : [model(_109404, not _109402)], (613 ^ _86652) ^ [] : [-(model(_109404, _109402))]], 616 ^ _86652 : [(619 ^ _86652) ^ [] : [model(_109404, _109402)], (617 ^ _86652) ^ [] : [-(model(_109404, not _109402))]]], (665 ^ _86652) ^ [_111409] : [model(_111409, 659 ^ []), -(model(_111409, 660 ^ []))], (438 ^ _86652) ^ [_102454, _102456] : [status(_102456, _102454, csa), 442 ^ _86652 : [(445 ^ _86652) ^ [] : [-(model(441 ^ [_102454, _102456], not _102454))], (443 ^ _86652) ^ [] : [-(model(441 ^ [_102454, _102456], _102456))]]], (267 ^ _86652) ^ [_96215, _96217] : [status(_96217, _96215, tau), 270 ^ _86652 : [(273 ^ _86652) ^ [_96407] : [-(model(_96407, _96215))], (271 ^ _86652) ^ [_96359] : [-(model(_96359, _96217))]]], (416 ^ _86652) ^ [_101601, _101603] : [status(_101603, _101601, wca), 419 ^ _86652 : [(426 ^ _86652) ^ [] : [model(424 ^ [_101601, _101603], _101601)], (423 ^ _86652) ^ [] : [-(model(421 ^ [_101601, _101603], _101601))], (420 ^ _86652) ^ [_101764] : [model(_101764, _101603)]]], (172 ^ _86652) ^ [_92905, _92907] : [-(status(_92907, _92905, wec)), 175 ^ _86652 : [(176 ^ _86652) ^ [_93046] : [model(_93046, _92907)]], 180 ^ _86652 : [(183 ^ _86652) ^ [] : [model(179 ^ [_92905, _92907], _92905)], (181 ^ _86652) ^ [] : [-(model(179 ^ [_92905, _92907], _92907))]], 184 ^ _86652 : [(185 ^ _86652) ^ [_93335] : [model(_93335, _92905), -(model(_93335, _92907))]]], (638 ^ _86652) ^ [] : [-(model(636 ^ [], 635 ^ []))], (290 ^ _86652) ^ [_97002, _97004] : [status(_97004, _97002, wtc), 294 ^ _86652 : [(300 ^ _86652) ^ [_97381] : [-(model(_97381, _97002))], (298 ^ _86652) ^ [] : [model(296 ^ [_97002, _97004], _97004)], (295 ^ _86652) ^ [] : [-(model(293 ^ [_97002, _97004], _97004))]]], (559 ^ _86652) ^ [_107372, _107374] : [562 ^ _86652 : [(565 ^ _86652) ^ [] : [-(status(560 ^ [_107372, _107374], 561 ^ [_107372, _107374], _107372))], (563 ^ _86652) ^ [] : [-(status(560 ^ [_107372, _107374], 561 ^ [_107372, _107374], _107374))]], -(nevera(_107374, _107372))], (651 ^ _86652) ^ [] : [-(model(647 ^ [], 646 ^ []))], (654 ^ _86652) ^ [] : [model(652 ^ [], 645 ^ []), model(652 ^ [], 646 ^ [])], (372 ^ _86652) ^ [_100024, _100026] : [status(_100026, _100024, sca), 375 ^ _86652 : [(379 ^ _86652) ^ [] : [-(model(377 ^ [_100024, _100026], _100024))], (376 ^ _86652) ^ [_100174] : [model(_100174, _100026)]]], (95 ^ _86652) ^ [_90149, _90151] : [97 ^ _86652 : [(100 ^ _86652) ^ [] : [model(96 ^ [_90149, _90151], _90149)], (98 ^ _86652) ^ [] : [-(model(96 ^ [_90149, _90151], _90151))]], -(status(_90151, _90149, thm))], (355 ^ _86652) ^ [_99423, _99425] : [status(_99425, _99423, cax), 358 ^ _86652 : [(359 ^ _86652) ^ [_99542] : [model(_99542, _99425)]]], (348 ^ _86652) ^ [_99199, _99201] : [-(model(349 ^ [_99199, _99201], _99201)), -(status(_99201, _99199, cax))], (682 ^ _86652) ^ [] : [-(model(678 ^ [], 679 ^ []))], (621 ^ _86652) ^ [_109798, _109800] : [model(_109800, _109798), model(_109800, not _109798)], (459 ^ _86652) ^ [_103221, _103223] : [status(_103223, _103221, uns), 462 ^ _86652 : [(465 ^ _86652) ^ [_103434] : [-(model(_103434, not _103221))], (463 ^ _86652) ^ [_103372] : [-(model(_103372, _103223))]]], (11 ^ _86652) ^ [_87115, _87117] : [status(_87117, _87115, unp), -(model(16 ^ [_87115, _87117], _87117)), 19 ^ _86652 : [(20 ^ _86652) ^ [_87379] : [model(_87379, _87115)]]], (684 ^ _86652) ^ [] : [model(678 ^ [], 680 ^ [])], (529 ^ _86652) ^ [_106110, _106112] : [isa(_106112, _106110), 532 ^ _86652 : [(533 ^ _86652) ^ [_106268, _106270] : [status(_106270, _106268, _106112), -(status(_106270, _106268, _106110))]]], (509 ^ _86652) ^ [_105223, _105225] : [mighta(_105225, _105223), 514 ^ _86652 : [(517 ^ _86652) ^ [] : [-(status(512 ^ [_105223, _105225], 513 ^ [_105223, _105225], _105223))], (515 ^ _86652) ^ [] : [-(status(512 ^ [_105223, _105225], 513 ^ [_105223, _105225], _105225))]]], (627 ^ _86652) ^ [_109965, _109967] : [-(model(_109967, not _109965)), -(model(_109967, _109965))], (104 ^ _86652) ^ [_90458, _90460] : [status(_90460, _90458, thm), 107 ^ _86652 : [(108 ^ _86652) ^ [_90597] : [model(_90597, _90460), -(model(_90597, _90458))]]], (22 ^ _86652) ^ [_87530, _87532] : [24 ^ _86652 : [(27 ^ _86652) ^ [_87730] : [model(_87730, _87530)], (25 ^ _86652) ^ [] : [-(model(23 ^ [_87530, _87532], _87532))]], -(status(_87532, _87530, sap))], (327 ^ _86652) ^ [_98312, _98314] : [status(_98314, _98312, wth), 331 ^ _86652 : [(341 ^ _86652) ^ [] : [-(model(339 ^ [_98312, _98314], _98312))], (343 ^ _86652) ^ [] : [model(339 ^ [_98312, _98314], _98314)], (346 ^ _86652) ^ [] : [model(344 ^ [_98312, _98314], _98312)], (334 ^ _86652) ^ [_98632] : [model(_98632, _98314), -(model(_98632, _98312))], (332 ^ _86652) ^ [] : [-(model(330 ^ [_98312, _98314], _98314))]]], (234 ^ _86652) ^ [_95029, _95031] : [status(_95031, _95029, eth), 238 ^ _86652 : [(250 ^ _86652) ^ [_95630] : [model(_95630, _95029), -(model(_95630, _95031))], (239 ^ _86652) ^ [] : [-(model(237 ^ [_95029, _95031], _95031))], (244 ^ _86652) ^ [_95458] : [model(_95458, _95031), -(model(_95458, _95029))], (242 ^ _86652) ^ [] : [model(240 ^ [_95029, _95031], _95031)]]], (256 ^ _86652) ^ [_95892, _95894] : [-(status(_95894, _95892, tau)), model(257 ^ [_95892, _95894], _95894), model(257 ^ [_95892, _95894], _95892)], (401 ^ _86652) ^ [_101152, _101154] : [-(status(_101154, _101152, wca)), -(model(404 ^ [_101152, _101154], _101154)), 409 ^ _86652 : [(410 ^ _86652) ^ [_101415] : [model(_101415, _101152)]], 411 ^ _86652 : [(412 ^ _86652) ^ [_101477] : [-(model(_101477, _101152))]]], (31 ^ _86652) ^ [_87847, _87849] : [status(_87849, _87847, sap), 36 ^ _86652 : [(37 ^ _86652) ^ [_88009] : [model(_88009, _87849)]], -(model(38 ^ [_87847, _87849], _87847))], (467 ^ _86652) ^ [_103565, _103567] : [-(status(_103567, _103565, noc)), 470 ^ _86652 : [(471 ^ _86652) ^ [_103711] : [model(_103711, _103567), model(_103711, _103565)]], 476 ^ _86652 : [(477 ^ _86652) ^ [_103896] : [model(_103896, _103567), model(_103896, not _103565)]]], (499 ^ _86652) ^ [_104878, _104880] : [-(mighta(_104880, _104878)), 500 ^ _86652 : [(501 ^ _86652) ^ [_104991, _104993] : [status(_104993, _104991, _104880), status(_104993, _104991, _104878)]]], (275 ^ _86652) ^ [_96556, _96558] : [-(status(_96558, _96556, wtc)), 278 ^ _86652 : [(279 ^ _86652) ^ [_96685] : [model(_96685, _96558)]], 282 ^ _86652 : [(283 ^ _86652) ^ [_96781] : [-(model(_96781, _96558))]], model(284 ^ [_96556, _96558], _96556)], (539 ^ _86652) ^ [_106534, _106536] : [-(nota(_106536, _106534)), 540 ^ _86652 : [(541 ^ _86652) ^ [_106649, _106651] : [status(_106651, _106649, _106536), -(status(_106651, _106649, _106534))]]], (579 ^ _86652) ^ [_108210, _108212] : [-(xora(_108212, _108210)), 582 ^ _86652 : [(589 ^ _86652) ^ [] : [status(580 ^ [_108210, _108212], 581 ^ [_108210, _108212], _108210), -(status(580 ^ [_108210, _108212], 581 ^ [_108210, _108212], _108212))], (583 ^ _86652) ^ [] : [status(580 ^ [_108210, _108212], 581 ^ [_108210, _108212], _108212), -(status(580 ^ [_108210, _108212], 581 ^ [_108210, _108212], _108210))]]], (672 ^ _86652) ^ [] : [model(670 ^ [], 659 ^ [])], (76 ^ _86652) ^ [_89445, _89447] : [-(status(_89447, _89445, sat)), 77 ^ _86652 : [(78 ^ _86652) ^ [_89538] : [model(_89538, _89447), model(_89538, _89445)]]], (674 ^ _86652) ^ [] : [-(model(670 ^ [], 660 ^ []))], (447 ^ _86652) ^ [_102848, _102850] : [-(status(_102850, _102848, uns)), model(450 ^ [_102848, _102850], _102850), model(453 ^ [_102848, _102850], not _102848)], (687 ^ _86652) ^ [] : [-(model(685 ^ [], 680 ^ []))], (519 ^ _86652) ^ [_105706, _105708] : [522 ^ _86652 : [(525 ^ _86652) ^ [] : [status(520 ^ [_105706, _105708], 521 ^ [_105706, _105708], _105706)], (523 ^ _86652) ^ [] : [-(status(520 ^ [_105706, _105708], 521 ^ [_105706, _105708], _105708))]], -(isa(_105708, _105706))], (2 ^ _86652) ^ [_86794, _86796] : [3 ^ _86652 : [(7 ^ _86652) ^ [] : [-(model(5 ^ [_86794, _86796], _86794))], (4 ^ _86652) ^ [_86900] : [model(_86900, _86796)]], -(status(_86796, _86794, unp))], (549 ^ _86652) ^ [_106884, _106886] : [nota(_106886, _106884), 554 ^ _86652 : [(557 ^ _86652) ^ [] : [status(552 ^ [_106884, _106886], 553 ^ [_106884, _106886], _106884)], (555 ^ _86652) ^ [] : [-(status(552 ^ [_106884, _106886], 553 ^ [_106884, _106886], _106886))]]], (393 ^ _86652) ^ [_100791, _100793] : [status(_100793, _100791, tca), 396 ^ _86652 : [(399 ^ _86652) ^ [_101003] : [-(model(_101003, _100791))], (397 ^ _86652) ^ [_100941] : [model(_100941, _100793)]]], (663 ^ _86652) ^ [] : [-(model(661 ^ [], 659 ^ []))]], input).
% 196.58/190.47 ncf('1',plain,[xora(csa, thm)],start(689 ^ 0)).
% 196.58/190.47 ncf('1.1',plain,[-(xora(csa, thm)), 583 : status(580 ^ [thm, csa], 581 ^ [thm, csa], csa), 583 : -(status(580 ^ [thm, csa], 581 ^ [thm, csa], thm))],extension(579 ^ 1,bind([[_108210, _108212], [thm, csa]]))).
% 196.58/190.47 ncf('1.1.1',plain,[-(status(580 ^ [thm, csa], 581 ^ [thm, csa], csa)), 430 : model(96 ^ [581 ^ [thm, csa], 580 ^ [thm, csa]], 580 ^ [thm, csa]), 430 : model(96 ^ [581 ^ [thm, csa], 580 ^ [thm, csa]], not 581 ^ [thm, csa])],extension(428 ^ 4,bind([[_102132, _102134, _102227], [581 ^ [thm, csa], 580 ^ [thm, csa], 96 ^ [581 ^ [thm, csa], 580 ^ [thm, csa]]]]))).
% 196.58/190.47 ncf('1.1.1.1',plain,[-(model(96 ^ [581 ^ [thm, csa], 580 ^ [thm, csa]], 580 ^ [thm, csa])), -(status(580 ^ [thm, csa], 581 ^ [thm, csa], thm))],extension(95 ^ 7,bind([[_90149, _90151], [581 ^ [thm, csa], 580 ^ [thm, csa]]]))).
% 196.58/190.47 ncf('1.1.1.1.1',plain,[status(580 ^ [thm, csa], 581 ^ [thm, csa], thm), -(status(580 ^ [thm, csa], 581 ^ [thm, csa], csa))],extension(589 ^ 8)).
% 196.58/190.47 ncf('1.1.1.1.1.1',plain,[status(580 ^ [thm, csa], 581 ^ [thm, csa], csa)],reduction('1.1')).
% 196.58/190.47 ncf('1.1.1.2',plain,[-(model(96 ^ [581 ^ [thm, csa], 580 ^ [thm, csa]], not 581 ^ [thm, csa])), 613 : -(model(96 ^ [581 ^ [thm, csa], 580 ^ [thm, csa]], 581 ^ [thm, csa]))],extension(611 ^ 7,bind([[_109402, _109404], [581 ^ [thm, csa], 96 ^ [581 ^ [thm, csa], 580 ^ [thm, csa]]]]))).
% 196.58/190.47 ncf('1.1.1.2.1',plain,[model(96 ^ [581 ^ [thm, csa], 580 ^ [thm, csa]], 581 ^ [thm, csa]), -(status(580 ^ [thm, csa], 581 ^ [thm, csa], thm))],extension(95 ^ 10,bind([[_90149, _90151], [581 ^ [thm, csa], 580 ^ [thm, csa]]]))).
% 196.58/190.47 ncf('1.1.1.2.1.1',plain,[status(580 ^ [thm, csa], 581 ^ [thm, csa], thm), -(status(580 ^ [thm, csa], 581 ^ [thm, csa], csa))],extension(589 ^ 11)).
% 196.58/190.47 ncf('1.1.1.2.1.1.1',plain,[status(580 ^ [thm, csa], 581 ^ [thm, csa], csa)],reduction('1.1')).
% 196.58/190.47 ncf('1.1.2',plain,[status(580 ^ [thm, csa], 581 ^ [thm, csa], thm), 108 : model(441 ^ [581 ^ [thm, csa], 580 ^ [thm, csa]], 580 ^ [thm, csa]), 108 : -(model(441 ^ [581 ^ [thm, csa], 580 ^ [thm, csa]], 581 ^ [thm, csa]))],extension(104 ^ 4,bind([[_90458, _90460, _90597], [581 ^ [thm, csa], 580 ^ [thm, csa], 441 ^ [581 ^ [thm, csa], 580 ^ [thm, csa]]]]))).
% 196.58/190.47 ncf('1.1.2.1',plain,[-(model(441 ^ [581 ^ [thm, csa], 580 ^ [thm, csa]], 580 ^ [thm, csa])), status(580 ^ [thm, csa], 581 ^ [thm, csa], csa)],extension(438 ^ 7,bind([[_102454, _102456], [581 ^ [thm, csa], 580 ^ [thm, csa]]]))).
% 196.58/190.47 ncf('1.1.2.1.1',plain,[-(status(580 ^ [thm, csa], 581 ^ [thm, csa], csa)), status(580 ^ [thm, csa], 581 ^ [thm, csa], thm)],extension(589 ^ 8)).
% 196.58/190.47 ncf('1.1.2.1.1.1',plain,[-(status(580 ^ [thm, csa], 581 ^ [thm, csa], thm))],reduction('1.1')).
% 196.58/190.47 ncf('1.1.2.2',plain,[model(441 ^ [581 ^ [thm, csa], 580 ^ [thm, csa]], 581 ^ [thm, csa]), 615 : model(441 ^ [581 ^ [thm, csa], 580 ^ [thm, csa]], not 581 ^ [thm, csa])],extension(611 ^ 7,bind([[_109402, _109404], [581 ^ [thm, csa], 441 ^ [581 ^ [thm, csa], 580 ^ [thm, csa]]]]))).
% 196.58/190.47 ncf('1.1.2.2.1',plain,[-(model(441 ^ [581 ^ [thm, csa], 580 ^ [thm, csa]], not 581 ^ [thm, csa])), status(580 ^ [thm, csa], 581 ^ [thm, csa], csa)],extension(438 ^ 10,bind([[_102454, _102456], [581 ^ [thm, csa], 580 ^ [thm, csa]]]))).
% 196.58/190.47 ncf('1.1.2.2.1.1',plain,[-(status(580 ^ [thm, csa], 581 ^ [thm, csa], csa))],lemmata('[1].x')).
% 196.58/190.47 %-----------------------------------------------------
% 196.58/190.47 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------