%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS234+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n021.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:31 EDT 2023
% Result : Theorem 44.59s 43.92s
% Output : Proof 44.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.13 % Problem : KRS234+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.05/0.13 % Command : nanocop.sh %s %d
% 0.13/0.35 % Computer : n021.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 18 23:05:12 EDT 2023
% 0.13/0.35 % CPUTime :
% 44.59/43.92
% 44.59/43.92 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 44.59/43.92 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 44.59/43.92 %-----------------------------------------------------
% 44.59/43.92 ncf(matrix, plain, [(689 ^ _110516) ^ [] : [nevera(uns, thm)], !, (569 ^ _84947) ^ [_106078, _106080] : [nevera(_106080, _106078), 572 ^ _84947 : [(573 ^ _84947) ^ [_106238, _106240] : [status(_106240, _106238, _106080), status(_106240, _106238, _106078)]]], (355 ^ _84947) ^ [_97718, _97720] : [status(_97720, _97718, cax), 358 ^ _84947 : [(359 ^ _84947) ^ [_97837] : [model(_97837, _97720)]]], (372 ^ _84947) ^ [_98319, _98321] : [status(_98321, _98319, sca), 375 ^ _84947 : [(379 ^ _84947) ^ [] : [-(model(377 ^ [_98319, _98321], _98319))], (376 ^ _84947) ^ [_98469] : [model(_98469, _98321)]]], (428 ^ _84947) ^ [_100427, _100429] : [-(status(_100429, _100427, csa)), 429 ^ _84947 : [(430 ^ _84947) ^ [_100522] : [model(_100522, _100429), model(_100522, not _100427)]]], (275 ^ _84947) ^ [_94851, _94853] : [-(status(_94853, _94851, wtc)), 278 ^ _84947 : [(279 ^ _84947) ^ [_94980] : [model(_94980, _94853)]], 282 ^ _84947 : [(283 ^ _84947) ^ [_95076] : [-(model(_95076, _94853))]], model(284 ^ [_94851, _94853], _94851)], (649 ^ _84947) ^ [] : [-(model(647 ^ [], 645 ^ []))], (42 ^ _84947) ^ [_86553, _86555] : [-(status(_86555, _86553, esa)), 46 ^ _84947 : [(49 ^ _84947) ^ [_86796] : [model(_86796, _86553)], (47 ^ _84947) ^ [] : [-(model(45 ^ [_86553, _86555], _86555))]], 51 ^ _84947 : [(54 ^ _84947) ^ [_86977] : [model(_86977, _86555)], (52 ^ _84947) ^ [] : [-(model(50 ^ [_86553, _86555], _86553))]]], (31 ^ _84947) ^ [_86142, _86144] : [status(_86144, _86142, sap), 36 ^ _84947 : [(37 ^ _84947) ^ [_86304] : [model(_86304, _86144)]], -(model(38 ^ [_86142, _86144], _86142))], (234 ^ _84947) ^ [_93324, _93326] : [status(_93326, _93324, eth), 238 ^ _84947 : [(242 ^ _84947) ^ [] : [model(240 ^ [_93324, _93326], _93326)], (244 ^ _84947) ^ [_93753] : [model(_93753, _93326), -(model(_93753, _93324))], (250 ^ _84947) ^ [_93925] : [model(_93925, _93324), -(model(_93925, _93326))], (239 ^ _84947) ^ [] : [-(model(237 ^ [_93324, _93326], _93326))]]], (193 ^ _84947) ^ [_91866, _91868] : [status(_91868, _91866, wec), 197 ^ _84947 : [(207 ^ _84947) ^ [] : [-(model(205 ^ [_91866, _91868], _91866))], (209 ^ _84947) ^ [] : [model(205 ^ [_91866, _91868], _91868)], (200 ^ _84947) ^ [_92173] : [model(_92173, _91868), -(model(_92173, _91866))], (198 ^ _84947) ^ [] : [-(model(196 ^ [_91866, _91868], _91868))]]], (152 ^ _84947) ^ [_90472, _90474] : [-(status(_90474, _90472, tac)), 155 ^ _84947 : [(156 ^ _84947) ^ [_90588] : [model(_90588, _90474)]], model(157 ^ [_90472, _90474], _90472)], (348 ^ _84947) ^ [_97494, _97496] : [-(model(349 ^ [_97494, _97496], _97496)), -(status(_97496, _97494, cax))], (529 ^ _84947) ^ [_104405, _104407] : [isa(_104407, _104405), 532 ^ _84947 : [(533 ^ _84947) ^ [_104563, _104565] : [status(_104565, _104563, _104407), -(status(_104565, _104563, _104405))]]], (499 ^ _84947) ^ [_103173, _103175] : [-(mighta(_103175, _103173)), 500 ^ _84947 : [(501 ^ _84947) ^ [_103286, _103288] : [status(_103288, _103286, _103175), status(_103288, _103286, _103173)]]], (114 ^ _84947) ^ [_89148, _89150] : [-(status(_89150, _89148, eqv)), 117 ^ _84947 : [(118 ^ _84947) ^ [_89270] : [model(_89270, _89150)]], 122 ^ _84947 : [(125 ^ _84947) ^ [] : [model(119 ^ [_89148, _89150], _89148)], (123 ^ _84947) ^ [] : [-(model(119 ^ [_89148, _89150], _89150))]], 126 ^ _84947 : [(129 ^ _84947) ^ [] : [model(119 ^ [_89148, _89150], _89150)], (127 ^ _84947) ^ [] : [-(model(119 ^ [_89148, _89150], _89148))]]], (665 ^ _84947) ^ [_109704] : [model(_109704, 659 ^ []), -(model(_109704, 660 ^ []))], (634 ^ _84947) ^ [_108492] : [-(model(_108492, 632 ^ []))], (438 ^ _84947) ^ [_100749, _100751] : [status(_100751, _100749, csa), 442 ^ _84947 : [(445 ^ _84947) ^ [] : [-(model(441 ^ [_100749, _100751], not _100749))], (443 ^ _84947) ^ [] : [-(model(441 ^ [_100749, _100751], _100751))]]], (519 ^ _84947) ^ [_104001, _104003] : [522 ^ _84947 : [(525 ^ _84947) ^ [] : [status(520 ^ [_104001, _104003], 521 ^ [_104001, _104003], _104001)], (523 ^ _84947) ^ [] : [-(status(520 ^ [_104001, _104003], 521 ^ [_104001, _104003], _104003))]], -(isa(_104003, _104001))], (677 ^ _84947) ^ [] : [model(675 ^ [], 660 ^ [])], (627 ^ _84947) ^ [_108260, _108262] : [-(model(_108262, not _108260)), -(model(_108262, _108260))], (256 ^ _84947) ^ [_94187, _94189] : [-(status(_94189, _94187, tau)), model(257 ^ [_94187, _94189], _94189), model(257 ^ [_94187, _94189], _94187)], (76 ^ _84947) ^ [_87740, _87742] : [-(status(_87742, _87740, sat)), 77 ^ _84947 : [(78 ^ _84947) ^ [_87833] : [model(_87833, _87742), model(_87833, _87740)]]], (621 ^ _84947) ^ [_108093, _108095] : [model(_108095, _108093), model(_108095, not _108093)], (684 ^ _84947) ^ [] : [model(678 ^ [], 680 ^ [])], (133 ^ _84947) ^ [_89743, _89745] : [status(_89745, _89743, eqv), 137 ^ _84947 : [(146 ^ _84947) ^ [_90212] : [model(_90212, _89743), -(model(_90212, _89745))], (140 ^ _84947) ^ [_90040] : [model(_90040, _89745), -(model(_90040, _89743))], (138 ^ _84947) ^ [] : [-(model(136 ^ [_89743, _89745], _89745))]]], (22 ^ _84947) ^ [_85825, _85827] : [24 ^ _84947 : [(27 ^ _84947) ^ [_86025] : [model(_86025, _85825)], (25 ^ _84947) ^ [] : [-(model(23 ^ [_85825, _85827], _85827))]], -(status(_85827, _85825, sap))], (682 ^ _84947) ^ [] : [-(model(678 ^ [], 679 ^ []))], (467 ^ _84947) ^ [_101860, _101862] : [-(status(_101862, _101860, noc)), 470 ^ _84947 : [(471 ^ _84947) ^ [_102006] : [model(_102006, _101862), model(_102006, _101860)]], 476 ^ _84947 : [(477 ^ _84947) ^ [_102191] : [model(_102191, _101862), model(_102191, not _101860)]]], (644 ^ _84947) ^ [_108851] : [model(_108851, 642 ^ [])], (559 ^ _84947) ^ [_105667, _105669] : [562 ^ _84947 : [(565 ^ _84947) ^ [] : [-(status(560 ^ [_105667, _105669], 561 ^ [_105667, _105669], _105667))], (563 ^ _84947) ^ [] : [-(status(560 ^ [_105667, _105669], 561 ^ [_105667, _105669], _105669))]], -(nevera(_105669, _105667))], (687 ^ _84947) ^ [] : [-(model(685 ^ [], 680 ^ []))], (211 ^ _84947) ^ [_92615, _92617] : [-(status(_92617, _92615, eth)), 214 ^ _84947 : [(215 ^ _84947) ^ [_92750] : [model(_92750, _92617)]], 218 ^ _84947 : [(219 ^ _84947) ^ [_92846] : [-(model(_92846, _92617))]], 223 ^ _84947 : [(226 ^ _84947) ^ [] : [model(220 ^ [_92615, _92617], _92615)], (224 ^ _84947) ^ [] : [-(model(220 ^ [_92615, _92617], _92617))]], 227 ^ _84947 : [(230 ^ _84947) ^ [] : [model(220 ^ [_92615, _92617], _92617)], (228 ^ _84947) ^ [] : [-(model(220 ^ [_92615, _92617], _92615))]]], (381 ^ _84947) ^ [_98716, _98718] : [-(status(_98718, _98716, tca)), -(model(384 ^ [_98716, _98718], _98718)), model(387 ^ [_98716, _98718], _98716)], (459 ^ _84947) ^ [_101516, _101518] : [status(_101518, _101516, uns), 462 ^ _84947 : [(465 ^ _84947) ^ [_101729] : [-(model(_101729, not _101516))], (463 ^ _84947) ^ [_101667] : [-(model(_101667, _101518))]]], (579 ^ _84947) ^ [_106505, _106507] : [-(xora(_106507, _106505)), 582 ^ _84947 : [(589 ^ _84947) ^ [] : [status(580 ^ [_106505, _106507], 581 ^ [_106505, _106507], _106505), -(status(580 ^ [_106505, _106507], 581 ^ [_106505, _106507], _106507))], (583 ^ _84947) ^ [] : [status(580 ^ [_106505, _106507], 581 ^ [_106505, _106507], _106507), -(status(580 ^ [_106505, _106507], 581 ^ [_106505, _106507], _106505))]]], (416 ^ _84947) ^ [_99896, _99898] : [status(_99898, _99896, wca), 419 ^ _84947 : [(426 ^ _84947) ^ [] : [model(424 ^ [_99896, _99898], _99896)], (423 ^ _84947) ^ [] : [-(model(421 ^ [_99896, _99898], _99896))], (420 ^ _84947) ^ [_100059] : [model(_100059, _99898)]]], (401 ^ _84947) ^ [_99447, _99449] : [-(status(_99449, _99447, wca)), -(model(404 ^ [_99447, _99449], _99449)), 409 ^ _84947 : [(410 ^ _84947) ^ [_99710] : [model(_99710, _99447)]], 411 ^ _84947 : [(412 ^ _84947) ^ [_99772] : [-(model(_99772, _99447))]]], (638 ^ _84947) ^ [] : [-(model(636 ^ [], 635 ^ []))], (104 ^ _84947) ^ [_88753, _88755] : [status(_88755, _88753, thm), 107 ^ _84947 : [(108 ^ _84947) ^ [_88892] : [model(_88892, _88755), -(model(_88892, _88753))]]], (447 ^ _84947) ^ [_101143, _101145] : [-(status(_101145, _101143, uns)), model(450 ^ [_101143, _101145], _101145), model(453 ^ [_101143, _101145], not _101143)], (163 ^ _84947) ^ [_90804, _90806] : [status(_90806, _90804, tac), 167 ^ _84947 : [(170 ^ _84947) ^ [_91051] : [-(model(_91051, _90804))], (168 ^ _84947) ^ [] : [-(model(166 ^ [_90804, _90806], _90806))]]], (509 ^ _84947) ^ [_103518, _103520] : [mighta(_103520, _103518), 514 ^ _84947 : [(517 ^ _84947) ^ [] : [-(status(512 ^ [_103518, _103520], 513 ^ [_103518, _103520], _103518))], (515 ^ _84947) ^ [] : [-(status(512 ^ [_103518, _103520], 513 ^ [_103518, _103520], _103520))]]], (393 ^ _84947) ^ [_99086, _99088] : [status(_99088, _99086, tca), 396 ^ _84947 : [(399 ^ _84947) ^ [_99298] : [-(model(_99298, _99086))], (397 ^ _84947) ^ [_99236] : [model(_99236, _99088)]]], (549 ^ _84947) ^ [_105179, _105181] : [nota(_105181, _105179), 554 ^ _84947 : [(557 ^ _84947) ^ [] : [status(552 ^ [_105179, _105181], 553 ^ [_105179, _105181], _105179)], (555 ^ _84947) ^ [] : [-(status(552 ^ [_105179, _105181], 553 ^ [_105179, _105181], _105181))]]], (267 ^ _84947) ^ [_94510, _94512] : [status(_94512, _94510, tau), 270 ^ _84947 : [(273 ^ _84947) ^ [_94702] : [-(model(_94702, _94510))], (271 ^ _84947) ^ [_94654] : [-(model(_94654, _94512))]]], (663 ^ _84947) ^ [] : [-(model(661 ^ [], 659 ^ []))], (361 ^ _84947) ^ [_97984, _97986] : [-(status(_97986, _97984, sca)), -(model(364 ^ [_97984, _97986], _97986)), 367 ^ _84947 : [(368 ^ _84947) ^ [_98200] : [model(_98200, _97984)]]], (58 ^ _84947) ^ [_87099, _87101] : [status(_87101, _87099, esa), 61 ^ _84947 : [(69 ^ _84947) ^ [] : [70 ^ _84947 : [(71 ^ _84947) ^ [_87488] : [model(_87488, _87099)]], -(model(72 ^ [_87099, _87101], _87101))], (62 ^ _84947) ^ [] : [63 ^ _84947 : [(64 ^ _84947) ^ [_87290] : [model(_87290, _87101)]], -(model(65 ^ [_87099, _87101], _87099))]]], (485 ^ _84947) ^ [_102423, _102425] : [status(_102425, _102423, noc), 489 ^ _84947 : [(492 ^ _84947) ^ [] : [-(model(488 ^ [_102423, _102425], _102423))], (495 ^ _84947) ^ [] : [-(model(493 ^ [_102423, _102425], _102425))], (497 ^ _84947) ^ [] : [-(model(493 ^ [_102423, _102425], not _102423))], (490 ^ _84947) ^ [] : [-(model(488 ^ [_102423, _102425], _102425))]]], (95 ^ _84947) ^ [_88444, _88446] : [97 ^ _84947 : [(100 ^ _84947) ^ [] : [model(96 ^ [_88444, _88446], _88444)], (98 ^ _84947) ^ [] : [-(model(96 ^ [_88444, _88446], _88446))]], -(status(_88446, _88444, thm))], (290 ^ _84947) ^ [_95297, _95299] : [status(_95299, _95297, wtc), 294 ^ _84947 : [(300 ^ _84947) ^ [_95676] : [-(model(_95676, _95297))], (298 ^ _84947) ^ [] : [model(296 ^ [_95297, _95299], _95299)], (295 ^ _84947) ^ [] : [-(model(293 ^ [_95297, _95299], _95299))]]], (539 ^ _84947) ^ [_104829, _104831] : [-(nota(_104831, _104829)), 540 ^ _84947 : [(541 ^ _84947) ^ [_104944, _104946] : [status(_104946, _104944, _104831), -(status(_104946, _104944, _104829))]]], (327 ^ _84947) ^ [_96607, _96609] : [status(_96609, _96607, wth), 331 ^ _84947 : [(332 ^ _84947) ^ [] : [-(model(330 ^ [_96607, _96609], _96609))], (343 ^ _84947) ^ [] : [model(339 ^ [_96607, _96609], _96609)], (334 ^ _84947) ^ [_96927] : [model(_96927, _96609), -(model(_96927, _96607))], (346 ^ _84947) ^ [] : [model(344 ^ [_96607, _96609], _96607)], (341 ^ _84947) ^ [] : [-(model(339 ^ [_96607, _96609], _96607))]]], (674 ^ _84947) ^ [] : [-(model(670 ^ [], 660 ^ []))], (172 ^ _84947) ^ [_91200, _91202] : [-(status(_91202, _91200, wec)), 175 ^ _84947 : [(176 ^ _84947) ^ [_91341] : [model(_91341, _91202)]], 180 ^ _84947 : [(183 ^ _84947) ^ [] : [model(179 ^ [_91200, _91202], _91200)], (181 ^ _84947) ^ [] : [-(model(179 ^ [_91200, _91202], _91202))]], 184 ^ _84947 : [(185 ^ _84947) ^ [_91630] : [model(_91630, _91200), -(model(_91630, _91202))]]], (611 ^ _84947) ^ [_107697, _107699] : [612 ^ _84947 : [(615 ^ _84947) ^ [] : [model(_107699, not _107697)], (613 ^ _84947) ^ [] : [-(model(_107699, _107697))]], 616 ^ _84947 : [(619 ^ _84947) ^ [] : [model(_107699, _107697)], (617 ^ _84947) ^ [] : [-(model(_107699, not _107697))]]], (641 ^ _84947) ^ [] : [model(639 ^ [], 635 ^ [])], (672 ^ _84947) ^ [] : [model(670 ^ [], 659 ^ [])], (654 ^ _84947) ^ [] : [model(652 ^ [], 645 ^ []), model(652 ^ [], 646 ^ [])], (2 ^ _84947) ^ [_85089, _85091] : [3 ^ _84947 : [(7 ^ _84947) ^ [] : [-(model(5 ^ [_85089, _85091], _85089))], (4 ^ _84947) ^ [_85195] : [model(_85195, _85091)]], -(status(_85091, _85089, unp))], (86 ^ _84947) ^ [_88056, _88058] : [status(_88058, _88056, sat), 90 ^ _84947 : [(93 ^ _84947) ^ [] : [-(model(89 ^ [_88056, _88058], _88056))], (91 ^ _84947) ^ [] : [-(model(89 ^ [_88056, _88058], _88058))]]], (302 ^ _84947) ^ [_95827, _95829] : [-(status(_95829, _95827, wth)), 305 ^ _84947 : [(306 ^ _84947) ^ [_95981] : [model(_95981, _95829)]], 310 ^ _84947 : [(313 ^ _84947) ^ [] : [model(309 ^ [_95827, _95829], _95827)], (311 ^ _84947) ^ [] : [-(model(309 ^ [_95827, _95829], _95829))]], 322 ^ _84947 : [(323 ^ _84947) ^ [_96477] : [-(model(_96477, _95827))]], 316 ^ _84947 : [(317 ^ _84947) ^ [_96304] : [model(_96304, _95827), -(model(_96304, _95829))]]], (11 ^ _84947) ^ [_85410, _85412] : [status(_85412, _85410, unp), -(model(16 ^ [_85410, _85412], _85412)), 19 ^ _84947 : [(20 ^ _84947) ^ [_85674] : [model(_85674, _85410)]]], (651 ^ _84947) ^ [] : [-(model(647 ^ [], 646 ^ []))], (597 ^ _84947) ^ [_107121, _107123] : [xora(_107123, _107121), 600 ^ _84947 : [(601 ^ _84947) ^ [_107290, _107292] : [602 ^ _84947 : [(605 ^ _84947) ^ [] : [status(_107292, _107290, _107121)], (603 ^ _84947) ^ [] : [-(status(_107292, _107290, _107123))]], 606 ^ _84947 : [(609 ^ _84947) ^ [] : [status(_107292, _107290, _107123)], (607 ^ _84947) ^ [] : [-(status(_107292, _107290, _107121))]]]]]], input).
% 44.59/43.92 ncf('1',plain,[nevera(uns, thm)],start(689 ^ 0)).
% 44.59/43.92 ncf('1.1',plain,[-(nevera(uns, thm)), 565 : -(status(560 ^ [thm, uns], 561 ^ [thm, uns], thm))],extension(559 ^ 1,bind([[_105667, _105669], [thm, uns]]))).
% 44.59/43.92 ncf('1.1.1',plain,[status(560 ^ [thm, uns], 561 ^ [thm, uns], thm), 108 : model(72 ^ [561 ^ [thm, uns], not 561 ^ [thm, uns]], 560 ^ [thm, uns]), 108 : -(model(72 ^ [561 ^ [thm, uns], not 561 ^ [thm, uns]], 561 ^ [thm, uns]))],extension(104 ^ 4,bind([[_88753, _88755, _88892], [561 ^ [thm, uns], 560 ^ [thm, uns], 72 ^ [561 ^ [thm, uns], not 561 ^ [thm, uns]]]]))).
% 44.59/43.92 ncf('1.1.1.1',plain,[-(model(72 ^ [561 ^ [thm, uns], not 561 ^ [thm, uns]], 560 ^ [thm, uns])), -(status(560 ^ [thm, uns], 560 ^ [thm, uns], wtc)), 279 : model(_63799, 560 ^ [thm, uns]), 279 : model(284 ^ [560 ^ [thm, uns], 560 ^ [thm, uns]], 560 ^ [thm, uns])],extension(275 ^ 7,bind([[_94851, _94853, _95076, _94980], [560 ^ [thm, uns], 560 ^ [thm, uns], 72 ^ [561 ^ [thm, uns], not 561 ^ [thm, uns]], _63799]]))).
% 44.59/43.92 ncf('1.1.1.1.1',plain,[status(560 ^ [thm, uns], 560 ^ [thm, uns], wtc), 300 : -(model(72 ^ [561 ^ [thm, uns], not 561 ^ [thm, uns]], 560 ^ [thm, uns]))],extension(290 ^ 8,bind([[_95297, _95299, _95676], [560 ^ [thm, uns], 560 ^ [thm, uns], 72 ^ [561 ^ [thm, uns], not 561 ^ [thm, uns]]]]))).
% 44.59/43.92 ncf('1.1.1.1.1.1',plain,[model(72 ^ [561 ^ [thm, uns], not 561 ^ [thm, uns]], 560 ^ [thm, uns])],reduction('1.1.1')).
% 44.59/43.92 ncf('1.1.1.1.2',plain,[-(model(_63799, 560 ^ [thm, uns])), status(560 ^ [thm, uns], 561 ^ [thm, uns], uns)],extension(459 ^ 10,bind([[_101516, _101518, _101667], [561 ^ [thm, uns], 560 ^ [thm, uns], _63799]]))).
% 44.59/43.92 ncf('1.1.1.1.2.1',plain,[-(status(560 ^ [thm, uns], 561 ^ [thm, uns], uns))],extension(563 ^ 11)).
% 44.59/43.92 ncf('1.1.1.1.3',plain,[-(model(284 ^ [560 ^ [thm, uns], 560 ^ [thm, uns]], 560 ^ [thm, uns])), status(560 ^ [thm, uns], 561 ^ [thm, uns], uns)],extension(459 ^ 8,bind([[_101516, _101518, _101667], [561 ^ [thm, uns], 560 ^ [thm, uns], 284 ^ [560 ^ [thm, uns], 560 ^ [thm, uns]]]]))).
% 44.59/43.92 ncf('1.1.1.1.3.1',plain,[-(status(560 ^ [thm, uns], 561 ^ [thm, uns], uns))],extension(563 ^ 9)).
% 44.59/43.92 ncf('1.1.1.2',plain,[model(72 ^ [561 ^ [thm, uns], not 561 ^ [thm, uns]], 561 ^ [thm, uns]), -(status(not 561 ^ [thm, uns], 561 ^ [thm, uns], esa)), 54 : model(_65953, not 561 ^ [thm, uns])],extension(42 ^ 7,bind([[_86553, _86555, _86796, _86977], [561 ^ [thm, uns], not 561 ^ [thm, uns], 72 ^ [561 ^ [thm, uns], not 561 ^ [thm, uns]], _65953]]))).
% 44.59/43.92 ncf('1.1.1.2.1',plain,[status(not 561 ^ [thm, uns], 561 ^ [thm, uns], esa), 71 : model(72 ^ [561 ^ [thm, uns], not 561 ^ [thm, uns]], 561 ^ [thm, uns]), 71 : -(model(72 ^ [561 ^ [thm, uns], not 561 ^ [thm, uns]], not 561 ^ [thm, uns]))],extension(58 ^ 8,bind([[_87099, _87101, _87488], [561 ^ [thm, uns], not 561 ^ [thm, uns], 72 ^ [561 ^ [thm, uns], not 561 ^ [thm, uns]]]]))).
% 44.59/43.92 ncf('1.1.1.2.1.1',plain,[-(model(72 ^ [561 ^ [thm, uns], not 561 ^ [thm, uns]], 561 ^ [thm, uns]))],reduction('1.1.1')).
% 44.59/43.92 ncf('1.1.1.2.1.2',plain,[model(72 ^ [561 ^ [thm, uns], not 561 ^ [thm, uns]], not 561 ^ [thm, uns]), model(72 ^ [561 ^ [thm, uns], not 561 ^ [thm, uns]], 561 ^ [thm, uns])],extension(621 ^ 11,bind([[_108093, _108095], [561 ^ [thm, uns], 72 ^ [561 ^ [thm, uns], not 561 ^ [thm, uns]]]]))).
% 44.59/43.92 ncf('1.1.1.2.1.2.1',plain,[-(model(72 ^ [561 ^ [thm, uns], not 561 ^ [thm, uns]], 561 ^ [thm, uns]))],reduction('1.1.1')).
% 44.59/43.92 ncf('1.1.1.2.2',plain,[-(model(_65953, not 561 ^ [thm, uns])), status(560 ^ [thm, uns], 561 ^ [thm, uns], uns)],extension(459 ^ 10,bind([[_101516, _101518, _101729], [561 ^ [thm, uns], 560 ^ [thm, uns], _65953]]))).
% 44.59/43.92 ncf('1.1.1.2.2.1',plain,[-(status(560 ^ [thm, uns], 561 ^ [thm, uns], uns))],extension(563 ^ 11)).
% 44.59/43.92 %-----------------------------------------------------
% 44.59/43.92 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------