%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO234+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n023.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:19 EDT 2023
% Result : Theorem 0.36s 1.37s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO234+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n023.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri May 19 04:38:29 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.36/1.37
% 0.36/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.36/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 ncf(matrix, plain, [(395 ^ _53513) ^ [] : [-(unequally_directed_lines(391 ^ [], reverse_line(392 ^ [])))], (397 ^ _53513) ^ [] : [unequally_directed_lines(391 ^ [], 393 ^ [])], (399 ^ _53513) ^ [] : [unequally_directed_lines(392 ^ [], reverse_line(393 ^ []))], (12 ^ _53513) ^ [_53911, _53913] : [13 ^ _53513 : [(14 ^ _53513) ^ [] : [left_apart_point(_53913, _53911)], (16 ^ _53513) ^ [] : [left_apart_point(_53913, reverse_line(_53911))]], -(apart_point_and_line(_53913, _53911))], (2 ^ _53513) ^ [_53655, _53657] : [apart_point_and_line(_53657, _53655), -(left_apart_point(_53657, _53655)), -(left_apart_point(_53657, reverse_line(_53655)))], (20 ^ _53513) ^ [_54230, _54232] : [convergent_lines(_54232, _54230), 23 ^ _53513 : [(24 ^ _53513) ^ [] : [-(unequally_directed_lines(_54232, _54230))], (26 ^ _53513) ^ [] : [-(unequally_directed_lines(_54232, reverse_line(_54230)))]]], (28 ^ _53513) ^ [_54471, _54473] : [-(convergent_lines(_54473, _54471)), unequally_directed_lines(_54473, _54471), unequally_directed_lines(_54473, reverse_line(_54471))], (38 ^ _53513) ^ [_54819, _54821, _54823] : [divides_points(_54819, _54823, _54821), 43 ^ _53513 : [(44 ^ _53513) ^ [] : [-(left_apart_point(_54823, _54819))], (46 ^ _53513) ^ [] : [-(left_apart_point(_54821, reverse_line(_54819)))]], 47 ^ _53513 : [(48 ^ _53513) ^ [] : [-(left_apart_point(_54823, reverse_line(_54819)))], (50 ^ _53513) ^ [] : [-(left_apart_point(_54821, _54819))]]], (52 ^ _53513) ^ [_55245, _55247, _55249] : [-(divides_points(_55245, _55249, _55247)), 53 ^ _53513 : [(54 ^ _53513) ^ [] : [left_apart_point(_55249, _55245), left_apart_point(_55247, reverse_line(_55245))], (60 ^ _53513) ^ [] : [left_apart_point(_55249, reverse_line(_55245)), left_apart_point(_55247, _55245)]]], (68 ^ _53513) ^ [_55778, _55780, _55782] : [before_on_line(_55782, _55780, _55778), 71 ^ _53513 : [(72 ^ _53513) ^ [] : [-(distinct_points(_55780, _55778))], (74 ^ _53513) ^ [] : [left_apart_point(_55780, _55782)], (76 ^ _53513) ^ [] : [left_apart_point(_55780, reverse_line(_55782))], (78 ^ _53513) ^ [] : [left_apart_point(_55778, _55782)], (80 ^ _53513) ^ [] : [left_apart_point(_55778, reverse_line(_55782))], (82 ^ _53513) ^ [] : [unequally_directed_lines(_55782, line_connecting(_55780, _55778))]]], (84 ^ _53513) ^ [_56348, _56350, _56352] : [-(before_on_line(_56352, _56350, _56348)), distinct_points(_56350, _56348), -(left_apart_point(_56350, _56352)), -(left_apart_point(_56350, reverse_line(_56352))), -(unequally_directed_lines(_56352, line_connecting(_56350, _56348))), -(left_apart_point(_56348, _56352)), -(left_apart_point(_56348, reverse_line(_56352)))], (110 ^ _53513) ^ [_57117, _57119, _57121, _57123] : [between_on_line(_57123, _57121, _57119, _57117), 115 ^ _53513 : [(116 ^ _53513) ^ [] : [-(before_on_line(_57123, _57121, _57119))], (118 ^ _53513) ^ [] : [-(before_on_line(_57123, _57119, _57117))]], 119 ^ _53513 : [(120 ^ _53513) ^ [] : [-(before_on_line(_57123, _57117, _57119))], (122 ^ _53513) ^ [] : [-(before_on_line(_57123, _57119, _57121))]]], (124 ^ _53513) ^ [_57559, _57561, _57563, _57565] : [-(between_on_line(_57565, _57563, _57561, _57559)), 125 ^ _53513 : [(126 ^ _53513) ^ [] : [before_on_line(_57565, _57563, _57561), before_on_line(_57565, _57561, _57559)], (132 ^ _53513) ^ [] : [before_on_line(_57565, _57559, _57561), before_on_line(_57565, _57561, _57563)]]], (140 ^ _53513) ^ [_58037] : [distinct_points(_58037, _58037)], (142 ^ _53513) ^ [_58158, _58160, _58162] : [distinct_points(_58162, _58160), -(distinct_points(_58162, _58158)), -(distinct_points(_58160, _58158))], (152 ^ _53513) ^ [_58438] : [distinct_lines(_58438, _58438)], (154 ^ _53513) ^ [_58559, _58561, _58563] : [distinct_lines(_58563, _58561), -(distinct_lines(_58563, _58559)), -(distinct_lines(_58561, _58559))], (164 ^ _53513) ^ [_58839] : [unequally_directed_lines(_58839, _58839)], (166 ^ _53513) ^ [_58960, _58962, _58964] : [unequally_directed_lines(_58964, _58962), -(unequally_directed_lines(_58964, _58960)), -(unequally_directed_lines(_58962, _58960))], (176 ^ _53513) ^ [_59284, _59286, _59288] : [unequally_directed_lines(_59288, _59286), unequally_directed_lines(_59288, reverse_line(_59286)), 185 ^ _53513 : [(186 ^ _53513) ^ [] : [-(unequally_directed_lines(_59288, _59284))], (188 ^ _53513) ^ [] : [-(unequally_directed_lines(_59288, reverse_line(_59284)))]], 189 ^ _53513 : [(190 ^ _53513) ^ [] : [-(unequally_directed_lines(_59286, _59284))], (192 ^ _53513) ^ [] : [-(unequally_directed_lines(_59286, reverse_line(_59284)))]]], (194 ^ _53513) ^ [_59855, _59857] : [line(_59857), line(_59855), -(unequally_directed_lines(_59857, _59855)), -(unequally_directed_lines(_59857, reverse_line(_59855)))], (208 ^ _53513) ^ [_60246, _60248] : [unequally_directed_lines(_60248, _60246), unequally_directed_lines(_60248, reverse_line(_60246)), -(left_convergent_lines(_60248, _60246)), -(left_convergent_lines(_60248, reverse_line(_60246)))], (222 ^ _53513) ^ [_60649, _60651] : [left_apart_point(_60651, _60649)], (224 ^ _53513) ^ [_60694, _60696] : [left_apart_point(_60696, reverse_line(_60694))], (226 ^ _53513) ^ [_60811, _60813] : [left_convergent_lines(_60813, _60811)], (228 ^ _53513) ^ [_60856, _60858] : [left_convergent_lines(_60858, reverse_line(_60856))], (230 ^ _53513) ^ [_60969, _60971] : [-(line(line_connecting(_60971, _60969))), point(_60971), point(_60969), distinct_points(_60971, _60969)], (244 ^ _53513) ^ [_61357, _61359] : [-(point(intersection_point(_61359, _61357))), line(_61359), line(_61357), unequally_directed_lines(_61359, _61357), unequally_directed_lines(_61359, reverse_line(_61357))], (262 ^ _53513) ^ [_61838, _61840] : [-(line(parallel_through_point(_61840, _61838))), point(_61838), line(_61840)], (272 ^ _53513) ^ [_62123] : [line(_62123), -(line(reverse_line(_62123)))], (278 ^ _53513) ^ [_62327, _62329] : [distinct_points(_62329, _62327), 281 ^ _53513 : [(282 ^ _53513) ^ [] : [apart_point_and_line(_62329, line_connecting(_62329, _62327))], (284 ^ _53513) ^ [] : [apart_point_and_line(_62327, line_connecting(_62329, _62327))]]], (286 ^ _53513) ^ [_62626, _62628] : [293 ^ _53513 : [(294 ^ _53513) ^ [] : [apart_point_and_line(intersection_point(_62628, _62626), _62628)], (296 ^ _53513) ^ [] : [apart_point_and_line(intersection_point(_62628, _62626), _62626)]], unequally_directed_lines(_62628, _62626), unequally_directed_lines(_62628, reverse_line(_62626))], (298 ^ _53513) ^ [_63002, _63004] : [apart_point_and_line(_63004, parallel_through_point(_63002, _63004))], (300 ^ _53513) ^ [_63084] : [distinct_lines(_63084, reverse_line(_63084))], (302 ^ _53513) ^ [_63177, _63179] : [unequally_directed_lines(line_connecting(_63179, _63177), reverse_line(line_connecting(_63177, _63179)))], (304 ^ _53513) ^ [_63278, _63280] : [unequally_directed_lines(parallel_through_point(_63278, _63280), _63278)], (306 ^ _53513) ^ [_63418, _63420, _63422, _63424] : [distinct_points(_63424, _63422), distinct_lines(_63420, _63418), -(left_apart_point(_63424, _63420)), -(left_apart_point(_63422, _63420)), -(left_apart_point(_63424, _63418)), -(left_apart_point(_63422, _63418)), -(left_apart_point(_63424, reverse_line(_63420))), -(left_apart_point(_63422, reverse_line(_63420))), -(left_apart_point(_63424, reverse_line(_63418))), -(left_apart_point(_63422, reverse_line(_63418)))], (344 ^ _53513) ^ [_64455, _64457, _64459] : [distinct_points(_64459, _64457), left_apart_point(_64459, _64455), -(left_apart_point(_64457, _64455)), -(left_convergent_lines(line_connecting(_64459, _64457), _64455))], (358 ^ _53513) ^ [_64880, _64882, _64884] : [left_apart_point(_64884, _64880), -(distinct_points(_64884, _64882)), -(left_apart_point(_64882, _64880))], (382 ^ _53513) ^ [_65607, _65609, _65611] : [left_convergent_lines(_65611, _65609), -(unequally_directed_lines(_65609, _65607)), -(left_convergent_lines(_65611, _65607))], (368 ^ _53513) ^ [_65204, _65206, _65208] : [left_apart_point(_65208, _65206), unequally_directed_lines(_65206, _65204), -(distinct_lines(_65206, _65204)), -(left_apart_point(_65208, reverse_line(_65204)))]], input).
% 0.36/1.37 ncf('1',plain,[unequally_directed_lines(392 ^ [], reverse_line(393 ^ []))],start(399 ^ 0)).
% 0.36/1.37 ncf('1.1',plain,[-(unequally_directed_lines(392 ^ [], reverse_line(393 ^ []))), unequally_directed_lines(reverse_line(392 ^ []), 392 ^ []), -(unequally_directed_lines(reverse_line(392 ^ []), reverse_line(393 ^ [])))],extension(166 ^ 1,bind([[_58960, _58962, _58964], [reverse_line(393 ^ []), 392 ^ [], reverse_line(392 ^ [])]]))).
% 0.36/1.37 ncf('1.1.1',plain,[-(unequally_directed_lines(reverse_line(392 ^ []), 392 ^ [])), unequally_directed_lines(391 ^ [], reverse_line(392 ^ [])), -(unequally_directed_lines(391 ^ [], 392 ^ []))],extension(166 ^ 2,bind([[_58960, _58962, _58964], [392 ^ [], reverse_line(392 ^ []), 391 ^ []]]))).
% 0.36/1.37 ncf('1.1.1.1',plain,[-(unequally_directed_lines(391 ^ [], reverse_line(392 ^ [])))],extension(395 ^ 3)).
% 0.36/1.37 ncf('1.1.1.2',plain,[unequally_directed_lines(391 ^ [], 392 ^ []), unequally_directed_lines(391 ^ [], reverse_line(392 ^ [])), 186 : -(unequally_directed_lines(391 ^ [], 393 ^ [])), 192 : -(unequally_directed_lines(392 ^ [], reverse_line(393 ^ [])))],extension(176 ^ 3,bind([[_59284, _59286, _59288], [393 ^ [], 392 ^ [], 391 ^ []]]))).
% 0.36/1.37 ncf('1.1.1.2.1',plain,[-(unequally_directed_lines(391 ^ [], reverse_line(392 ^ [])))],lemmata('[1, 1].x')).
% 0.36/1.37 ncf('1.1.1.2.2',plain,[unequally_directed_lines(391 ^ [], 393 ^ [])],extension(397 ^ 6)).
% 0.36/1.37 ncf('1.1.1.2.3',plain,[unequally_directed_lines(392 ^ [], reverse_line(393 ^ []))],reduction('1')).
% 0.36/1.37 ncf('1.1.2',plain,[unequally_directed_lines(reverse_line(392 ^ []), reverse_line(393 ^ [])), unequally_directed_lines(reverse_line(392 ^ []), 393 ^ []), -(left_convergent_lines(reverse_line(392 ^ []), 393 ^ [])), -(left_convergent_lines(reverse_line(392 ^ []), reverse_line(393 ^ [])))],extension(208 ^ 2,bind([[_60246, _60248], [393 ^ [], reverse_line(392 ^ [])]]))).
% 0.36/1.37 ncf('1.1.2.1',plain,[-(unequally_directed_lines(reverse_line(392 ^ []), 393 ^ [])), unequally_directed_lines(391 ^ [], reverse_line(392 ^ [])), -(unequally_directed_lines(391 ^ [], 393 ^ []))],extension(166 ^ 3,bind([[_58960, _58962, _58964], [393 ^ [], reverse_line(392 ^ []), 391 ^ []]]))).
% 0.36/1.37 ncf('1.1.2.1.1',plain,[-(unequally_directed_lines(391 ^ [], reverse_line(392 ^ [])))],extension(395 ^ 4)).
% 0.36/1.37 ncf('1.1.2.1.2',plain,[unequally_directed_lines(391 ^ [], 393 ^ [])],extension(397 ^ 4)).
% 0.36/1.37 ncf('1.1.2.2',plain,[left_convergent_lines(reverse_line(392 ^ []), 393 ^ [])],extension(226 ^ 3,bind([[_60811, _60813], [393 ^ [], reverse_line(392 ^ [])]]))).
% 0.36/1.37 ncf('1.1.2.3',plain,[left_convergent_lines(reverse_line(392 ^ []), reverse_line(393 ^ []))],extension(226 ^ 3,bind([[_60811, _60813], [reverse_line(393 ^ []), reverse_line(392 ^ [])]]))).
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------