%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO231+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n009.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:18 EDT 2023
% Result : Theorem 13.76s 13.79s
% Output : Proof 13.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO231+3 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n009.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Fri May 19 03:59:02 EDT 2023
% 0.13/0.33 % CPUTime :
% 13.76/13.79
% 13.76/13.79 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 13.76/13.79 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.76/13.79 %-----------------------------------------------------
% 13.76/13.79 ncf(matrix, plain, [(439 ^ _66539) ^ [] : [-(equally_directed_opposite_lines(435 ^ [], 436 ^ []))], (441 ^ _66539) ^ [] : [-(equally_directed_lines(435 ^ [], 437 ^ []))], (443 ^ _66539) ^ [] : [equally_directed_opposite_lines(436 ^ [], 437 ^ [])], (2 ^ _66539) ^ [_66681, _66683] : [unequally_directed_opposite_lines(_66683, _66681), -(unequally_directed_lines(_66683, reverse_line(_66681)))], (8 ^ _66539) ^ [_66847, _66849] : [unequally_directed_lines(_66849, reverse_line(_66847)), -(unequally_directed_opposite_lines(_66849, _66847))], (14 ^ _66539) ^ [_67092, _67094] : [right_apart_point(_67094, _67092), -(left_apart_point(_67094, reverse_line(_67092)))], (20 ^ _66539) ^ [_67258, _67260] : [left_apart_point(_67260, reverse_line(_67258)), -(right_apart_point(_67260, _67258))], (26 ^ _66539) ^ [_67503, _67505] : [right_convergent_lines(_67505, _67503), -(left_convergent_lines(_67505, reverse_line(_67503)))], (32 ^ _66539) ^ [_67669, _67671] : [left_convergent_lines(_67671, reverse_line(_67669)), -(right_convergent_lines(_67671, _67669))], (38 ^ _66539) ^ [_67914, _67916] : [equally_directed_lines(_67916, _67914), unequally_directed_lines(_67916, _67914)], (44 ^ _66539) ^ [_68077, _68079] : [-(unequally_directed_lines(_68079, _68077)), -(equally_directed_lines(_68079, _68077))], (50 ^ _66539) ^ [_68321, _68323] : [equally_directed_opposite_lines(_68323, _68321), unequally_directed_opposite_lines(_68323, _68321)], (56 ^ _66539) ^ [_68484, _68486] : [-(unequally_directed_opposite_lines(_68486, _68484)), -(equally_directed_opposite_lines(_68486, _68484))], (72 ^ _66539) ^ [_68980, _68982] : [73 ^ _66539 : [(74 ^ _66539) ^ [] : [left_apart_point(_68982, _68980)], (76 ^ _66539) ^ [] : [right_apart_point(_68982, _68980)]], -(apart_point_and_line(_68982, _68980))], (62 ^ _66539) ^ [_68728, _68730] : [apart_point_and_line(_68730, _68728), -(left_apart_point(_68730, _68728)), -(right_apart_point(_68730, _68728))], (80 ^ _66539) ^ [_69295, _69297] : [convergent_lines(_69297, _69295), 83 ^ _66539 : [(84 ^ _66539) ^ [] : [-(unequally_directed_lines(_69297, _69295))], (86 ^ _66539) ^ [] : [-(unequally_directed_opposite_lines(_69297, _69295))]]], (88 ^ _66539) ^ [_69532, _69534] : [-(convergent_lines(_69534, _69532)), unequally_directed_lines(_69534, _69532), unequally_directed_opposite_lines(_69534, _69532)], (98 ^ _66539) ^ [_69876, _69878, _69880] : [divides_points(_69876, _69880, _69878), 103 ^ _66539 : [(104 ^ _66539) ^ [] : [-(left_apart_point(_69880, _69876))], (106 ^ _66539) ^ [] : [-(right_apart_point(_69878, _69876))]], 107 ^ _66539 : [(108 ^ _66539) ^ [] : [-(right_apart_point(_69880, _69876))], (110 ^ _66539) ^ [] : [-(left_apart_point(_69878, _69876))]]], (112 ^ _66539) ^ [_70294, _70296, _70298] : [-(divides_points(_70294, _70298, _70296)), 113 ^ _66539 : [(114 ^ _66539) ^ [] : [left_apart_point(_70298, _70294), right_apart_point(_70296, _70294)], (120 ^ _66539) ^ [] : [right_apart_point(_70298, _70294), left_apart_point(_70296, _70294)]]], (128 ^ _66539) ^ [_70819, _70821, _70823] : [before_on_line(_70823, _70821, _70819), 131 ^ _66539 : [(132 ^ _66539) ^ [] : [-(distinct_points(_70821, _70819))], (134 ^ _66539) ^ [] : [-(incident_point_and_line(_70821, _70823))], (136 ^ _66539) ^ [] : [-(incident_point_and_line(_70819, _70823))], (138 ^ _66539) ^ [] : [-(equally_directed_lines(_70823, line_connecting(_70821, _70819)))]]], (140 ^ _66539) ^ [_71224, _71226, _71228] : [-(before_on_line(_71228, _71226, _71224)), distinct_points(_71226, _71224), incident_point_and_line(_71226, _71228), incident_point_and_line(_71224, _71228), equally_directed_lines(_71228, line_connecting(_71226, _71224))], (158 ^ _66539) ^ [_71786, _71788, _71790, _71792] : [between_on_line(_71792, _71790, _71788, _71786), 163 ^ _66539 : [(164 ^ _66539) ^ [] : [-(before_on_line(_71792, _71790, _71788))], (166 ^ _66539) ^ [] : [-(before_on_line(_71792, _71788, _71786))]], 167 ^ _66539 : [(168 ^ _66539) ^ [] : [-(before_on_line(_71792, _71786, _71788))], (170 ^ _66539) ^ [] : [-(before_on_line(_71792, _71788, _71790))]]], (172 ^ _66539) ^ [_72228, _72230, _72232, _72234] : [-(between_on_line(_72234, _72232, _72230, _72228)), 173 ^ _66539 : [(174 ^ _66539) ^ [] : [before_on_line(_72234, _72232, _72230), before_on_line(_72234, _72230, _72228)], (180 ^ _66539) ^ [] : [before_on_line(_72234, _72228, _72230), before_on_line(_72234, _72230, _72232)]]], (188 ^ _66539) ^ [_72706] : [distinct_points(_72706, _72706)], (190 ^ _66539) ^ [_72827, _72829, _72831] : [distinct_points(_72831, _72829), -(distinct_points(_72831, _72827)), -(distinct_points(_72829, _72827))], (200 ^ _66539) ^ [_73107] : [distinct_lines(_73107, _73107)], (202 ^ _66539) ^ [_73228, _73230, _73232] : [distinct_lines(_73232, _73230), -(distinct_lines(_73232, _73228)), -(distinct_lines(_73230, _73228))], (212 ^ _66539) ^ [_73509] : [-(equally_directed_lines(_73509, _73509))], (214 ^ _66539) ^ [_73630, _73632, _73634] : [unequally_directed_lines(_73634, _73632), -(unequally_directed_lines(_73634, _73630)), -(unequally_directed_lines(_73632, _73630))], (224 ^ _66539) ^ [_73954, _73956, _73958] : [unequally_directed_lines(_73958, _73956), unequally_directed_lines(_73958, reverse_line(_73956)), 233 ^ _66539 : [(234 ^ _66539) ^ [] : [-(unequally_directed_lines(_73958, _73954))], (236 ^ _66539) ^ [] : [-(unequally_directed_lines(_73958, reverse_line(_73954)))]], 237 ^ _66539 : [(238 ^ _66539) ^ [] : [-(unequally_directed_lines(_73956, _73954))], (240 ^ _66539) ^ [] : [-(unequally_directed_lines(_73956, reverse_line(_73954)))]]], (242 ^ _66539) ^ [_74525, _74527] : [-(unequally_directed_lines(_74527, _74525)), -(unequally_directed_lines(_74527, reverse_line(_74525)))], (248 ^ _66539) ^ [_74740, _74742] : [unequally_directed_lines(_74742, _74740), unequally_directed_lines(_74742, reverse_line(_74740)), -(left_convergent_lines(_74742, _74740)), -(left_convergent_lines(_74742, reverse_line(_74740)))], (262 ^ _66539) ^ [_75143, _75145] : [left_apart_point(_75145, _75143)], (264 ^ _66539) ^ [_75188, _75190] : [left_apart_point(_75190, reverse_line(_75188))], (266 ^ _66539) ^ [_75305, _75307] : [left_convergent_lines(_75307, _75305)], (268 ^ _66539) ^ [_75350, _75352] : [left_convergent_lines(_75352, reverse_line(_75350))], (270 ^ _66539) ^ [_75463, _75465] : [-(line(line_connecting(_75465, _75463))), point(_75465), point(_75463), distinct_points(_75465, _75463)], (284 ^ _66539) ^ [_75851, _75853] : [-(point(intersection_point(_75853, _75851))), line(_75853), line(_75851), unequally_directed_lines(_75853, _75851), unequally_directed_lines(_75853, reverse_line(_75851))], (302 ^ _66539) ^ [_76332, _76334] : [-(line(parallel_through_point(_76334, _76332))), point(_76332), line(_76334)], (312 ^ _66539) ^ [_76617] : [line(_76617), -(line(reverse_line(_76617)))], (318 ^ _66539) ^ [_76821, _76823] : [distinct_points(_76823, _76821), 321 ^ _66539 : [(322 ^ _66539) ^ [] : [apart_point_and_line(_76823, line_connecting(_76823, _76821))], (324 ^ _66539) ^ [] : [apart_point_and_line(_76821, line_connecting(_76823, _76821))]]], (326 ^ _66539) ^ [_77120, _77122] : [333 ^ _66539 : [(334 ^ _66539) ^ [] : [apart_point_and_line(intersection_point(_77122, _77120), _77122)], (336 ^ _66539) ^ [] : [apart_point_and_line(intersection_point(_77122, _77120), _77120)]], unequally_directed_lines(_77122, _77120), unequally_directed_lines(_77122, reverse_line(_77120))], (338 ^ _66539) ^ [_77496, _77498] : [apart_point_and_line(_77498, parallel_through_point(_77496, _77498))], (340 ^ _66539) ^ [_77578] : [distinct_lines(_77578, reverse_line(_77578))], (342 ^ _66539) ^ [_77687, _77689] : [distinct_points(_77689, _77687), -(equally_directed_lines(line_connecting(_77689, _77687), reverse_line(line_connecting(_77687, _77689))))], (348 ^ _66539) ^ [_77898, _77900] : [-(equally_directed_lines(parallel_through_point(_77898, _77900), _77898))], (350 ^ _66539) ^ [_78038, _78040, _78042, _78044] : [distinct_points(_78044, _78042), distinct_lines(_78040, _78038), -(left_apart_point(_78044, _78040)), -(left_apart_point(_78042, _78040)), -(left_apart_point(_78044, _78038)), -(left_apart_point(_78042, _78038)), -(left_apart_point(_78044, reverse_line(_78040))), -(left_apart_point(_78042, reverse_line(_78040))), -(left_apart_point(_78044, reverse_line(_78038))), -(left_apart_point(_78042, reverse_line(_78038)))], (388 ^ _66539) ^ [_79075, _79077, _79079] : [distinct_points(_79079, _79077), left_apart_point(_79079, _79075), -(left_apart_point(_79077, _79075)), -(left_convergent_lines(line_connecting(_79079, _79077), _79075))], (402 ^ _66539) ^ [_79500, _79502, _79504] : [left_apart_point(_79504, _79500), -(distinct_points(_79504, _79502)), -(left_apart_point(_79502, _79500))], (426 ^ _66539) ^ [_80227, _80229, _80231] : [left_convergent_lines(_80231, _80229), -(unequally_directed_lines(_80229, _80227)), -(left_convergent_lines(_80231, _80227))], (412 ^ _66539) ^ [_79824, _79826, _79828] : [left_apart_point(_79828, _79826), unequally_directed_lines(_79826, _79824), -(distinct_lines(_79826, _79824)), -(left_apart_point(_79828, reverse_line(_79824)))]], input).
% 13.76/13.79 ncf('1',plain,[equally_directed_lines(435 ^ [], 437 ^ []), unequally_directed_lines(435 ^ [], 437 ^ [])],start(38 ^ 0,bind([[_67914, _67916], [437 ^ [], 435 ^ []]]))).
% 13.76/13.79 ncf('1.1',plain,[-(equally_directed_lines(435 ^ [], 437 ^ []))],extension(441 ^ 1)).
% 13.76/13.79 ncf('1.2',plain,[-(unequally_directed_lines(435 ^ [], 437 ^ [])), unequally_directed_lines(reverse_line(437 ^ []), 435 ^ []), -(unequally_directed_lines(reverse_line(437 ^ []), 437 ^ []))],extension(214 ^ 1,bind([[_73630, _73632, _73634], [437 ^ [], 435 ^ [], reverse_line(437 ^ [])]]))).
% 13.76/13.79 ncf('1.2.1',plain,[-(unequally_directed_lines(reverse_line(437 ^ []), 435 ^ [])), unequally_directed_lines(436 ^ [], reverse_line(437 ^ [])), -(unequally_directed_lines(436 ^ [], 435 ^ []))],extension(214 ^ 2,bind([[_73630, _73632, _73634], [435 ^ [], reverse_line(437 ^ []), 436 ^ []]]))).
% 13.76/13.79 ncf('1.2.1.1',plain,[-(unequally_directed_lines(436 ^ [], reverse_line(437 ^ []))), unequally_directed_opposite_lines(436 ^ [], 437 ^ [])],extension(2 ^ 3,bind([[_66681, _66683], [437 ^ [], 436 ^ []]]))).
% 13.76/13.79 ncf('1.2.1.1.1',plain,[-(unequally_directed_opposite_lines(436 ^ [], 437 ^ [])), -(equally_directed_opposite_lines(436 ^ [], 437 ^ []))],extension(56 ^ 4,bind([[_68484, _68486], [437 ^ [], 436 ^ []]]))).
% 13.76/13.79 ncf('1.2.1.1.1.1',plain,[equally_directed_opposite_lines(436 ^ [], 437 ^ [])],extension(443 ^ 5)).
% 13.76/13.79 ncf('1.2.1.2',plain,[unequally_directed_lines(436 ^ [], 435 ^ []), -(unequally_directed_lines(436 ^ [], 436 ^ [])), -(unequally_directed_lines(435 ^ [], 436 ^ []))],extension(214 ^ 3,bind([[_73630, _73632, _73634], [436 ^ [], 435 ^ [], 436 ^ []]]))).
% 13.76/13.79 ncf('1.2.1.2.1',plain,[unequally_directed_lines(436 ^ [], 436 ^ []), equally_directed_lines(436 ^ [], 436 ^ [])],extension(38 ^ 4,bind([[_67914, _67916], [436 ^ [], 436 ^ []]]))).
% 13.76/13.79 ncf('1.2.1.2.1.1',plain,[-(equally_directed_lines(436 ^ [], 436 ^ []))],extension(212 ^ 5,bind([[_73509], [436 ^ []]]))).
% 13.76/13.79 ncf('1.2.1.2.2',plain,[unequally_directed_lines(435 ^ [], 436 ^ []), -(unequally_directed_lines(435 ^ [], 437 ^ [])), -(unequally_directed_lines(436 ^ [], 437 ^ []))],extension(214 ^ 4,bind([[_73630, _73632, _73634], [437 ^ [], 436 ^ [], 435 ^ []]]))).
% 13.76/13.79 ncf('1.2.1.2.2.1',plain,[unequally_directed_lines(435 ^ [], 437 ^ [])],reduction('1')).
% 13.76/13.79 ncf('1.2.1.2.2.2',plain,[unequally_directed_lines(436 ^ [], 437 ^ []), -(unequally_directed_lines(436 ^ [], 436 ^ [])), -(unequally_directed_lines(437 ^ [], 436 ^ []))],extension(214 ^ 5,bind([[_73630, _73632, _73634], [436 ^ [], 437 ^ [], 436 ^ []]]))).
% 13.76/13.79 ncf('1.2.1.2.2.2.1',plain,[unequally_directed_lines(436 ^ [], 436 ^ []), equally_directed_lines(436 ^ [], 436 ^ [])],extension(38 ^ 6,bind([[_67914, _67916], [436 ^ [], 436 ^ []]]))).
% 13.76/13.79 ncf('1.2.1.2.2.2.1.1',plain,[-(equally_directed_lines(436 ^ [], 436 ^ []))],extension(212 ^ 7,bind([[_73509], [436 ^ []]]))).
% 13.76/13.79 ncf('1.2.1.2.2.2.2',plain,[unequally_directed_lines(437 ^ [], 436 ^ []), unequally_directed_lines(437 ^ [], reverse_line(436 ^ [])), -(left_convergent_lines(437 ^ [], 436 ^ [])), -(left_convergent_lines(437 ^ [], reverse_line(436 ^ [])))],extension(248 ^ 6,bind([[_74740, _74742], [436 ^ [], 437 ^ []]]))).
% 13.76/13.79 ncf('1.2.1.2.2.2.2.1',plain,[-(unequally_directed_lines(437 ^ [], reverse_line(436 ^ []))), unequally_directed_lines(436 ^ [], 437 ^ []), unequally_directed_lines(436 ^ [], reverse_line(437 ^ [])), 234 : -(unequally_directed_lines(436 ^ [], 436 ^ []))],extension(224 ^ 7,bind([[_73954, _73956, _73958], [436 ^ [], 437 ^ [], 436 ^ []]]))).
% 13.76/13.79 ncf('1.2.1.2.2.2.2.1.1',plain,[-(unequally_directed_lines(436 ^ [], 437 ^ []))],reduction('1.2.1.2.2')).
% 13.76/13.79 ncf('1.2.1.2.2.2.2.1.2',plain,[-(unequally_directed_lines(436 ^ [], reverse_line(437 ^ [])))],lemmata('[2, 1].x')).
% 13.76/13.79 ncf('1.2.1.2.2.2.2.1.3',plain,[unequally_directed_lines(436 ^ [], 436 ^ [])],lemmata('[2, 2, 1, 2, 1].x')).
% 13.76/13.79 ncf('1.2.1.2.2.2.2.2',plain,[left_convergent_lines(437 ^ [], 436 ^ [])],extension(266 ^ 7,bind([[_75305, _75307], [436 ^ [], 437 ^ []]]))).
% 13.76/13.79 ncf('1.2.1.2.2.2.2.3',plain,[left_convergent_lines(437 ^ [], reverse_line(436 ^ []))],extension(266 ^ 7,bind([[_75305, _75307], [reverse_line(436 ^ []), 437 ^ []]]))).
% 13.76/13.79 ncf('1.2.2',plain,[unequally_directed_lines(reverse_line(437 ^ []), 437 ^ []), unequally_directed_lines(reverse_line(437 ^ []), reverse_line(437 ^ [])), 234 : -(unequally_directed_lines(reverse_line(437 ^ []), reverse_line(reverse_line(437 ^ [])))), 238 : -(unequally_directed_lines(437 ^ [], reverse_line(reverse_line(437 ^ []))))],extension(224 ^ 2,bind([[_73954, _73956, _73958], [reverse_line(reverse_line(437 ^ [])), 437 ^ [], reverse_line(437 ^ [])]]))).
% 13.76/13.79 ncf('1.2.2.1',plain,[-(unequally_directed_lines(reverse_line(437 ^ []), reverse_line(437 ^ []))), unequally_directed_lines(436 ^ [], reverse_line(437 ^ [])), unequally_directed_lines(436 ^ [], reverse_line(reverse_line(437 ^ []))), 234 : -(unequally_directed_lines(436 ^ [], reverse_line(437 ^ [])))],extension(224 ^ 3,bind([[_73954, _73956, _73958], [reverse_line(437 ^ []), reverse_line(437 ^ []), 436 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.1.1',plain,[-(unequally_directed_lines(436 ^ [], reverse_line(437 ^ []))), unequally_directed_opposite_lines(436 ^ [], 437 ^ [])],extension(2 ^ 4,bind([[_66681, _66683], [437 ^ [], 436 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.1.1.1',plain,[-(unequally_directed_opposite_lines(436 ^ [], 437 ^ [])), -(equally_directed_opposite_lines(436 ^ [], 437 ^ []))],extension(56 ^ 5,bind([[_68484, _68486], [437 ^ [], 436 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.1.1.1.1',plain,[equally_directed_opposite_lines(436 ^ [], 437 ^ [])],extension(443 ^ 6)).
% 13.76/13.79 ncf('1.2.2.1.2',plain,[-(unequally_directed_lines(436 ^ [], reverse_line(reverse_line(437 ^ [])))), unequally_directed_lines(435 ^ [], 436 ^ []), -(unequally_directed_lines(435 ^ [], reverse_line(reverse_line(437 ^ []))))],extension(214 ^ 4,bind([[_73630, _73632, _73634], [reverse_line(reverse_line(437 ^ [])), 436 ^ [], 435 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.1.2.1',plain,[-(unequally_directed_lines(435 ^ [], 436 ^ [])), -(unequally_directed_lines(435 ^ [], reverse_line(436 ^ [])))],extension(242 ^ 5,bind([[_74525, _74527], [436 ^ [], 435 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.1.2.1.1',plain,[unequally_directed_lines(435 ^ [], reverse_line(436 ^ [])), -(unequally_directed_opposite_lines(435 ^ [], 436 ^ []))],extension(8 ^ 6,bind([[_66847, _66849], [436 ^ [], 435 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.1.2.1.1.1',plain,[unequally_directed_opposite_lines(435 ^ [], 436 ^ []), equally_directed_opposite_lines(435 ^ [], 436 ^ [])],extension(50 ^ 7,bind([[_68321, _68323], [436 ^ [], 435 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.1.2.1.1.1.1',plain,[-(equally_directed_opposite_lines(435 ^ [], 436 ^ []))],extension(439 ^ 8)).
% 13.76/13.79 ncf('1.2.2.1.2.2',plain,[unequally_directed_lines(435 ^ [], reverse_line(reverse_line(437 ^ []))), unequally_directed_lines(435 ^ [], reverse_line(437 ^ [])), 234 : -(unequally_directed_lines(435 ^ [], 437 ^ [])), 240 : -(unequally_directed_lines(reverse_line(437 ^ []), reverse_line(437 ^ [])))],extension(224 ^ 5,bind([[_73954, _73956, _73958], [437 ^ [], reverse_line(437 ^ []), 435 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.1.2.2.1',plain,[-(unequally_directed_lines(435 ^ [], reverse_line(437 ^ []))), -(unequally_directed_lines(435 ^ [], 437 ^ []))],extension(242 ^ 6,bind([[_74525, _74527], [437 ^ [], 435 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.1.2.2.1.1',plain,[unequally_directed_lines(435 ^ [], 437 ^ [])],reduction('1')).
% 13.76/13.79 ncf('1.2.2.1.2.2.2',plain,[unequally_directed_lines(435 ^ [], 437 ^ [])],reduction('1')).
% 13.76/13.79 ncf('1.2.2.1.2.2.3',plain,[unequally_directed_lines(reverse_line(437 ^ []), reverse_line(437 ^ []))],reduction('1.2.2')).
% 13.76/13.79 ncf('1.2.2.1.3',plain,[unequally_directed_lines(436 ^ [], reverse_line(437 ^ [])), -(unequally_directed_lines(436 ^ [], 436 ^ [])), -(unequally_directed_lines(reverse_line(437 ^ []), 436 ^ []))],extension(214 ^ 6,bind([[_73630, _73632, _73634], [436 ^ [], reverse_line(437 ^ []), 436 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.1.3.1',plain,[unequally_directed_lines(436 ^ [], 436 ^ []), equally_directed_lines(436 ^ [], 436 ^ [])],extension(38 ^ 7,bind([[_67914, _67916], [436 ^ [], 436 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.1.3.1.1',plain,[-(equally_directed_lines(436 ^ [], 436 ^ []))],extension(212 ^ 8,bind([[_73509], [436 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.1.3.2',plain,[unequally_directed_lines(reverse_line(437 ^ []), 436 ^ []), unequally_directed_lines(reverse_line(437 ^ []), reverse_line(436 ^ [])), 234 : -(unequally_directed_lines(reverse_line(437 ^ []), reverse_line(437 ^ []))), 240 : -(unequally_directed_lines(436 ^ [], reverse_line(reverse_line(437 ^ []))))],extension(224 ^ 7,bind([[_73954, _73956, _73958], [reverse_line(437 ^ []), 436 ^ [], reverse_line(437 ^ [])]]))).
% 13.76/13.79 ncf('1.2.2.1.3.2.1',plain,[-(unequally_directed_lines(reverse_line(437 ^ []), reverse_line(436 ^ []))), unequally_directed_lines(436 ^ [], reverse_line(437 ^ [])), unequally_directed_lines(436 ^ [], reverse_line(reverse_line(437 ^ []))), 234 : -(unequally_directed_lines(436 ^ [], 436 ^ []))],extension(224 ^ 8,bind([[_73954, _73956, _73958], [436 ^ [], reverse_line(437 ^ []), 436 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.1.3.2.1.1',plain,[-(unequally_directed_lines(436 ^ [], reverse_line(437 ^ [])))],reduction('1.2.2.1')).
% 13.76/13.79 ncf('1.2.2.1.3.2.1.2',plain,[-(unequally_directed_lines(436 ^ [], reverse_line(reverse_line(437 ^ []))))],lemmata('[2, 2, 1].x')).
% 13.76/13.79 ncf('1.2.2.1.3.2.1.3',plain,[unequally_directed_lines(436 ^ [], 436 ^ [])],lemmata('[1, 2, 2, 1].x')).
% 13.76/13.79 ncf('1.2.2.1.3.2.2',plain,[unequally_directed_lines(reverse_line(437 ^ []), reverse_line(437 ^ []))],reduction('1.2.2')).
% 13.76/13.79 ncf('1.2.2.1.3.2.3',plain,[unequally_directed_lines(436 ^ [], reverse_line(reverse_line(437 ^ []))), unequally_directed_lines(436 ^ [], reverse_line(437 ^ [])), -(left_convergent_lines(436 ^ [], reverse_line(437 ^ []))), -(left_convergent_lines(436 ^ [], reverse_line(reverse_line(437 ^ []))))],extension(248 ^ 10,bind([[_74740, _74742], [reverse_line(437 ^ []), 436 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.1.3.2.3.1',plain,[-(unequally_directed_lines(436 ^ [], reverse_line(437 ^ [])))],lemmata('[2, 2, 1].x')).
% 13.76/13.79 ncf('1.2.2.1.3.2.3.2',plain,[left_convergent_lines(436 ^ [], reverse_line(437 ^ []))],extension(266 ^ 11,bind([[_75305, _75307], [reverse_line(437 ^ []), 436 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.1.3.2.3.3',plain,[left_convergent_lines(436 ^ [], reverse_line(reverse_line(437 ^ [])))],extension(266 ^ 11,bind([[_75305, _75307], [reverse_line(reverse_line(437 ^ [])), 436 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.2',plain,[unequally_directed_lines(reverse_line(437 ^ []), reverse_line(reverse_line(437 ^ []))), -(unequally_directed_opposite_lines(reverse_line(437 ^ []), reverse_line(437 ^ [])))],extension(8 ^ 5,bind([[_66847, _66849], [reverse_line(437 ^ []), reverse_line(437 ^ [])]]))).
% 13.76/13.79 ncf('1.2.2.2.1',plain,[unequally_directed_opposite_lines(reverse_line(437 ^ []), reverse_line(437 ^ [])), -(convergent_lines(reverse_line(437 ^ []), reverse_line(437 ^ []))), unequally_directed_lines(reverse_line(437 ^ []), reverse_line(437 ^ []))],extension(88 ^ 6,bind([[_69532, _69534], [reverse_line(437 ^ []), reverse_line(437 ^ [])]]))).
% 13.76/13.79 ncf('1.2.2.2.1.1',plain,[convergent_lines(reverse_line(437 ^ []), reverse_line(437 ^ [])), 84 : -(unequally_directed_lines(reverse_line(437 ^ []), reverse_line(437 ^ [])))],extension(80 ^ 7,bind([[_69295, _69297], [reverse_line(437 ^ []), reverse_line(437 ^ [])]]))).
% 13.76/13.79 ncf('1.2.2.2.1.1.1',plain,[unequally_directed_lines(reverse_line(437 ^ []), reverse_line(437 ^ [])), equally_directed_lines(reverse_line(437 ^ []), reverse_line(437 ^ []))],extension(38 ^ 10,bind([[_67914, _67916], [reverse_line(437 ^ []), reverse_line(437 ^ [])]]))).
% 13.76/13.79 ncf('1.2.2.2.1.1.1.1',plain,[-(equally_directed_lines(reverse_line(437 ^ []), reverse_line(437 ^ [])))],extension(212 ^ 11,bind([[_73509], [reverse_line(437 ^ [])]]))).
% 13.76/13.79 ncf('1.2.2.2.1.2',plain,[-(unequally_directed_lines(reverse_line(437 ^ []), reverse_line(437 ^ [])))],lemmata('[2, 1].x')).
% 13.76/13.79 ncf('1.2.2.3',plain,[unequally_directed_lines(437 ^ [], reverse_line(reverse_line(437 ^ []))), -(unequally_directed_opposite_lines(437 ^ [], reverse_line(437 ^ [])))],extension(8 ^ 5,bind([[_66847, _66849], [reverse_line(437 ^ []), 437 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.3.1',plain,[unequally_directed_opposite_lines(437 ^ [], reverse_line(437 ^ [])), -(convergent_lines(437 ^ [], reverse_line(437 ^ []))), unequally_directed_lines(437 ^ [], reverse_line(437 ^ []))],extension(88 ^ 6,bind([[_69532, _69534], [reverse_line(437 ^ []), 437 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.3.1.1',plain,[convergent_lines(437 ^ [], reverse_line(437 ^ [])), 84 : -(unequally_directed_lines(437 ^ [], reverse_line(437 ^ [])))],extension(80 ^ 7,bind([[_69295, _69297], [reverse_line(437 ^ []), 437 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.3.1.1.1',plain,[unequally_directed_lines(437 ^ [], reverse_line(437 ^ [])), unequally_directed_lines(437 ^ [], reverse_line(reverse_line(437 ^ []))), -(left_convergent_lines(437 ^ [], reverse_line(437 ^ []))), -(left_convergent_lines(437 ^ [], reverse_line(reverse_line(437 ^ []))))],extension(248 ^ 10,bind([[_74740, _74742], [reverse_line(437 ^ []), 437 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.3.1.1.1.1',plain,[-(unequally_directed_lines(437 ^ [], reverse_line(reverse_line(437 ^ []))))],reduction('1.2.2')).
% 13.76/13.79 ncf('1.2.2.3.1.1.1.2',plain,[left_convergent_lines(437 ^ [], reverse_line(437 ^ []))],extension(266 ^ 11,bind([[_75305, _75307], [reverse_line(437 ^ []), 437 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.3.1.1.1.3',plain,[left_convergent_lines(437 ^ [], reverse_line(reverse_line(437 ^ [])))],extension(266 ^ 11,bind([[_75305, _75307], [reverse_line(reverse_line(437 ^ [])), 437 ^ []]]))).
% 13.76/13.79 ncf('1.2.2.3.1.2',plain,[-(unequally_directed_lines(437 ^ [], reverse_line(437 ^ []))), unequally_directed_lines(reverse_line(437 ^ []), 437 ^ []), -(unequally_directed_lines(reverse_line(437 ^ []), reverse_line(437 ^ [])))],extension(214 ^ 7,bind([[_73630, _73632, _73634], [reverse_line(437 ^ []), 437 ^ [], reverse_line(437 ^ [])]]))).
% 13.76/13.79 ncf('1.2.2.3.1.2.1',plain,[-(unequally_directed_lines(reverse_line(437 ^ []), 437 ^ []))],reduction('1.2')).
% 13.76/13.79 ncf('1.2.2.3.1.2.2',plain,[unequally_directed_lines(reverse_line(437 ^ []), reverse_line(437 ^ [])), equally_directed_lines(reverse_line(437 ^ []), reverse_line(437 ^ []))],extension(38 ^ 8,bind([[_67914, _67916], [reverse_line(437 ^ []), reverse_line(437 ^ [])]]))).
% 13.76/13.79 ncf('1.2.2.3.1.2.2.1',plain,[-(equally_directed_lines(reverse_line(437 ^ []), reverse_line(437 ^ [])))],extension(212 ^ 9,bind([[_73509], [reverse_line(437 ^ [])]]))).
% 13.76/13.79 %-----------------------------------------------------
% 13.76/13.79 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------