%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO126+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n028.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:11:59 EDT 2023
% Result : Theorem 19.96s 19.99s
% Output : Proof 19.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO126+1 : TPTP v8.1.2. Released v2.4.0.
% 0.03/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n028.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Fri May 19 04:30:48 EDT 2023
% 0.13/0.34 % CPUTime :
% 19.96/19.99
% 19.96/19.99 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 19.96/19.99 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.96/19.99 %-----------------------------------------------------
% 19.96/19.99 ncf(matrix, plain, [(845 ^ _111405) ^ [_140988, _140990] : [ordered_by(843 ^ [], _140990, _140988), -(_140990 = _140988)], (228 ^ _111405) ^ [_119018, _119020] : [_119020 = _119018, -(underlying_curve(_119020) = underlying_curve(_119018))], (218 ^ _111405) ^ [_118707, _118709, _118711, _118713] : [-(sum(_118713, _118709) = sum(_118711, _118707)), _118713 = _118711, _118709 = _118707], (2 ^ _111405) ^ [_111549] : [-(_111549 = _111549)], (4 ^ _111405) ^ [_111656, _111658] : [_111658 = _111656, -(_111656 = _111658)], (10 ^ _111405) ^ [_111860, _111862, _111864] : [-(_111864 = _111860), _111864 = _111862, _111862 = _111860], (20 ^ _111405) ^ [_112173, _112175] : [-(closed(_112173)), _112175 = _112173, closed(_112175)], (30 ^ _111405) ^ [_112524, _112526, _112528, _112530, _112532, _112534] : [-(meet(_112532, _112528, _112524)), meet(_112534, _112530, _112526), _112534 = _112532, _112530 = _112528, _112526 = _112524], (48 ^ _111405) ^ [_113105, _113107, _113109, _113111] : [-(part_of(_113109, _113105)), part_of(_113111, _113107), _113111 = _113109, _113107 = _113105], (62 ^ _111405) ^ [_113549, _113551, _113553, _113555] : [-(end_point(_113553, _113549)), end_point(_113555, _113551), _113555 = _113553, _113551 = _113549], (76 ^ _111405) ^ [_113993, _113995, _113997, _113999] : [-(inner_point(_113997, _113993)), inner_point(_113999, _113995), _113999 = _113997, _113995 = _113993], (90 ^ _111405) ^ [_114437, _114439, _114441, _114443] : [-(finish_point(_114441, _114437)), finish_point(_114443, _114439), _114443 = _114441, _114439 = _114437], (104 ^ _111405) ^ [_114937, _114939, _114941, _114943, _114945, _114947, _114949, _114951] : [-(between_o(_114949, _114945, _114941, _114937)), between_o(_114951, _114947, _114943, _114939), _114951 = _114949, _114947 = _114945, _114943 = _114941, _114939 = _114937], (126 ^ _111405) ^ [_115727, _115729, _115731, _115733, _115735, _115737, _115739, _115741] : [-(between_c(_115739, _115735, _115731, _115727)), between_c(_115741, _115737, _115733, _115729), _115741 = _115739, _115737 = _115735, _115733 = _115731, _115729 = _115727], (148 ^ _111405) ^ [_116461, _116463, _116465, _116467] : [-(start_point(_116465, _116461)), start_point(_116467, _116463), _116467 = _116465, _116463 = _116461], (162 ^ _111405) ^ [_116877, _116879] : [-(open(_116877)), _116879 = _116877, open(_116879)], (172 ^ _111405) ^ [_117200, _117202, _117204, _117206] : [-(incident_o(_117204, _117200)), incident_o(_117206, _117202), _117206 = _117204, _117202 = _117200], (186 ^ _111405) ^ [_117644, _117646, _117648, _117650] : [-(incident_c(_117648, _117644)), incident_c(_117650, _117646), _117650 = _117648, _117646 = _117644], (200 ^ _111405) ^ [_118096, _118098, _118100, _118102, _118104, _118106] : [-(ordered_by(_118104, _118100, _118096)), ordered_by(_118106, _118102, _118098), _118106 = _118104, _118102 = _118100, _118098 = _118096], (573 ^ _111405) ^ [_130992, _130994, _130996, _130998] : [between_c(_130998, _130996, _130994, _130992), 576 ^ _111405 : [(577 ^ _111405) ^ [] : [_130996 = _130992], (580 ^ _111405) ^ [] : [-(part_of(578 ^ [_130992, _130994, _130996, _130998], _130998))], (582 ^ _111405) ^ [] : [-(end_point(_130996, 578 ^ [_130992, _130994, _130996, _130998]))], (584 ^ _111405) ^ [] : [-(end_point(_130992, 578 ^ [_130992, _130994, _130996, _130998]))], (586 ^ _111405) ^ [] : [-(inner_point(_130994, 578 ^ [_130992, _130994, _130996, _130998]))]]], (588 ^ _111405) ^ [_131604, _131606, _131608, _131610] : [-(between_c(_131610, _131608, _131606, _131604)), -(_131608 = _131604), 593 ^ _111405 : [(594 ^ _111405) ^ [_131810] : [part_of(_131810, _131610), end_point(_131608, _131810), end_point(_131604, _131810), inner_point(_131606, _131810)]]], (610 ^ _111405) ^ [_132367, _132369, _132371, _132373] : [between_o(_132373, _132371, _132369, _132367), 615 ^ _111405 : [(616 ^ _111405) ^ [] : [-(ordered_by(_132373, _132371, _132369))], (618 ^ _111405) ^ [] : [-(ordered_by(_132373, _132369, _132367))]], 619 ^ _111405 : [(620 ^ _111405) ^ [] : [-(ordered_by(_132373, _132367, _132369))], (622 ^ _111405) ^ [] : [-(ordered_by(_132373, _132369, _132371))]]], (624 ^ _111405) ^ [_132809, _132811, _132813, _132815] : [-(between_o(_132815, _132813, _132811, _132809)), 625 ^ _111405 : [(626 ^ _111405) ^ [] : [ordered_by(_132815, _132813, _132811), ordered_by(_132815, _132811, _132809)], (632 ^ _111405) ^ [] : [ordered_by(_132815, _132809, _132811), ordered_by(_132815, _132811, _132813)]]], (656 ^ _111405) ^ [_133841, _133843] : [-(start_point(_133843, _133841)), incident_o(_133843, _133841), 662 ^ _111405 : [(663 ^ _111405) ^ [] : [_133843 = 661 ^ [_133841, _133843]], (665 ^ _111405) ^ [] : [-(incident_o(661 ^ [_133841, _133843], _133841))], (667 ^ _111405) ^ [] : [ordered_by(_133841, _133843, 661 ^ [_133841, _133843])]]], (640 ^ _111405) ^ [_133346, _133348] : [start_point(_133348, _133346), 643 ^ _111405 : [(644 ^ _111405) ^ [] : [-(incident_o(_133348, _133346))], (646 ^ _111405) ^ [_133564] : [-(ordered_by(_133346, _133348, _133564)), -(_133348 = _133564), incident_o(_133564, _133346)]]], (687 ^ _111405) ^ [_134906, _134908] : [-(finish_point(_134908, _134906)), incident_o(_134908, _134906), 693 ^ _111405 : [(694 ^ _111405) ^ [] : [_134908 = 692 ^ [_134906, _134908]], (696 ^ _111405) ^ [] : [-(incident_o(692 ^ [_134906, _134908], _134906))], (698 ^ _111405) ^ [] : [ordered_by(_134906, 692 ^ [_134906, _134908], _134908)]]], (671 ^ _111405) ^ [_134411, _134413] : [finish_point(_134413, _134411), 674 ^ _111405 : [(675 ^ _111405) ^ [] : [-(incident_o(_134413, _134411))], (677 ^ _111405) ^ [_134629] : [-(ordered_by(_134411, _134629, _134413)), -(_134413 = _134629), incident_o(_134629, _134411)]]], (702 ^ _111405) ^ [_135461, _135463, _135465] : [ordered_by(_135465, _135463, _135461), 705 ^ _111405 : [(706 ^ _111405) ^ [] : [-(incident_o(_135463, _135465))], (708 ^ _111405) ^ [] : [-(incident_o(_135461, _135465))]]], (711 ^ _111405) ^ [_135802] : [-(open(709 ^ [_135802]))], (713 ^ _111405) ^ [_135908, _135910] : [incident_o(_135908, _135910), -(incident_c(_135908, 709 ^ [_135910]))], (719 ^ _111405) ^ [_136080, _136082] : [incident_c(_136080, 709 ^ [_136082]), -(incident_o(_136080, _136082))], (744 ^ _111405) ^ [_137136, _137138, _137140, _137142] : [-(between_o(_137136, _137142, _137140, _137138)), 745 ^ _111405 : [(746 ^ _111405) ^ [_137247] : [between_c(_137247, _137142, _137140, _137138), 750 ^ _111405 : [(751 ^ _111405) ^ [] : [-(incident_o(747 ^ [_137136, _137138, _137140, _137142, _137247], _137136))], (753 ^ _111405) ^ [] : [incident_c(747 ^ [_137136, _137138, _137140, _137142, _137247], _137247)]], 754 ^ _111405 : [(755 ^ _111405) ^ [] : [-(incident_c(747 ^ [_137136, _137138, _137140, _137142, _137247], _137247))], (757 ^ _111405) ^ [] : [incident_o(747 ^ [_137136, _137138, _137140, _137142, _137247], _137136)]]]]], (725 ^ _111405) ^ [_136361, _136363, _136365, _136367] : [between_o(_136361, _136367, _136365, _136363), 729 ^ _111405 : [(742 ^ _111405) ^ [] : [-(between_c(728 ^ [_136361, _136363, _136365, _136367], _136367, _136365, _136363))], (730 ^ _111405) ^ [_136644] : [incident_o(_136644, _136361), -(incident_c(_136644, 728 ^ [_136361, _136363, _136365, _136367]))], (736 ^ _111405) ^ [_136854] : [incident_c(_136854, 728 ^ [_136361, _136363, _136365, _136367]), -(incident_o(_136854, _136361))]]], (764 ^ _111405) ^ [_137935] : [-(start_point(762 ^ [_137935], _137935))], (766 ^ _111405) ^ [_138061, _138063, _138065] : [open(_138061), -(_138065 = _138063), incident_c(_138065, _138061), incident_c(_138063, _138061), 782 ^ _111405 : [(795 ^ _111405) ^ [] : [-(ordered_by(781 ^ [_138061, _138063, _138065], _138065, _138063))], (783 ^ _111405) ^ [_138610] : [incident_o(_138610, 781 ^ [_138061, _138063, _138065]), -(incident_c(_138610, _138061))], (789 ^ _111405) ^ [_138808] : [incident_c(_138808, _138061), -(incident_o(_138808, 781 ^ [_138061, _138063, _138065]))]]], (797 ^ _111405) ^ [_139127, _139129] : [-(_139129 = _139127), 802 ^ _111405 : [(803 ^ _111405) ^ [] : [-(ordered_by(_139129, 798 ^ [_139127, _139129], 799 ^ [_139127, _139129]))], (805 ^ _111405) ^ [] : [ordered_by(_139127, 798 ^ [_139127, _139129], 799 ^ [_139127, _139129])]], 806 ^ _111405 : [(807 ^ _111405) ^ [] : [-(ordered_by(_139127, 798 ^ [_139127, _139129], 799 ^ [_139127, _139129]))], (809 ^ _111405) ^ [] : [ordered_by(_139129, 798 ^ [_139127, _139129], 799 ^ [_139127, _139129])]]], (829 ^ _111405) ^ [_140300, _140302] : [-(_140302 = underlying_curve(_140300)), 833 ^ _111405 : [(834 ^ _111405) ^ [] : [-(incident_o(830 ^ [_140300, _140302], _140300))], (836 ^ _111405) ^ [] : [incident_c(830 ^ [_140300, _140302], _140302)]], 837 ^ _111405 : [(838 ^ _111405) ^ [] : [-(incident_c(830 ^ [_140300, _140302], _140302))], (840 ^ _111405) ^ [] : [incident_o(830 ^ [_140300, _140302], _140300)]]], (813 ^ _111405) ^ [_139779, _139781] : [_139781 = underlying_curve(_139779), 816 ^ _111405 : [(817 ^ _111405) ^ [_139949] : [incident_o(_139949, _139779), -(incident_c(_139949, _139781))], (823 ^ _111405) ^ [_140121] : [incident_c(_140121, _139781), -(incident_o(_140121, _139779))]]], (244 ^ _111405) ^ [_119637, _119639] : [246 ^ _111405 : [(247 ^ _111405) ^ [] : [-(incident_c(245 ^ [_119637, _119639], _119637))], (249 ^ _111405) ^ [] : [incident_c(245 ^ [_119637, _119639], _119639)]], -(part_of(_119637, _119639))], (234 ^ _111405) ^ [_119323, _119325] : [part_of(_119323, _119325), 237 ^ _111405 : [(238 ^ _111405) ^ [_119460] : [incident_c(_119460, _119323), -(incident_c(_119460, _119325))]]], (275 ^ _111405) ^ [_120762, _120764, _120766] : [-(_120766 = sum(_120764, _120762)), 279 ^ _111405 : [(280 ^ _111405) ^ [] : [-(incident_c(276 ^ [_120762, _120764, _120766], _120766))], (282 ^ _111405) ^ [] : [incident_c(276 ^ [_120762, _120764, _120766], _120764)], (284 ^ _111405) ^ [] : [incident_c(276 ^ [_120762, _120764, _120766], _120762)]], 285 ^ _111405 : [(292 ^ _111405) ^ [] : [incident_c(276 ^ [_120762, _120764, _120766], _120766)], (286 ^ _111405) ^ [] : [-(incident_c(276 ^ [_120762, _120764, _120766], _120764)), -(incident_c(276 ^ [_120762, _120764, _120766], _120762))]]], (253 ^ _111405) ^ [_120037, _120039, _120041] : [_120041 = sum(_120039, _120037), 256 ^ _111405 : [(267 ^ _111405) ^ [_120497] : [268 ^ _111405 : [(269 ^ _111405) ^ [] : [incident_c(_120497, _120039)], (271 ^ _111405) ^ [] : [incident_c(_120497, _120037)]], -(incident_c(_120497, _120041))], (257 ^ _111405) ^ [_120219] : [incident_c(_120219, _120041), -(incident_c(_120219, _120039)), -(incident_c(_120219, _120037))]]], (324 ^ _111405) ^ [_122370, _122372] : [-(end_point(_122372, _122370)), incident_c(_122372, _122370), 331 ^ _111405 : [(332 ^ _111405) ^ [] : [-(part_of(329 ^ [_122370, _122372], _122370))], (334 ^ _111405) ^ [] : [-(part_of(330 ^ [_122370, _122372], _122370))], (336 ^ _111405) ^ [] : [-(incident_c(_122372, 329 ^ [_122370, _122372]))], (338 ^ _111405) ^ [] : [-(incident_c(_122372, 330 ^ [_122370, _122372]))], (340 ^ _111405) ^ [] : [part_of(329 ^ [_122370, _122372], 330 ^ [_122370, _122372])], (342 ^ _111405) ^ [] : [part_of(330 ^ [_122370, _122372], 329 ^ [_122370, _122372])]]], (296 ^ _111405) ^ [_121542, _121544] : [end_point(_121544, _121542), 299 ^ _111405 : [(300 ^ _111405) ^ [] : [-(incident_c(_121544, _121542))], (302 ^ _111405) ^ [_121794, _121796] : [-(part_of(_121796, _121794)), -(part_of(_121794, _121796)), part_of(_121796, _121542), part_of(_121794, _121542), incident_c(_121544, _121796), incident_c(_121544, _121794)]]], (346 ^ _111405) ^ [_123325, _123327] : [inner_point(_123327, _123325), 349 ^ _111405 : [(350 ^ _111405) ^ [] : [-(incident_c(_123327, _123325))], (352 ^ _111405) ^ [] : [end_point(_123327, _123325)]]], (354 ^ _111405) ^ [_123563, _123565] : [-(inner_point(_123565, _123563)), incident_c(_123565, _123563), -(end_point(_123565, _123563))], (364 ^ _111405) ^ [_123910, _123912, _123914] : [meet(_123914, _123912, _123910), 367 ^ _111405 : [(368 ^ _111405) ^ [] : [-(incident_c(_123914, _123912))], (370 ^ _111405) ^ [] : [-(incident_c(_123914, _123910))], (372 ^ _111405) ^ [_124213] : [379 ^ _111405 : [(380 ^ _111405) ^ [] : [-(end_point(_124213, _123912))], (382 ^ _111405) ^ [] : [-(end_point(_124213, _123910))]], incident_c(_124213, _123912), incident_c(_124213, _123910)]]], (384 ^ _111405) ^ [_124578, _124580, _124582] : [-(meet(_124582, _124580, _124578)), incident_c(_124582, _124580), incident_c(_124582, _124578), 394 ^ _111405 : [(395 ^ _111405) ^ [] : [-(incident_c(393 ^ [_124578, _124580, _124582], _124580))], (397 ^ _111405) ^ [] : [-(incident_c(393 ^ [_124578, _124580, _124582], _124578))], (399 ^ _111405) ^ [] : [end_point(393 ^ [_124578, _124580, _124582], _124580), end_point(393 ^ [_124578, _124580, _124582], _124578)]]], (407 ^ _111405) ^ [_125355] : [closed(_125355), 410 ^ _111405 : [(411 ^ _111405) ^ [_125466] : [end_point(_125466, _125355)]]], (413 ^ _111405) ^ [_125532] : [-(end_point(414 ^ [_125532], _125532)), -(closed(_125532))], (420 ^ _111405) ^ [_125805] : [open(_125805), -(end_point(423 ^ [_125805], _125805))], (427 ^ _111405) ^ [_126010] : [428 ^ _111405 : [(429 ^ _111405) ^ [_126077] : [end_point(_126077, _126010)]], -(open(_126010))], (433 ^ _111405) ^ [_126236, _126238] : [-(open(_126236)), part_of(_126236, _126238), -(_126236 = _126238)], (443 ^ _111405) ^ [_126564, _126566, _126568, _126570] : [part_of(_126568, _126570), part_of(_126566, _126570), part_of(_126564, _126570), 456 ^ _111405 : [(457 ^ _111405) ^ [_126975] : [end_point(_126975, _126568), end_point(_126975, _126566), end_point(_126975, _126564)]], -(part_of(_126566, _126564)), -(part_of(_126564, _126566)), -(part_of(_126568, _126566)), -(part_of(_126566, _126568)), -(part_of(_126568, _126564)), -(part_of(_126564, _126568))], (490 ^ _111405) ^ [_127854] : [-(inner_point(488 ^ [_127854], _127854))], (492 ^ _111405) ^ [_127966, _127968] : [inner_point(_127966, _127968), 497 ^ _111405 : [(498 ^ _111405) ^ [] : [-(meet(_127966, 495 ^ [_127966, _127968], 496 ^ [_127966, _127968]))], (500 ^ _111405) ^ [] : [-(_127968 = sum(495 ^ [_127966, _127968], 496 ^ [_127966, _127968]))]]], (502 ^ _111405) ^ [_128454, _128456, _128458, _128460] : [end_point(_128458, _128460), end_point(_128456, _128460), end_point(_128454, _128460), -(_128458 = _128456), -(_128458 = _128454), -(_128456 = _128454)], (524 ^ _111405) ^ [_129070, _129072] : [end_point(_129070, _129072), 528 ^ _111405 : [(529 ^ _111405) ^ [] : [-(end_point(527 ^ [_129070, _129072], _129072))], (531 ^ _111405) ^ [] : [_129070 = 527 ^ [_129070, _129072]]]], (533 ^ _111405) ^ [_129456, _129458, _129460, _129462] : [544 ^ _111405 : [(545 ^ _111405) ^ [_129802] : [end_point(_129802, _129460), -(meet(_129802, _129460, _129458))]], closed(_129462), meet(_129456, _129460, _129458), _129462 = sum(_129460, _129458)], (551 ^ _111405) ^ [_130045, _130047] : [552 ^ _111405 : [(553 ^ _111405) ^ [_130124] : [meet(_130124, _130047, _130045)]], -(554 ^ [_130045, _130047] = sum(_130047, _130045))], (558 ^ _111405) ^ [_130325, _130327] : [-(_130327 = _130325), 562 ^ _111405 : [(563 ^ _111405) ^ [] : [-(incident_c(559 ^ [_130325, _130327], _130327))], (565 ^ _111405) ^ [] : [incident_c(559 ^ [_130325, _130327], _130325)]], 566 ^ _111405 : [(567 ^ _111405) ^ [] : [-(incident_c(559 ^ [_130325, _130327], _130325))], (569 ^ _111405) ^ [] : [incident_c(559 ^ [_130325, _130327], _130327)]]]], input).
% 19.96/19.99 ncf('1',plain,[end_point(423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]), 531 : 423 ^ [709 ^ [843 ^ []]] = 527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]]],start(524 ^ 0,bind([[_129070, _129072], [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]]]))).
% 19.96/19.99 ncf('1.1',plain,[-(end_point(423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []])), end_point(423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]), 423 ^ [709 ^ [843 ^ []]] = 423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []] = 709 ^ [843 ^ []]],extension(62 ^ 1,bind([[_113549, _113551, _113553, _113555], [709 ^ [843 ^ []], 709 ^ [843 ^ []], 423 ^ [709 ^ [843 ^ []]], 423 ^ [709 ^ [843 ^ []]]]]))).
% 19.96/19.99 ncf('1.1.1',plain,[-(end_point(423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []])), end_point(423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]), 423 ^ [709 ^ [843 ^ []]] = 423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []] = 709 ^ [843 ^ []]],extension(62 ^ 2,bind([[_113549, _113551, _113553, _113555], [709 ^ [843 ^ []], 709 ^ [843 ^ []], 423 ^ [709 ^ [843 ^ []]], 423 ^ [709 ^ [843 ^ []]]]]))).
% 19.96/19.99 ncf('1.1.1.1',plain,[-(end_point(423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []])), end_point(423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]), 423 ^ [709 ^ [843 ^ []]] = 423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []] = 709 ^ [843 ^ []]],extension(62 ^ 3,bind([[_113549, _113551, _113553, _113555], [709 ^ [843 ^ []], 709 ^ [843 ^ []], 423 ^ [709 ^ [843 ^ []]], 423 ^ [709 ^ [843 ^ []]]]]))).
% 19.96/19.99 ncf('1.1.1.1.1',plain,[-(end_point(423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []])), open(709 ^ [843 ^ []])],extension(420 ^ 4,bind([[_125805], [709 ^ [843 ^ []]]]))).
% 19.96/19.99 ncf('1.1.1.1.1.1',plain,[-(open(709 ^ [843 ^ []]))],extension(711 ^ 5,bind([[_135802], [843 ^ []]]))).
% 19.96/19.99 ncf('1.1.1.1.2',plain,[-(423 ^ [709 ^ [843 ^ []]] = 423 ^ [709 ^ [843 ^ []]])],extension(2 ^ 4,bind([[_111549], [423 ^ [709 ^ [843 ^ []]]]]))).
% 19.96/19.99 ncf('1.1.1.1.3',plain,[-(709 ^ [843 ^ []] = 709 ^ [843 ^ []])],extension(2 ^ 4,bind([[_111549], [709 ^ [843 ^ []]]]))).
% 19.96/19.99 ncf('1.1.1.2',plain,[-(423 ^ [709 ^ [843 ^ []]] = 423 ^ [709 ^ [843 ^ []]])],extension(2 ^ 3,bind([[_111549], [423 ^ [709 ^ [843 ^ []]]]]))).
% 19.96/19.99 ncf('1.1.1.3',plain,[-(709 ^ [843 ^ []] = 709 ^ [843 ^ []])],extension(2 ^ 3,bind([[_111549], [709 ^ [843 ^ []]]]))).
% 19.96/19.99 ncf('1.1.2',plain,[-(423 ^ [709 ^ [843 ^ []]] = 423 ^ [709 ^ [843 ^ []]])],extension(2 ^ 2,bind([[_111549], [423 ^ [709 ^ [843 ^ []]]]]))).
% 19.96/19.99 ncf('1.1.3',plain,[-(709 ^ [843 ^ []] = 709 ^ [843 ^ []])],extension(2 ^ 2,bind([[_111549], [709 ^ [843 ^ []]]]))).
% 19.96/19.99 ncf('1.2',plain,[-(423 ^ [709 ^ [843 ^ []]] = 527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]]), 677 : -(ordered_by(843 ^ [], 527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]], 423 ^ [709 ^ [843 ^ []]])), 677 : incident_o(527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]], 843 ^ []), 677 : finish_point(423 ^ [709 ^ [843 ^ []]], 843 ^ [])],extension(671 ^ 3,bind([[_134411, _134413, _134629], [843 ^ [], 423 ^ [709 ^ [843 ^ []]], 527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]]]]))).
% 19.96/19.99 ncf('1.2.1',plain,[ordered_by(843 ^ [], 527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]], 423 ^ [709 ^ [843 ^ []]]), -(527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]] = 423 ^ [709 ^ [843 ^ []]])],extension(845 ^ 6,bind([[_140988, _140990], [423 ^ [709 ^ [843 ^ []]], 527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]]]]))).
% 19.96/19.99 ncf('1.2.1.1',plain,[527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]] = 423 ^ [709 ^ [843 ^ []]], -(423 ^ [709 ^ [843 ^ []]] = 527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]])],extension(4 ^ 7,bind([[_111656, _111658], [423 ^ [709 ^ [843 ^ []]], 527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]]]]))).
% 19.96/19.99 ncf('1.2.1.1.1',plain,[423 ^ [709 ^ [843 ^ []]] = 527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]]],reduction('1')).
% 19.96/19.99 ncf('1.2.2',plain,[-(incident_o(527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]], 843 ^ [])), incident_c(527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]], 709 ^ [843 ^ []])],extension(719 ^ 6,bind([[_136080, _136082], [527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]], 843 ^ []]]))).
% 19.96/19.99 ncf('1.2.2.1',plain,[-(incident_c(527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]], 709 ^ [843 ^ []])), 238 : incident_c(527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]], 709 ^ [843 ^ []]), 238 : part_of(709 ^ [843 ^ []], 709 ^ [843 ^ []])],extension(234 ^ 7,bind([[_119323, _119325, _119460], [709 ^ [843 ^ []], 709 ^ [843 ^ []], 527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]]]]))).
% 19.96/19.99 ncf('1.2.2.1.1',plain,[-(incident_c(527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]], 709 ^ [843 ^ []])), end_point(527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]], 709 ^ [843 ^ []])],extension(296 ^ 10,bind([[_121542, _121544], [709 ^ [843 ^ []], 527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]]]]))).
% 19.96/19.99 ncf('1.2.2.1.1.1',plain,[-(end_point(527 ^ [423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]], 709 ^ [843 ^ []]))],extension(529 ^ 11)).
% 19.96/19.99 ncf('1.2.2.1.2',plain,[-(part_of(709 ^ [843 ^ []], 709 ^ [843 ^ []])), 247 : -(incident_c(245 ^ [709 ^ [843 ^ []], 709 ^ [843 ^ []]], 709 ^ [843 ^ []]))],extension(244 ^ 8,bind([[_119637, _119639], [709 ^ [843 ^ []], 709 ^ [843 ^ []]]]))).
% 19.96/19.99 ncf('1.2.2.1.2.1',plain,[incident_c(245 ^ [709 ^ [843 ^ []], 709 ^ [843 ^ []]], 709 ^ [843 ^ []])],extension(249 ^ 11)).
% 19.96/19.99 ncf('1.2.3',plain,[-(finish_point(423 ^ [709 ^ [843 ^ []]], 843 ^ [])), finish_point(762 ^ [843 ^ []], 843 ^ []), 762 ^ [843 ^ []] = 423 ^ [709 ^ [843 ^ []]], 843 ^ [] = 843 ^ []],extension(90 ^ 4,bind([[_114437, _114439, _114441, _114443], [843 ^ [], 843 ^ [], 423 ^ [709 ^ [843 ^ []]], 762 ^ [843 ^ []]]]))).
% 19.96/19.99 ncf('1.2.3.1',plain,[-(finish_point(762 ^ [843 ^ []], 843 ^ [])), incident_o(762 ^ [843 ^ []], 843 ^ []), 694 : 762 ^ [843 ^ []] = 692 ^ [843 ^ [], 762 ^ [843 ^ []]]],extension(687 ^ 5,bind([[_134906, _134908], [843 ^ [], 762 ^ [843 ^ []]]]))).
% 19.96/19.99 ncf('1.2.3.1.1',plain,[-(incident_o(762 ^ [843 ^ []], 843 ^ [])), start_point(762 ^ [843 ^ []], 843 ^ [])],extension(640 ^ 6,bind([[_133346, _133348], [843 ^ [], 762 ^ [843 ^ []]]]))).
% 19.96/19.99 ncf('1.2.3.1.1.1',plain,[-(start_point(762 ^ [843 ^ []], 843 ^ []))],extension(764 ^ 7,bind([[_137935], [843 ^ []]]))).
% 19.96/19.99 ncf('1.2.3.1.2',plain,[-(762 ^ [843 ^ []] = 692 ^ [843 ^ [], 762 ^ [843 ^ []]]), 646 : -(ordered_by(843 ^ [], 762 ^ [843 ^ []], 692 ^ [843 ^ [], 762 ^ [843 ^ []]])), 646 : incident_o(692 ^ [843 ^ [], 762 ^ [843 ^ []]], 843 ^ []), 646 : start_point(762 ^ [843 ^ []], 843 ^ [])],extension(640 ^ 8,bind([[_133346, _133348, _133564], [843 ^ [], 762 ^ [843 ^ []], 692 ^ [843 ^ [], 762 ^ [843 ^ []]]]]))).
% 19.96/19.99 ncf('1.2.3.1.2.1',plain,[ordered_by(843 ^ [], 762 ^ [843 ^ []], 692 ^ [843 ^ [], 762 ^ [843 ^ []]]), -(762 ^ [843 ^ []] = 692 ^ [843 ^ [], 762 ^ [843 ^ []]])],extension(845 ^ 11,bind([[_140988, _140990], [692 ^ [843 ^ [], 762 ^ [843 ^ []]], 762 ^ [843 ^ []]]]))).
% 19.96/19.99 ncf('1.2.3.1.2.1.1',plain,[762 ^ [843 ^ []] = 692 ^ [843 ^ [], 762 ^ [843 ^ []]]],reduction('1.2.3.1')).
% 19.96/19.99 ncf('1.2.3.1.2.2',plain,[-(incident_o(692 ^ [843 ^ [], 762 ^ [843 ^ []]], 843 ^ []))],extension(696 ^ 11)).
% 19.96/19.99 ncf('1.2.3.1.2.3',plain,[-(start_point(762 ^ [843 ^ []], 843 ^ []))],extension(764 ^ 9,bind([[_137935], [843 ^ []]]))).
% 19.96/19.99 ncf('1.2.3.2',plain,[-(762 ^ [843 ^ []] = 423 ^ [709 ^ [843 ^ []]]), 646 : -(ordered_by(843 ^ [], 762 ^ [843 ^ []], 423 ^ [709 ^ [843 ^ []]])), 646 : incident_o(423 ^ [709 ^ [843 ^ []]], 843 ^ []), 646 : start_point(762 ^ [843 ^ []], 843 ^ [])],extension(640 ^ 5,bind([[_133346, _133348, _133564], [843 ^ [], 762 ^ [843 ^ []], 423 ^ [709 ^ [843 ^ []]]]]))).
% 19.96/19.99 ncf('1.2.3.2.1',plain,[ordered_by(843 ^ [], 762 ^ [843 ^ []], 423 ^ [709 ^ [843 ^ []]]), -(762 ^ [843 ^ []] = 423 ^ [709 ^ [843 ^ []]])],extension(845 ^ 8,bind([[_140988, _140990], [423 ^ [709 ^ [843 ^ []]], 762 ^ [843 ^ []]]]))).
% 19.96/19.99 ncf('1.2.3.2.1.1',plain,[762 ^ [843 ^ []] = 423 ^ [709 ^ [843 ^ []]]],reduction('1.2.3')).
% 19.96/19.99 ncf('1.2.3.2.2',plain,[-(incident_o(423 ^ [709 ^ [843 ^ []]], 843 ^ [])), incident_c(423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []])],extension(719 ^ 8,bind([[_136080, _136082], [423 ^ [709 ^ [843 ^ []]], 843 ^ []]]))).
% 19.96/19.99 ncf('1.2.3.2.2.1',plain,[-(incident_c(423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []])), end_point(423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []])],extension(296 ^ 9,bind([[_121542, _121544], [709 ^ [843 ^ []], 423 ^ [709 ^ [843 ^ []]]]]))).
% 19.96/19.99 ncf('1.2.3.2.2.1.1',plain,[-(end_point(423 ^ [709 ^ [843 ^ []]], 709 ^ [843 ^ []]))],lemmata('x')).
% 19.96/19.99 ncf('1.2.3.2.3',plain,[-(start_point(762 ^ [843 ^ []], 843 ^ [])), start_point(762 ^ [843 ^ []], 843 ^ []), 762 ^ [843 ^ []] = 762 ^ [843 ^ []], 843 ^ [] = 843 ^ []],extension(148 ^ 6,bind([[_116461, _116463, _116465, _116467], [843 ^ [], 843 ^ [], 762 ^ [843 ^ []], 762 ^ [843 ^ []]]]))).
% 19.96/19.99 ncf('1.2.3.2.3.1',plain,[-(start_point(762 ^ [843 ^ []], 843 ^ []))],extension(764 ^ 7,bind([[_137935], [843 ^ []]]))).
% 19.96/19.99 ncf('1.2.3.2.3.2',plain,[-(762 ^ [843 ^ []] = 762 ^ [843 ^ []])],extension(2 ^ 7,bind([[_111549], [762 ^ [843 ^ []]]]))).
% 19.96/19.99 ncf('1.2.3.2.3.3',plain,[-(843 ^ [] = 843 ^ [])],extension(2 ^ 7,bind([[_111549], [843 ^ []]]))).
% 19.96/19.99 ncf('1.2.3.3',plain,[-(843 ^ [] = 843 ^ [])],extension(2 ^ 5,bind([[_111549], [843 ^ []]]))).
% 19.96/19.99 %-----------------------------------------------------
% 19.96/19.99 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------