%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO243+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n021.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:20 EDT 2023
% Result : Theorem 0.33s 1.39s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO243+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n021.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:42 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.33/1.39
% 0.33/1.39 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.33/1.39 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/1.39 %-----------------------------------------------------
% 0.33/1.39 ncf(matrix, plain, [(395 ^ _51886) ^ [] : [-(distinct_points(391 ^ [], 392 ^ []))], (397 ^ _51886) ^ [] : [-(left_apart_point(393 ^ [], line_connecting(391 ^ [], 392 ^ [])))], (399 ^ _51886) ^ [] : [left_apart_point(393 ^ [], reverse_line(line_connecting(392 ^ [], 391 ^ [])))], (12 ^ _51886) ^ [_52284, _52286] : [13 ^ _51886 : [(14 ^ _51886) ^ [] : [left_apart_point(_52286, _52284)], (16 ^ _51886) ^ [] : [left_apart_point(_52286, reverse_line(_52284))]], -(apart_point_and_line(_52286, _52284))], (2 ^ _51886) ^ [_52028, _52030] : [apart_point_and_line(_52030, _52028), -(left_apart_point(_52030, _52028)), -(left_apart_point(_52030, reverse_line(_52028)))], (20 ^ _51886) ^ [_52603, _52605] : [convergent_lines(_52605, _52603), 23 ^ _51886 : [(24 ^ _51886) ^ [] : [-(unequally_directed_lines(_52605, _52603))], (26 ^ _51886) ^ [] : [-(unequally_directed_lines(_52605, reverse_line(_52603)))]]], (28 ^ _51886) ^ [_52844, _52846] : [-(convergent_lines(_52846, _52844)), unequally_directed_lines(_52846, _52844), unequally_directed_lines(_52846, reverse_line(_52844))], (38 ^ _51886) ^ [_53192, _53194, _53196] : [divides_points(_53192, _53196, _53194), 43 ^ _51886 : [(44 ^ _51886) ^ [] : [-(left_apart_point(_53196, _53192))], (46 ^ _51886) ^ [] : [-(left_apart_point(_53194, reverse_line(_53192)))]], 47 ^ _51886 : [(48 ^ _51886) ^ [] : [-(left_apart_point(_53196, reverse_line(_53192)))], (50 ^ _51886) ^ [] : [-(left_apart_point(_53194, _53192))]]], (52 ^ _51886) ^ [_53618, _53620, _53622] : [-(divides_points(_53618, _53622, _53620)), 53 ^ _51886 : [(54 ^ _51886) ^ [] : [left_apart_point(_53622, _53618), left_apart_point(_53620, reverse_line(_53618))], (60 ^ _51886) ^ [] : [left_apart_point(_53622, reverse_line(_53618)), left_apart_point(_53620, _53618)]]], (68 ^ _51886) ^ [_54151, _54153, _54155] : [before_on_line(_54155, _54153, _54151), 71 ^ _51886 : [(72 ^ _51886) ^ [] : [-(distinct_points(_54153, _54151))], (74 ^ _51886) ^ [] : [left_apart_point(_54153, _54155)], (76 ^ _51886) ^ [] : [left_apart_point(_54153, reverse_line(_54155))], (78 ^ _51886) ^ [] : [left_apart_point(_54151, _54155)], (80 ^ _51886) ^ [] : [left_apart_point(_54151, reverse_line(_54155))], (82 ^ _51886) ^ [] : [unequally_directed_lines(_54155, line_connecting(_54153, _54151))]]], (84 ^ _51886) ^ [_54721, _54723, _54725] : [-(before_on_line(_54725, _54723, _54721)), distinct_points(_54723, _54721), -(left_apart_point(_54723, _54725)), -(left_apart_point(_54723, reverse_line(_54725))), -(unequally_directed_lines(_54725, line_connecting(_54723, _54721))), -(left_apart_point(_54721, _54725)), -(left_apart_point(_54721, reverse_line(_54725)))], (110 ^ _51886) ^ [_55490, _55492, _55494, _55496] : [between_on_line(_55496, _55494, _55492, _55490), 115 ^ _51886 : [(116 ^ _51886) ^ [] : [-(before_on_line(_55496, _55494, _55492))], (118 ^ _51886) ^ [] : [-(before_on_line(_55496, _55492, _55490))]], 119 ^ _51886 : [(120 ^ _51886) ^ [] : [-(before_on_line(_55496, _55490, _55492))], (122 ^ _51886) ^ [] : [-(before_on_line(_55496, _55492, _55494))]]], (124 ^ _51886) ^ [_55932, _55934, _55936, _55938] : [-(between_on_line(_55938, _55936, _55934, _55932)), 125 ^ _51886 : [(126 ^ _51886) ^ [] : [before_on_line(_55938, _55936, _55934), before_on_line(_55938, _55934, _55932)], (132 ^ _51886) ^ [] : [before_on_line(_55938, _55932, _55934), before_on_line(_55938, _55934, _55936)]]], (140 ^ _51886) ^ [_56410] : [distinct_points(_56410, _56410)], (142 ^ _51886) ^ [_56531, _56533, _56535] : [distinct_points(_56535, _56533), -(distinct_points(_56535, _56531)), -(distinct_points(_56533, _56531))], (152 ^ _51886) ^ [_56811] : [distinct_lines(_56811, _56811)], (154 ^ _51886) ^ [_56932, _56934, _56936] : [distinct_lines(_56936, _56934), -(distinct_lines(_56936, _56932)), -(distinct_lines(_56934, _56932))], (164 ^ _51886) ^ [_57212] : [unequally_directed_lines(_57212, _57212)], (166 ^ _51886) ^ [_57333, _57335, _57337] : [unequally_directed_lines(_57337, _57335), -(unequally_directed_lines(_57337, _57333)), -(unequally_directed_lines(_57335, _57333))], (176 ^ _51886) ^ [_57657, _57659, _57661] : [unequally_directed_lines(_57661, _57659), unequally_directed_lines(_57661, reverse_line(_57659)), 185 ^ _51886 : [(186 ^ _51886) ^ [] : [-(unequally_directed_lines(_57661, _57657))], (188 ^ _51886) ^ [] : [-(unequally_directed_lines(_57661, reverse_line(_57657)))]], 189 ^ _51886 : [(190 ^ _51886) ^ [] : [-(unequally_directed_lines(_57659, _57657))], (192 ^ _51886) ^ [] : [-(unequally_directed_lines(_57659, reverse_line(_57657)))]]], (194 ^ _51886) ^ [_58228, _58230] : [line(_58230), line(_58228), -(unequally_directed_lines(_58230, _58228)), -(unequally_directed_lines(_58230, reverse_line(_58228)))], (208 ^ _51886) ^ [_58619, _58621] : [unequally_directed_lines(_58621, _58619), unequally_directed_lines(_58621, reverse_line(_58619)), -(left_convergent_lines(_58621, _58619)), -(left_convergent_lines(_58621, reverse_line(_58619)))], (222 ^ _51886) ^ [_59022, _59024] : [left_apart_point(_59024, _59022)], (224 ^ _51886) ^ [_59067, _59069] : [left_apart_point(_59069, reverse_line(_59067))], (226 ^ _51886) ^ [_59184, _59186] : [left_convergent_lines(_59186, _59184)], (228 ^ _51886) ^ [_59229, _59231] : [left_convergent_lines(_59231, reverse_line(_59229))], (230 ^ _51886) ^ [_59342, _59344] : [-(line(line_connecting(_59344, _59342))), point(_59344), point(_59342), distinct_points(_59344, _59342)], (244 ^ _51886) ^ [_59730, _59732] : [-(point(intersection_point(_59732, _59730))), line(_59732), line(_59730), unequally_directed_lines(_59732, _59730), unequally_directed_lines(_59732, reverse_line(_59730))], (262 ^ _51886) ^ [_60211, _60213] : [-(line(parallel_through_point(_60213, _60211))), point(_60211), line(_60213)], (272 ^ _51886) ^ [_60496] : [line(_60496), -(line(reverse_line(_60496)))], (278 ^ _51886) ^ [_60700, _60702] : [distinct_points(_60702, _60700), 281 ^ _51886 : [(282 ^ _51886) ^ [] : [apart_point_and_line(_60702, line_connecting(_60702, _60700))], (284 ^ _51886) ^ [] : [apart_point_and_line(_60700, line_connecting(_60702, _60700))]]], (286 ^ _51886) ^ [_60999, _61001] : [293 ^ _51886 : [(294 ^ _51886) ^ [] : [apart_point_and_line(intersection_point(_61001, _60999), _61001)], (296 ^ _51886) ^ [] : [apart_point_and_line(intersection_point(_61001, _60999), _60999)]], unequally_directed_lines(_61001, _60999), unequally_directed_lines(_61001, reverse_line(_60999))], (298 ^ _51886) ^ [_61375, _61377] : [apart_point_and_line(_61377, parallel_through_point(_61375, _61377))], (300 ^ _51886) ^ [_61457] : [distinct_lines(_61457, reverse_line(_61457))], (302 ^ _51886) ^ [_61550, _61552] : [unequally_directed_lines(line_connecting(_61552, _61550), reverse_line(line_connecting(_61550, _61552)))], (304 ^ _51886) ^ [_61651, _61653] : [unequally_directed_lines(parallel_through_point(_61651, _61653), _61651)], (306 ^ _51886) ^ [_61791, _61793, _61795, _61797] : [distinct_points(_61797, _61795), distinct_lines(_61793, _61791), -(left_apart_point(_61797, _61793)), -(left_apart_point(_61795, _61793)), -(left_apart_point(_61797, _61791)), -(left_apart_point(_61795, _61791)), -(left_apart_point(_61797, reverse_line(_61793))), -(left_apart_point(_61795, reverse_line(_61793))), -(left_apart_point(_61797, reverse_line(_61791))), -(left_apart_point(_61795, reverse_line(_61791)))], (344 ^ _51886) ^ [_62828, _62830, _62832] : [distinct_points(_62832, _62830), left_apart_point(_62832, _62828), -(left_apart_point(_62830, _62828)), -(left_convergent_lines(line_connecting(_62832, _62830), _62828))], (358 ^ _51886) ^ [_63253, _63255, _63257] : [left_apart_point(_63257, _63253), -(distinct_points(_63257, _63255)), -(left_apart_point(_63255, _63253))], (382 ^ _51886) ^ [_63980, _63982, _63984] : [left_convergent_lines(_63984, _63982), -(unequally_directed_lines(_63982, _63980)), -(left_convergent_lines(_63984, _63980))], (368 ^ _51886) ^ [_63577, _63579, _63581] : [left_apart_point(_63581, _63579), unequally_directed_lines(_63579, _63577), -(distinct_lines(_63579, _63577)), -(left_apart_point(_63581, reverse_line(_63577)))]], input).
% 0.33/1.39 ncf('1',plain,[left_apart_point(393 ^ [], line_connecting(391 ^ [], 392 ^ []))],start(222 ^ 0,bind([[_59022, _59024], [line_connecting(391 ^ [], 392 ^ []), 393 ^ []]]))).
% 0.33/1.39 ncf('1.1',plain,[-(left_apart_point(393 ^ [], line_connecting(391 ^ [], 392 ^ [])))],extension(397 ^ 1)).
% 0.33/1.39 %-----------------------------------------------------
% 0.33/1.39 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------