%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO266+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n015.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:12:23 EDT 2023
% Result : Theorem 2.77s 3.44s
% Output : Proof 2.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GEO266+3 : TPTP v8.1.2. Released v4.0.0.
% 0.06/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n015.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:34:22 EDT 2023
% 0.13/0.34 % CPUTime :
% 2.77/3.44
% 2.77/3.44 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 2.77/3.44 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.77/3.44 %-----------------------------------------------------
% 2.77/3.44 ncf(matrix, plain, [(438 ^ _68249) ^ [] : [439 ^ _68249 : [(440 ^ _68249) ^ [] : [-(unequally_directed_opposite_lines(435 ^ [], 436 ^ []))], (442 ^ _68249) ^ [] : [unequally_directed_opposite_lines(436 ^ [], 435 ^ [])]], 443 ^ _68249 : [(444 ^ _68249) ^ [] : [-(unequally_directed_opposite_lines(436 ^ [], 435 ^ []))], (446 ^ _68249) ^ [] : [unequally_directed_opposite_lines(435 ^ [], 436 ^ [])]]], (2 ^ _68249) ^ [_68391, _68393] : [unequally_directed_opposite_lines(_68393, _68391), -(unequally_directed_lines(_68393, reverse_line(_68391)))], (8 ^ _68249) ^ [_68557, _68559] : [unequally_directed_lines(_68559, reverse_line(_68557)), -(unequally_directed_opposite_lines(_68559, _68557))], (14 ^ _68249) ^ [_68802, _68804] : [right_apart_point(_68804, _68802), -(left_apart_point(_68804, reverse_line(_68802)))], (20 ^ _68249) ^ [_68968, _68970] : [left_apart_point(_68970, reverse_line(_68968)), -(right_apart_point(_68970, _68968))], (26 ^ _68249) ^ [_69213, _69215] : [right_convergent_lines(_69215, _69213), -(left_convergent_lines(_69215, reverse_line(_69213)))], (32 ^ _68249) ^ [_69379, _69381] : [left_convergent_lines(_69381, reverse_line(_69379)), -(right_convergent_lines(_69381, _69379))], (38 ^ _68249) ^ [_69624, _69626] : [equally_directed_lines(_69626, _69624), unequally_directed_lines(_69626, _69624)], (44 ^ _68249) ^ [_69787, _69789] : [-(unequally_directed_lines(_69789, _69787)), -(equally_directed_lines(_69789, _69787))], (50 ^ _68249) ^ [_70031, _70033] : [equally_directed_opposite_lines(_70033, _70031), unequally_directed_opposite_lines(_70033, _70031)], (56 ^ _68249) ^ [_70194, _70196] : [-(unequally_directed_opposite_lines(_70196, _70194)), -(equally_directed_opposite_lines(_70196, _70194))], (72 ^ _68249) ^ [_70690, _70692] : [73 ^ _68249 : [(74 ^ _68249) ^ [] : [left_apart_point(_70692, _70690)], (76 ^ _68249) ^ [] : [right_apart_point(_70692, _70690)]], -(apart_point_and_line(_70692, _70690))], (62 ^ _68249) ^ [_70438, _70440] : [apart_point_and_line(_70440, _70438), -(left_apart_point(_70440, _70438)), -(right_apart_point(_70440, _70438))], (80 ^ _68249) ^ [_71005, _71007] : [convergent_lines(_71007, _71005), 83 ^ _68249 : [(84 ^ _68249) ^ [] : [-(unequally_directed_lines(_71007, _71005))], (86 ^ _68249) ^ [] : [-(unequally_directed_opposite_lines(_71007, _71005))]]], (88 ^ _68249) ^ [_71242, _71244] : [-(convergent_lines(_71244, _71242)), unequally_directed_lines(_71244, _71242), unequally_directed_opposite_lines(_71244, _71242)], (98 ^ _68249) ^ [_71586, _71588, _71590] : [divides_points(_71586, _71590, _71588), 103 ^ _68249 : [(104 ^ _68249) ^ [] : [-(left_apart_point(_71590, _71586))], (106 ^ _68249) ^ [] : [-(right_apart_point(_71588, _71586))]], 107 ^ _68249 : [(108 ^ _68249) ^ [] : [-(right_apart_point(_71590, _71586))], (110 ^ _68249) ^ [] : [-(left_apart_point(_71588, _71586))]]], (112 ^ _68249) ^ [_72004, _72006, _72008] : [-(divides_points(_72004, _72008, _72006)), 113 ^ _68249 : [(114 ^ _68249) ^ [] : [left_apart_point(_72008, _72004), right_apart_point(_72006, _72004)], (120 ^ _68249) ^ [] : [right_apart_point(_72008, _72004), left_apart_point(_72006, _72004)]]], (128 ^ _68249) ^ [_72529, _72531, _72533] : [before_on_line(_72533, _72531, _72529), 131 ^ _68249 : [(132 ^ _68249) ^ [] : [-(distinct_points(_72531, _72529))], (134 ^ _68249) ^ [] : [-(incident_point_and_line(_72531, _72533))], (136 ^ _68249) ^ [] : [-(incident_point_and_line(_72529, _72533))], (138 ^ _68249) ^ [] : [-(equally_directed_lines(_72533, line_connecting(_72531, _72529)))]]], (140 ^ _68249) ^ [_72934, _72936, _72938] : [-(before_on_line(_72938, _72936, _72934)), distinct_points(_72936, _72934), incident_point_and_line(_72936, _72938), incident_point_and_line(_72934, _72938), equally_directed_lines(_72938, line_connecting(_72936, _72934))], (158 ^ _68249) ^ [_73496, _73498, _73500, _73502] : [between_on_line(_73502, _73500, _73498, _73496), 163 ^ _68249 : [(164 ^ _68249) ^ [] : [-(before_on_line(_73502, _73500, _73498))], (166 ^ _68249) ^ [] : [-(before_on_line(_73502, _73498, _73496))]], 167 ^ _68249 : [(168 ^ _68249) ^ [] : [-(before_on_line(_73502, _73496, _73498))], (170 ^ _68249) ^ [] : [-(before_on_line(_73502, _73498, _73500))]]], (172 ^ _68249) ^ [_73938, _73940, _73942, _73944] : [-(between_on_line(_73944, _73942, _73940, _73938)), 173 ^ _68249 : [(174 ^ _68249) ^ [] : [before_on_line(_73944, _73942, _73940), before_on_line(_73944, _73940, _73938)], (180 ^ _68249) ^ [] : [before_on_line(_73944, _73938, _73940), before_on_line(_73944, _73940, _73942)]]], (188 ^ _68249) ^ [_74416] : [distinct_points(_74416, _74416)], (190 ^ _68249) ^ [_74537, _74539, _74541] : [distinct_points(_74541, _74539), -(distinct_points(_74541, _74537)), -(distinct_points(_74539, _74537))], (200 ^ _68249) ^ [_74817] : [distinct_lines(_74817, _74817)], (202 ^ _68249) ^ [_74938, _74940, _74942] : [distinct_lines(_74942, _74940), -(distinct_lines(_74942, _74938)), -(distinct_lines(_74940, _74938))], (212 ^ _68249) ^ [_75219] : [-(equally_directed_lines(_75219, _75219))], (214 ^ _68249) ^ [_75340, _75342, _75344] : [unequally_directed_lines(_75344, _75342), -(unequally_directed_lines(_75344, _75340)), -(unequally_directed_lines(_75342, _75340))], (224 ^ _68249) ^ [_75664, _75666, _75668] : [unequally_directed_lines(_75668, _75666), unequally_directed_lines(_75668, reverse_line(_75666)), 233 ^ _68249 : [(234 ^ _68249) ^ [] : [-(unequally_directed_lines(_75668, _75664))], (236 ^ _68249) ^ [] : [-(unequally_directed_lines(_75668, reverse_line(_75664)))]], 237 ^ _68249 : [(238 ^ _68249) ^ [] : [-(unequally_directed_lines(_75666, _75664))], (240 ^ _68249) ^ [] : [-(unequally_directed_lines(_75666, reverse_line(_75664)))]]], (242 ^ _68249) ^ [_76235, _76237] : [-(unequally_directed_lines(_76237, _76235)), -(unequally_directed_lines(_76237, reverse_line(_76235)))], (248 ^ _68249) ^ [_76450, _76452] : [unequally_directed_lines(_76452, _76450), unequally_directed_lines(_76452, reverse_line(_76450)), -(left_convergent_lines(_76452, _76450)), -(left_convergent_lines(_76452, reverse_line(_76450)))], (262 ^ _68249) ^ [_76853, _76855] : [left_apart_point(_76855, _76853)], (264 ^ _68249) ^ [_76898, _76900] : [left_apart_point(_76900, reverse_line(_76898))], (266 ^ _68249) ^ [_77015, _77017] : [left_convergent_lines(_77017, _77015)], (268 ^ _68249) ^ [_77060, _77062] : [left_convergent_lines(_77062, reverse_line(_77060))], (270 ^ _68249) ^ [_77173, _77175] : [-(line(line_connecting(_77175, _77173))), point(_77175), point(_77173), distinct_points(_77175, _77173)], (284 ^ _68249) ^ [_77561, _77563] : [-(point(intersection_point(_77563, _77561))), line(_77563), line(_77561), unequally_directed_lines(_77563, _77561), unequally_directed_lines(_77563, reverse_line(_77561))], (302 ^ _68249) ^ [_78042, _78044] : [-(line(parallel_through_point(_78044, _78042))), point(_78042), line(_78044)], (312 ^ _68249) ^ [_78327] : [line(_78327), -(line(reverse_line(_78327)))], (318 ^ _68249) ^ [_78531, _78533] : [distinct_points(_78533, _78531), 321 ^ _68249 : [(322 ^ _68249) ^ [] : [apart_point_and_line(_78533, line_connecting(_78533, _78531))], (324 ^ _68249) ^ [] : [apart_point_and_line(_78531, line_connecting(_78533, _78531))]]], (326 ^ _68249) ^ [_78830, _78832] : [333 ^ _68249 : [(334 ^ _68249) ^ [] : [apart_point_and_line(intersection_point(_78832, _78830), _78832)], (336 ^ _68249) ^ [] : [apart_point_and_line(intersection_point(_78832, _78830), _78830)]], unequally_directed_lines(_78832, _78830), unequally_directed_lines(_78832, reverse_line(_78830))], (338 ^ _68249) ^ [_79206, _79208] : [apart_point_and_line(_79208, parallel_through_point(_79206, _79208))], (340 ^ _68249) ^ [_79288] : [distinct_lines(_79288, reverse_line(_79288))], (342 ^ _68249) ^ [_79397, _79399] : [distinct_points(_79399, _79397), -(equally_directed_lines(line_connecting(_79399, _79397), reverse_line(line_connecting(_79397, _79399))))], (348 ^ _68249) ^ [_79608, _79610] : [-(equally_directed_lines(parallel_through_point(_79608, _79610), _79608))], (350 ^ _68249) ^ [_79748, _79750, _79752, _79754] : [distinct_points(_79754, _79752), distinct_lines(_79750, _79748), -(left_apart_point(_79754, _79750)), -(left_apart_point(_79752, _79750)), -(left_apart_point(_79754, _79748)), -(left_apart_point(_79752, _79748)), -(left_apart_point(_79754, reverse_line(_79750))), -(left_apart_point(_79752, reverse_line(_79750))), -(left_apart_point(_79754, reverse_line(_79748))), -(left_apart_point(_79752, reverse_line(_79748)))], (388 ^ _68249) ^ [_80785, _80787, _80789] : [distinct_points(_80789, _80787), left_apart_point(_80789, _80785), -(left_apart_point(_80787, _80785)), -(left_convergent_lines(line_connecting(_80789, _80787), _80785))], (402 ^ _68249) ^ [_81210, _81212, _81214] : [left_apart_point(_81214, _81210), -(distinct_points(_81214, _81212)), -(left_apart_point(_81212, _81210))], (426 ^ _68249) ^ [_81937, _81939, _81941] : [left_convergent_lines(_81941, _81939), -(unequally_directed_lines(_81939, _81937)), -(left_convergent_lines(_81941, _81937))], (412 ^ _68249) ^ [_81534, _81536, _81538] : [left_apart_point(_81538, _81536), unequally_directed_lines(_81536, _81534), -(distinct_lines(_81536, _81534)), -(left_apart_point(_81538, reverse_line(_81534)))]], input).
% 2.77/3.44 ncf('1',plain,[442 : unequally_directed_opposite_lines(436 ^ [], 435 ^ []), 446 : unequally_directed_opposite_lines(435 ^ [], 436 ^ [])],start(438 ^ 0)).
% 2.77/3.44 ncf('1.1',plain,[-(unequally_directed_opposite_lines(436 ^ [], 435 ^ [])), unequally_directed_lines(436 ^ [], reverse_line(435 ^ []))],extension(8 ^ 3,bind([[_68557, _68559], [435 ^ [], 436 ^ []]]))).
% 2.77/3.44 ncf('1.1.1',plain,[-(unequally_directed_lines(436 ^ [], reverse_line(435 ^ []))), unequally_directed_lines(436 ^ [], reverse_line(436 ^ [])), -(unequally_directed_lines(reverse_line(436 ^ []), reverse_line(435 ^ [])))],extension(214 ^ 4,bind([[_75340, _75342, _75344], [reverse_line(435 ^ []), reverse_line(436 ^ []), 436 ^ []]]))).
% 2.77/3.44 ncf('1.1.1.1',plain,[-(unequally_directed_lines(436 ^ [], reverse_line(436 ^ []))), unequally_directed_lines(436 ^ [], reverse_line(436 ^ [])), -(unequally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ [])))],extension(214 ^ 5,bind([[_75340, _75342, _75344], [reverse_line(436 ^ []), reverse_line(436 ^ []), 436 ^ []]]))).
% 2.77/3.44 ncf('1.1.1.1.1',plain,[-(unequally_directed_lines(436 ^ [], reverse_line(436 ^ []))), unequally_directed_lines(436 ^ [], reverse_line(436 ^ [])), -(unequally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ [])))],extension(214 ^ 6,bind([[_75340, _75342, _75344], [reverse_line(436 ^ []), reverse_line(436 ^ []), 436 ^ []]]))).
% 2.77/3.44 ncf('1.1.1.1.1.1',plain,[-(unequally_directed_lines(436 ^ [], reverse_line(436 ^ []))), unequally_directed_lines(436 ^ [], 436 ^ []), -(unequally_directed_lines(436 ^ [], reverse_line(436 ^ [])))],extension(214 ^ 7,bind([[_75340, _75342, _75344], [reverse_line(436 ^ []), 436 ^ [], 436 ^ []]]))).
% 2.77/3.44 ncf('1.1.1.1.1.1.1',plain,[-(unequally_directed_lines(436 ^ [], 436 ^ [])), -(unequally_directed_lines(436 ^ [], reverse_line(436 ^ [])))],extension(242 ^ 8,bind([[_76235, _76237], [436 ^ [], 436 ^ []]]))).
% 2.77/3.44 ncf('1.1.1.1.1.1.1.1',plain,[unequally_directed_lines(436 ^ [], reverse_line(436 ^ []))],reduction('1.1.1.1.1')).
% 2.77/3.44 ncf('1.1.1.1.1.1.2',plain,[unequally_directed_lines(436 ^ [], reverse_line(436 ^ []))],reduction('1.1.1.1.1')).
% 2.77/3.44 ncf('1.1.1.1.1.2',plain,[unequally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ [])), equally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ []))],extension(38 ^ 7,bind([[_69624, _69626], [reverse_line(436 ^ []), reverse_line(436 ^ [])]]))).
% 2.77/3.44 ncf('1.1.1.1.1.2.1',plain,[-(equally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ [])))],extension(212 ^ 8,bind([[_75219], [reverse_line(436 ^ [])]]))).
% 2.77/3.44 ncf('1.1.1.1.2',plain,[unequally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ [])), equally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ []))],extension(38 ^ 6,bind([[_69624, _69626], [reverse_line(436 ^ []), reverse_line(436 ^ [])]]))).
% 2.77/3.44 ncf('1.1.1.1.2.1',plain,[-(equally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ [])))],extension(212 ^ 7,bind([[_75219], [reverse_line(436 ^ [])]]))).
% 2.77/3.44 ncf('1.1.1.2',plain,[unequally_directed_lines(reverse_line(436 ^ []), reverse_line(435 ^ [])), unequally_directed_lines(reverse_line(436 ^ []), reverse_line(reverse_line(435 ^ []))), 234 : -(unequally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ []))), 238 : -(unequally_directed_lines(reverse_line(435 ^ []), reverse_line(436 ^ [])))],extension(224 ^ 5,bind([[_75664, _75666, _75668], [reverse_line(436 ^ []), reverse_line(435 ^ []), reverse_line(436 ^ [])]]))).
% 2.77/3.44 ncf('1.1.1.2.1',plain,[-(unequally_directed_lines(reverse_line(436 ^ []), reverse_line(reverse_line(435 ^ [])))), unequally_directed_lines(435 ^ [], reverse_line(436 ^ [])), unequally_directed_lines(435 ^ [], reverse_line(reverse_line(436 ^ []))), 234 : -(unequally_directed_lines(435 ^ [], reverse_line(reverse_line(435 ^ []))))],extension(224 ^ 6,bind([[_75664, _75666, _75668], [reverse_line(reverse_line(435 ^ [])), reverse_line(436 ^ []), 435 ^ []]]))).
% 2.77/3.44 ncf('1.1.1.2.1.1',plain,[-(unequally_directed_lines(435 ^ [], reverse_line(436 ^ []))), unequally_directed_opposite_lines(435 ^ [], 436 ^ [])],extension(2 ^ 7,bind([[_68391, _68393], [436 ^ [], 435 ^ []]]))).
% 2.77/3.44 ncf('1.1.1.2.1.1.1',plain,[-(unequally_directed_opposite_lines(435 ^ [], 436 ^ []))],extension(440 ^ 8)).
% 2.77/3.44 ncf('1.1.1.2.1.2',plain,[-(unequally_directed_lines(435 ^ [], reverse_line(reverse_line(436 ^ [])))), unequally_directed_lines(436 ^ [], 435 ^ []), -(unequally_directed_lines(436 ^ [], reverse_line(reverse_line(436 ^ []))))],extension(214 ^ 7,bind([[_75340, _75342, _75344], [reverse_line(reverse_line(436 ^ [])), 435 ^ [], 436 ^ []]]))).
% 2.77/3.44 ncf('1.1.1.2.1.2.1',plain,[-(unequally_directed_lines(436 ^ [], 435 ^ [])), -(unequally_directed_lines(436 ^ [], reverse_line(435 ^ [])))],extension(242 ^ 8,bind([[_76235, _76237], [435 ^ [], 436 ^ []]]))).
% 2.77/3.44 ncf('1.1.1.2.1.2.1.1',plain,[unequally_directed_lines(436 ^ [], reverse_line(435 ^ []))],reduction('1.1')).
% 2.77/3.44 ncf('1.1.1.2.1.2.2',plain,[unequally_directed_lines(436 ^ [], reverse_line(reverse_line(436 ^ []))), unequally_directed_lines(436 ^ [], reverse_line(436 ^ [])), 234 : -(unequally_directed_lines(436 ^ [], reverse_line(435 ^ []))), 240 : -(unequally_directed_lines(reverse_line(436 ^ []), reverse_line(reverse_line(435 ^ []))))],extension(224 ^ 8,bind([[_75664, _75666, _75668], [reverse_line(435 ^ []), reverse_line(436 ^ []), 436 ^ []]]))).
% 2.77/3.44 ncf('1.1.1.2.1.2.2.1',plain,[-(unequally_directed_lines(436 ^ [], reverse_line(436 ^ [])))],lemmata('[1, 1].x')).
% 2.77/3.44 ncf('1.1.1.2.1.2.2.2',plain,[unequally_directed_lines(436 ^ [], reverse_line(435 ^ []))],reduction('1.1')).
% 2.77/3.44 ncf('1.1.1.2.1.2.2.3',plain,[unequally_directed_lines(reverse_line(436 ^ []), reverse_line(reverse_line(435 ^ [])))],reduction('1.1.1.2')).
% 2.77/3.44 ncf('1.1.1.2.1.3',plain,[unequally_directed_lines(435 ^ [], reverse_line(reverse_line(435 ^ []))), unequally_directed_lines(435 ^ [], reverse_line(reverse_line(reverse_line(435 ^ [])))), -(left_convergent_lines(435 ^ [], reverse_line(reverse_line(435 ^ [])))), -(left_convergent_lines(435 ^ [], reverse_line(reverse_line(reverse_line(435 ^ [])))))],extension(248 ^ 9,bind([[_76450, _76452], [reverse_line(reverse_line(435 ^ [])), 435 ^ []]]))).
% 2.77/3.44 ncf('1.1.1.2.1.3.1',plain,[-(unequally_directed_lines(435 ^ [], reverse_line(reverse_line(reverse_line(435 ^ [])))))],extension(236 ^ 10)).
% 2.77/3.44 ncf('1.1.1.2.1.3.2',plain,[left_convergent_lines(435 ^ [], reverse_line(reverse_line(435 ^ [])))],extension(266 ^ 10,bind([[_77015, _77017], [reverse_line(reverse_line(435 ^ [])), 435 ^ []]]))).
% 2.77/3.44 ncf('1.1.1.2.1.3.3',plain,[left_convergent_lines(435 ^ [], reverse_line(reverse_line(reverse_line(435 ^ []))))],extension(266 ^ 10,bind([[_77015, _77017], [reverse_line(reverse_line(reverse_line(435 ^ []))), 435 ^ []]]))).
% 2.77/3.44 ncf('1.1.1.2.2',plain,[unequally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ [])), equally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ []))],extension(38 ^ 8,bind([[_69624, _69626], [reverse_line(436 ^ []), reverse_line(436 ^ [])]]))).
% 2.77/3.44 ncf('1.1.1.2.2.1',plain,[-(equally_directed_lines(reverse_line(436 ^ []), reverse_line(436 ^ [])))],extension(212 ^ 9,bind([[_75219], [reverse_line(436 ^ [])]]))).
% 2.77/3.44 ncf('1.1.1.2.3',plain,[unequally_directed_lines(reverse_line(435 ^ []), reverse_line(436 ^ [])), unequally_directed_lines(reverse_line(435 ^ []), reverse_line(reverse_line(436 ^ []))), -(left_convergent_lines(reverse_line(435 ^ []), reverse_line(436 ^ []))), -(left_convergent_lines(reverse_line(435 ^ []), reverse_line(reverse_line(436 ^ []))))],extension(248 ^ 8,bind([[_76450, _76452], [reverse_line(436 ^ []), reverse_line(435 ^ [])]]))).
% 2.77/3.44 ncf('1.1.1.2.3.1',plain,[-(unequally_directed_lines(reverse_line(435 ^ []), reverse_line(reverse_line(436 ^ []))))],extension(240 ^ 9)).
% 2.77/3.44 ncf('1.1.1.2.3.2',plain,[left_convergent_lines(reverse_line(435 ^ []), reverse_line(436 ^ []))],extension(266 ^ 9,bind([[_77015, _77017], [reverse_line(436 ^ []), reverse_line(435 ^ [])]]))).
% 2.77/3.44 ncf('1.1.1.2.3.3',plain,[left_convergent_lines(reverse_line(435 ^ []), reverse_line(reverse_line(436 ^ [])))],extension(266 ^ 9,bind([[_77015, _77017], [reverse_line(reverse_line(436 ^ [])), reverse_line(435 ^ [])]]))).
% 2.77/3.44 ncf('1.2',plain,[-(unequally_directed_opposite_lines(435 ^ [], 436 ^ [])), unequally_directed_lines(435 ^ [], reverse_line(436 ^ []))],extension(8 ^ 3,bind([[_68557, _68559], [436 ^ [], 435 ^ []]]))).
% 2.77/3.44 ncf('1.2.1',plain,[-(unequally_directed_lines(435 ^ [], reverse_line(436 ^ []))), unequally_directed_lines(435 ^ [], reverse_line(435 ^ [])), -(unequally_directed_lines(reverse_line(435 ^ []), reverse_line(436 ^ [])))],extension(214 ^ 4,bind([[_75340, _75342, _75344], [reverse_line(436 ^ []), reverse_line(435 ^ []), 435 ^ []]]))).
% 2.77/3.44 ncf('1.2.1.1',plain,[-(unequally_directed_lines(435 ^ [], reverse_line(435 ^ []))), unequally_directed_lines(435 ^ [], reverse_line(435 ^ [])), -(unequally_directed_lines(reverse_line(435 ^ []), reverse_line(435 ^ [])))],extension(214 ^ 5,bind([[_75340, _75342, _75344], [reverse_line(435 ^ []), reverse_line(435 ^ []), 435 ^ []]]))).
% 2.77/3.44 ncf('1.2.1.1.1',plain,[-(unequally_directed_lines(435 ^ [], reverse_line(435 ^ []))), unequally_directed_lines(435 ^ [], reverse_line(435 ^ [])), -(unequally_directed_lines(reverse_line(435 ^ []), reverse_line(435 ^ [])))],extension(214 ^ 6,bind([[_75340, _75342, _75344], [reverse_line(435 ^ []), reverse_line(435 ^ []), 435 ^ []]]))).
% 2.77/3.44 ncf('1.2.1.1.1.1',plain,[-(unequally_directed_lines(435 ^ [], reverse_line(435 ^ []))), unequally_directed_lines(435 ^ [], 435 ^ []), -(unequally_directed_lines(435 ^ [], reverse_line(435 ^ [])))],extension(214 ^ 7,bind([[_75340, _75342, _75344], [reverse_line(435 ^ []), 435 ^ [], 435 ^ []]]))).
% 2.77/3.44 ncf('1.2.1.1.1.1.1',plain,[-(unequally_directed_lines(435 ^ [], 435 ^ [])), -(unequally_directed_lines(435 ^ [], reverse_line(435 ^ [])))],extension(242 ^ 8,bind([[_76235, _76237], [435 ^ [], 435 ^ []]]))).
% 2.77/3.44 ncf('1.2.1.1.1.1.1.1',plain,[unequally_directed_lines(435 ^ [], reverse_line(435 ^ []))],reduction('1.2.1.1.1')).
% 2.77/3.44 ncf('1.2.1.1.1.1.2',plain,[unequally_directed_lines(435 ^ [], reverse_line(435 ^ []))],reduction('1.2.1.1.1')).
% 2.77/3.44 ncf('1.2.1.1.1.2',plain,[unequally_directed_lines(reverse_line(435 ^ []), reverse_line(435 ^ [])), equally_directed_lines(reverse_line(435 ^ []), reverse_line(435 ^ []))],extension(38 ^ 7,bind([[_69624, _69626], [reverse_line(435 ^ []), reverse_line(435 ^ [])]]))).
% 2.77/3.44 ncf('1.2.1.1.1.2.1',plain,[-(equally_directed_lines(reverse_line(435 ^ []), reverse_line(435 ^ [])))],extension(212 ^ 8,bind([[_75219], [reverse_line(435 ^ [])]]))).
% 2.77/3.44 ncf('1.2.1.1.2',plain,[unequally_directed_lines(reverse_line(435 ^ []), reverse_line(435 ^ [])), equally_directed_lines(reverse_line(435 ^ []), reverse_line(435 ^ []))],extension(38 ^ 6,bind([[_69624, _69626], [reverse_line(435 ^ []), reverse_line(435 ^ [])]]))).
% 2.77/3.44 ncf('1.2.1.1.2.1',plain,[-(equally_directed_lines(reverse_line(435 ^ []), reverse_line(435 ^ [])))],extension(212 ^ 7,bind([[_75219], [reverse_line(435 ^ [])]]))).
% 2.77/3.44 ncf('1.2.1.2',plain,[unequally_directed_lines(reverse_line(435 ^ []), reverse_line(436 ^ [])), unequally_directed_lines(reverse_line(435 ^ []), reverse_line(reverse_line(436 ^ []))), 234 : -(unequally_directed_lines(reverse_line(435 ^ []), reverse_line(435 ^ []))), 238 : -(unequally_directed_lines(reverse_line(436 ^ []), reverse_line(435 ^ [])))],extension(224 ^ 5,bind([[_75664, _75666, _75668], [reverse_line(435 ^ []), reverse_line(436 ^ []), reverse_line(435 ^ [])]]))).
% 2.77/3.44 ncf('1.2.1.2.1',plain,[-(unequally_directed_lines(reverse_line(435 ^ []), reverse_line(reverse_line(436 ^ [])))), unequally_directed_lines(436 ^ [], reverse_line(435 ^ [])), unequally_directed_lines(436 ^ [], reverse_line(reverse_line(435 ^ []))), 234 : -(unequally_directed_lines(436 ^ [], reverse_line(reverse_line(436 ^ []))))],extension(224 ^ 6,bind([[_75664, _75666, _75668], [reverse_line(reverse_line(436 ^ [])), reverse_line(435 ^ []), 436 ^ []]]))).
% 2.77/3.44 ncf('1.2.1.2.1.1',plain,[-(unequally_directed_lines(436 ^ [], reverse_line(435 ^ []))), unequally_directed_opposite_lines(436 ^ [], 435 ^ [])],extension(2 ^ 7,bind([[_68391, _68393], [435 ^ [], 436 ^ []]]))).
% 2.77/3.44 ncf('1.2.1.2.1.1.1',plain,[-(unequally_directed_opposite_lines(436 ^ [], 435 ^ []))],extension(444 ^ 8)).
% 2.77/3.44 ncf('1.2.1.2.1.2',plain,[-(unequally_directed_lines(436 ^ [], reverse_line(reverse_line(435 ^ [])))), unequally_directed_lines(435 ^ [], 436 ^ []), -(unequally_directed_lines(435 ^ [], reverse_line(reverse_line(435 ^ []))))],extension(214 ^ 7,bind([[_75340, _75342, _75344], [reverse_line(reverse_line(435 ^ [])), 436 ^ [], 435 ^ []]]))).
% 2.77/3.44 ncf('1.2.1.2.1.2.1',plain,[-(unequally_directed_lines(435 ^ [], 436 ^ [])), -(unequally_directed_lines(435 ^ [], reverse_line(436 ^ [])))],extension(242 ^ 8,bind([[_76235, _76237], [436 ^ [], 435 ^ []]]))).
% 2.77/3.44 ncf('1.2.1.2.1.2.1.1',plain,[unequally_directed_lines(435 ^ [], reverse_line(436 ^ []))],reduction('1.2')).
% 2.77/3.44 ncf('1.2.1.2.1.2.2',plain,[unequally_directed_lines(435 ^ [], reverse_line(reverse_line(435 ^ []))), unequally_directed_lines(435 ^ [], reverse_line(435 ^ [])), 234 : -(unequally_directed_lines(435 ^ [], reverse_line(436 ^ []))), 240 : -(unequally_directed_lines(reverse_line(435 ^ []), reverse_line(reverse_line(436 ^ []))))],extension(224 ^ 8,bind([[_75664, _75666, _75668], [reverse_line(436 ^ []), reverse_line(435 ^ []), 435 ^ []]]))).
% 2.77/3.44 ncf('1.2.1.2.1.2.2.1',plain,[-(unequally_directed_lines(435 ^ [], reverse_line(435 ^ [])))],lemmata('[2, 1].x')).
% 2.77/3.44 ncf('1.2.1.2.1.2.2.2',plain,[unequally_directed_lines(435 ^ [], reverse_line(436 ^ []))],reduction('1.2')).
% 2.77/3.44 ncf('1.2.1.2.1.2.2.3',plain,[unequally_directed_lines(reverse_line(435 ^ []), reverse_line(reverse_line(436 ^ [])))],reduction('1.2.1.2')).
% 2.77/3.44 ncf('1.2.1.2.1.3',plain,[unequally_directed_lines(436 ^ [], reverse_line(reverse_line(436 ^ []))), unequally_directed_lines(436 ^ [], reverse_line(reverse_line(reverse_line(436 ^ [])))), -(left_convergent_lines(436 ^ [], reverse_line(reverse_line(436 ^ [])))), -(left_convergent_lines(436 ^ [], reverse_line(reverse_line(reverse_line(436 ^ [])))))],extension(248 ^ 9,bind([[_76450, _76452], [reverse_line(reverse_line(436 ^ [])), 436 ^ []]]))).
% 2.77/3.44 ncf('1.2.1.2.1.3.1',plain,[-(unequally_directed_lines(436 ^ [], reverse_line(reverse_line(reverse_line(436 ^ [])))))],extension(236 ^ 10)).
% 2.77/3.44 ncf('1.2.1.2.1.3.2',plain,[left_convergent_lines(436 ^ [], reverse_line(reverse_line(436 ^ [])))],extension(266 ^ 10,bind([[_77015, _77017], [reverse_line(reverse_line(436 ^ [])), 436 ^ []]]))).
% 2.77/3.44 ncf('1.2.1.2.1.3.3',plain,[left_convergent_lines(436 ^ [], reverse_line(reverse_line(reverse_line(436 ^ []))))],extension(266 ^ 10,bind([[_77015, _77017], [reverse_line(reverse_line(reverse_line(436 ^ []))), 436 ^ []]]))).
% 2.77/3.44 ncf('1.2.1.2.2',plain,[unequally_directed_lines(reverse_line(435 ^ []), reverse_line(435 ^ [])), equally_directed_lines(reverse_line(435 ^ []), reverse_line(435 ^ []))],extension(38 ^ 8,bind([[_69624, _69626], [reverse_line(435 ^ []), reverse_line(435 ^ [])]]))).
% 2.77/3.44 ncf('1.2.1.2.2.1',plain,[-(equally_directed_lines(reverse_line(435 ^ []), reverse_line(435 ^ [])))],extension(212 ^ 9,bind([[_75219], [reverse_line(435 ^ [])]]))).
% 2.77/3.44 ncf('1.2.1.2.3',plain,[unequally_directed_lines(reverse_line(436 ^ []), reverse_line(435 ^ [])), unequally_directed_lines(reverse_line(436 ^ []), reverse_line(reverse_line(435 ^ []))), -(left_convergent_lines(reverse_line(436 ^ []), reverse_line(435 ^ []))), -(left_convergent_lines(reverse_line(436 ^ []), reverse_line(reverse_line(435 ^ []))))],extension(248 ^ 8,bind([[_76450, _76452], [reverse_line(435 ^ []), reverse_line(436 ^ [])]]))).
% 2.77/3.44 ncf('1.2.1.2.3.1',plain,[-(unequally_directed_lines(reverse_line(436 ^ []), reverse_line(reverse_line(435 ^ []))))],extension(240 ^ 9)).
% 2.77/3.44 ncf('1.2.1.2.3.2',plain,[left_convergent_lines(reverse_line(436 ^ []), reverse_line(435 ^ []))],extension(266 ^ 9,bind([[_77015, _77017], [reverse_line(435 ^ []), reverse_line(436 ^ [])]]))).
% 2.77/3.44 ncf('1.2.1.2.3.3',plain,[left_convergent_lines(reverse_line(436 ^ []), reverse_line(reverse_line(435 ^ [])))],extension(266 ^ 9,bind([[_77015, _77017], [reverse_line(reverse_line(435 ^ [])), reverse_line(436 ^ [])]]))).
% 2.77/3.44 %-----------------------------------------------------
% 2.77/3.44 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------