%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO238+1 : TPTP v8.1.2. Bugfixed v6.4.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:19 EDT 2023
% Result : Theorem 0.34s 1.39s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GEO238+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% 0.11/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n015.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri May 19 04:40:07 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.34/1.39
% 0.34/1.39 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.34/1.39 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.34/1.39 %-----------------------------------------------------
% 0.34/1.39 ncf(matrix, plain, [(396 ^ _52707) ^ [] : [-(divides_points(394 ^ [], 391 ^ [], 392 ^ []))], (398 ^ _52707) ^ [] : [-(divides_points(394 ^ [], 391 ^ [], 393 ^ []))], (400 ^ _52707) ^ [] : [-(divides_points(394 ^ [], 392 ^ [], 393 ^ []))], (12 ^ _52707) ^ [_53105, _53107] : [13 ^ _52707 : [(14 ^ _52707) ^ [] : [left_apart_point(_53107, _53105)], (16 ^ _52707) ^ [] : [left_apart_point(_53107, reverse_line(_53105))]], -(apart_point_and_line(_53107, _53105))], (2 ^ _52707) ^ [_52849, _52851] : [apart_point_and_line(_52851, _52849), -(left_apart_point(_52851, _52849)), -(left_apart_point(_52851, reverse_line(_52849)))], (20 ^ _52707) ^ [_53424, _53426] : [convergent_lines(_53426, _53424), 23 ^ _52707 : [(24 ^ _52707) ^ [] : [-(unequally_directed_lines(_53426, _53424))], (26 ^ _52707) ^ [] : [-(unequally_directed_lines(_53426, reverse_line(_53424)))]]], (28 ^ _52707) ^ [_53665, _53667] : [-(convergent_lines(_53667, _53665)), unequally_directed_lines(_53667, _53665), unequally_directed_lines(_53667, reverse_line(_53665))], (38 ^ _52707) ^ [_54013, _54015, _54017] : [divides_points(_54013, _54017, _54015), 43 ^ _52707 : [(44 ^ _52707) ^ [] : [-(left_apart_point(_54017, _54013))], (46 ^ _52707) ^ [] : [-(left_apart_point(_54015, reverse_line(_54013)))]], 47 ^ _52707 : [(48 ^ _52707) ^ [] : [-(left_apart_point(_54017, reverse_line(_54013)))], (50 ^ _52707) ^ [] : [-(left_apart_point(_54015, _54013))]]], (52 ^ _52707) ^ [_54439, _54441, _54443] : [-(divides_points(_54439, _54443, _54441)), 53 ^ _52707 : [(54 ^ _52707) ^ [] : [left_apart_point(_54443, _54439), left_apart_point(_54441, reverse_line(_54439))], (60 ^ _52707) ^ [] : [left_apart_point(_54443, reverse_line(_54439)), left_apart_point(_54441, _54439)]]], (68 ^ _52707) ^ [_54972, _54974, _54976] : [before_on_line(_54976, _54974, _54972), 71 ^ _52707 : [(72 ^ _52707) ^ [] : [-(distinct_points(_54974, _54972))], (74 ^ _52707) ^ [] : [left_apart_point(_54974, _54976)], (76 ^ _52707) ^ [] : [left_apart_point(_54974, reverse_line(_54976))], (78 ^ _52707) ^ [] : [left_apart_point(_54972, _54976)], (80 ^ _52707) ^ [] : [left_apart_point(_54972, reverse_line(_54976))], (82 ^ _52707) ^ [] : [unequally_directed_lines(_54976, line_connecting(_54974, _54972))]]], (84 ^ _52707) ^ [_55542, _55544, _55546] : [-(before_on_line(_55546, _55544, _55542)), distinct_points(_55544, _55542), -(left_apart_point(_55544, _55546)), -(left_apart_point(_55544, reverse_line(_55546))), -(unequally_directed_lines(_55546, line_connecting(_55544, _55542))), -(left_apart_point(_55542, _55546)), -(left_apart_point(_55542, reverse_line(_55546)))], (110 ^ _52707) ^ [_56311, _56313, _56315, _56317] : [between_on_line(_56317, _56315, _56313, _56311), 115 ^ _52707 : [(116 ^ _52707) ^ [] : [-(before_on_line(_56317, _56315, _56313))], (118 ^ _52707) ^ [] : [-(before_on_line(_56317, _56313, _56311))]], 119 ^ _52707 : [(120 ^ _52707) ^ [] : [-(before_on_line(_56317, _56311, _56313))], (122 ^ _52707) ^ [] : [-(before_on_line(_56317, _56313, _56315))]]], (124 ^ _52707) ^ [_56753, _56755, _56757, _56759] : [-(between_on_line(_56759, _56757, _56755, _56753)), 125 ^ _52707 : [(126 ^ _52707) ^ [] : [before_on_line(_56759, _56757, _56755), before_on_line(_56759, _56755, _56753)], (132 ^ _52707) ^ [] : [before_on_line(_56759, _56753, _56755), before_on_line(_56759, _56755, _56757)]]], (140 ^ _52707) ^ [_57231] : [distinct_points(_57231, _57231)], (142 ^ _52707) ^ [_57352, _57354, _57356] : [distinct_points(_57356, _57354), -(distinct_points(_57356, _57352)), -(distinct_points(_57354, _57352))], (152 ^ _52707) ^ [_57632] : [distinct_lines(_57632, _57632)], (154 ^ _52707) ^ [_57753, _57755, _57757] : [distinct_lines(_57757, _57755), -(distinct_lines(_57757, _57753)), -(distinct_lines(_57755, _57753))], (164 ^ _52707) ^ [_58033] : [unequally_directed_lines(_58033, _58033)], (166 ^ _52707) ^ [_58154, _58156, _58158] : [unequally_directed_lines(_58158, _58156), -(unequally_directed_lines(_58158, _58154)), -(unequally_directed_lines(_58156, _58154))], (176 ^ _52707) ^ [_58478, _58480, _58482] : [unequally_directed_lines(_58482, _58480), unequally_directed_lines(_58482, reverse_line(_58480)), 185 ^ _52707 : [(186 ^ _52707) ^ [] : [-(unequally_directed_lines(_58482, _58478))], (188 ^ _52707) ^ [] : [-(unequally_directed_lines(_58482, reverse_line(_58478)))]], 189 ^ _52707 : [(190 ^ _52707) ^ [] : [-(unequally_directed_lines(_58480, _58478))], (192 ^ _52707) ^ [] : [-(unequally_directed_lines(_58480, reverse_line(_58478)))]]], (194 ^ _52707) ^ [_59049, _59051] : [line(_59051), line(_59049), -(unequally_directed_lines(_59051, _59049)), -(unequally_directed_lines(_59051, reverse_line(_59049)))], (208 ^ _52707) ^ [_59440, _59442] : [unequally_directed_lines(_59442, _59440), unequally_directed_lines(_59442, reverse_line(_59440)), -(left_convergent_lines(_59442, _59440)), -(left_convergent_lines(_59442, reverse_line(_59440)))], (222 ^ _52707) ^ [_59843, _59845] : [left_apart_point(_59845, _59843)], (224 ^ _52707) ^ [_59888, _59890] : [left_apart_point(_59890, reverse_line(_59888))], (226 ^ _52707) ^ [_60005, _60007] : [left_convergent_lines(_60007, _60005)], (228 ^ _52707) ^ [_60050, _60052] : [left_convergent_lines(_60052, reverse_line(_60050))], (230 ^ _52707) ^ [_60163, _60165] : [-(line(line_connecting(_60165, _60163))), point(_60165), point(_60163), distinct_points(_60165, _60163)], (244 ^ _52707) ^ [_60551, _60553] : [-(point(intersection_point(_60553, _60551))), line(_60553), line(_60551), unequally_directed_lines(_60553, _60551), unequally_directed_lines(_60553, reverse_line(_60551))], (262 ^ _52707) ^ [_61032, _61034] : [-(line(parallel_through_point(_61034, _61032))), point(_61032), line(_61034)], (272 ^ _52707) ^ [_61317] : [line(_61317), -(line(reverse_line(_61317)))], (278 ^ _52707) ^ [_61521, _61523] : [distinct_points(_61523, _61521), 281 ^ _52707 : [(282 ^ _52707) ^ [] : [apart_point_and_line(_61523, line_connecting(_61523, _61521))], (284 ^ _52707) ^ [] : [apart_point_and_line(_61521, line_connecting(_61523, _61521))]]], (286 ^ _52707) ^ [_61820, _61822] : [293 ^ _52707 : [(294 ^ _52707) ^ [] : [apart_point_and_line(intersection_point(_61822, _61820), _61822)], (296 ^ _52707) ^ [] : [apart_point_and_line(intersection_point(_61822, _61820), _61820)]], unequally_directed_lines(_61822, _61820), unequally_directed_lines(_61822, reverse_line(_61820))], (298 ^ _52707) ^ [_62196, _62198] : [apart_point_and_line(_62198, parallel_through_point(_62196, _62198))], (300 ^ _52707) ^ [_62278] : [distinct_lines(_62278, reverse_line(_62278))], (302 ^ _52707) ^ [_62371, _62373] : [unequally_directed_lines(line_connecting(_62373, _62371), reverse_line(line_connecting(_62371, _62373)))], (304 ^ _52707) ^ [_62472, _62474] : [unequally_directed_lines(parallel_through_point(_62472, _62474), _62472)], (306 ^ _52707) ^ [_62612, _62614, _62616, _62618] : [distinct_points(_62618, _62616), distinct_lines(_62614, _62612), -(left_apart_point(_62618, _62614)), -(left_apart_point(_62616, _62614)), -(left_apart_point(_62618, _62612)), -(left_apart_point(_62616, _62612)), -(left_apart_point(_62618, reverse_line(_62614))), -(left_apart_point(_62616, reverse_line(_62614))), -(left_apart_point(_62618, reverse_line(_62612))), -(left_apart_point(_62616, reverse_line(_62612)))], (344 ^ _52707) ^ [_63649, _63651, _63653] : [distinct_points(_63653, _63651), left_apart_point(_63653, _63649), -(left_apart_point(_63651, _63649)), -(left_convergent_lines(line_connecting(_63653, _63651), _63649))], (358 ^ _52707) ^ [_64074, _64076, _64078] : [left_apart_point(_64078, _64074), -(distinct_points(_64078, _64076)), -(left_apart_point(_64076, _64074))], (382 ^ _52707) ^ [_64801, _64803, _64805] : [left_convergent_lines(_64805, _64803), -(unequally_directed_lines(_64803, _64801)), -(left_convergent_lines(_64805, _64801))], (368 ^ _52707) ^ [_64398, _64400, _64402] : [left_apart_point(_64402, _64400), unequally_directed_lines(_64400, _64398), -(distinct_lines(_64400, _64398)), -(left_apart_point(_64402, reverse_line(_64398)))]], input).
% 0.34/1.39 ncf('1',plain,[left_apart_point(391 ^ [], 394 ^ [])],start(222 ^ 0,bind([[_59843, _59845], [394 ^ [], 391 ^ []]]))).
% 0.34/1.39 ncf('1.1',plain,[-(left_apart_point(391 ^ [], 394 ^ [])), divides_points(394 ^ [], 391 ^ [], 392 ^ []), 48 : -(left_apart_point(391 ^ [], reverse_line(394 ^ [])))],extension(38 ^ 1,bind([[_54013, _54015, _54017], [394 ^ [], 392 ^ [], 391 ^ []]]))).
% 0.34/1.39 ncf('1.1.1',plain,[-(divides_points(394 ^ [], 391 ^ [], 392 ^ []))],extension(396 ^ 2)).
% 0.34/1.39 ncf('1.1.2',plain,[left_apart_point(391 ^ [], reverse_line(394 ^ []))],extension(222 ^ 4,bind([[_59843, _59845], [reverse_line(394 ^ []), 391 ^ []]]))).
% 0.34/1.39 %-----------------------------------------------------
% 0.34/1.39 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------