%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO188+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n017.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:07 EDT 2023
% Result : Theorem 0.77s 1.37s
% Output : Proof 0.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : GEO188+3 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.11/0.33 % Computer : n017.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Fri May 19 03:42:30 EDT 2023
% 0.11/0.33 % CPUTime :
% 0.77/1.37
% 0.77/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.77/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.77/1.37 %-----------------------------------------------------
% 0.77/1.37 ncf(matrix, plain, [(329 ^ _50868) ^ [] : [-(distinct_points(325 ^ [], 326 ^ []))], (331 ^ _50868) ^ [] : [-(distinct_points(325 ^ [], 327 ^ []))], (333 ^ _50868) ^ [] : [-(distinct_points(326 ^ [], 327 ^ []))], (335 ^ _50868) ^ [] : [-(incident_point_and_line(327 ^ [], line_connecting(325 ^ [], 326 ^ [])))], (337 ^ _50868) ^ [] : [incident_point_and_line(325 ^ [], line_connecting(327 ^ [], 326 ^ []))], (2 ^ _50868) ^ [_50971] : [distinct_points(_50971, _50971)], (4 ^ _50868) ^ [_51048] : [distinct_lines(_51048, _51048)], (6 ^ _50868) ^ [_51125] : [convergent_lines(_51125, _51125)], (8 ^ _50868) ^ [_51246, _51248, _51250] : [distinct_points(_51250, _51248), -(distinct_points(_51250, _51246)), -(distinct_points(_51248, _51246))], (18 ^ _50868) ^ [_51570, _51572, _51574] : [distinct_lines(_51574, _51572), -(distinct_lines(_51574, _51570)), -(distinct_lines(_51572, _51570))], (28 ^ _50868) ^ [_51894, _51896, _51898] : [convergent_lines(_51898, _51896), -(convergent_lines(_51898, _51894)), -(convergent_lines(_51896, _51894))], (38 ^ _50868) ^ [_52204, _52206] : [distinct_points(_52206, _52204), apart_point_and_line(_52206, line_connecting(_52206, _52204))], (44 ^ _50868) ^ [_52421, _52423] : [distinct_points(_52423, _52421), apart_point_and_line(_52421, line_connecting(_52423, _52421))], (50 ^ _50868) ^ [_52638, _52640] : [convergent_lines(_52640, _52638), apart_point_and_line(intersection_point(_52640, _52638), _52640)], (56 ^ _50868) ^ [_52855, _52857] : [convergent_lines(_52857, _52855), apart_point_and_line(intersection_point(_52857, _52855), _52855)], (62 ^ _50868) ^ [_53100, _53102, _53104, _53106] : [distinct_points(_53106, _53104), distinct_lines(_53102, _53100), -(apart_point_and_line(_53106, _53102)), -(apart_point_and_line(_53106, _53100)), -(apart_point_and_line(_53104, _53102)), -(apart_point_and_line(_53104, _53100))], (84 ^ _50868) ^ [_53729, _53731, _53733] : [apart_point_and_line(_53733, _53731), -(distinct_points(_53733, _53729)), -(apart_point_and_line(_53729, _53731))], (94 ^ _50868) ^ [_54053, _54055, _54057] : [apart_point_and_line(_54057, _54055), -(distinct_lines(_54055, _54053)), -(apart_point_and_line(_54057, _54053))], (104 ^ _50868) ^ [_54357, _54359, _54361] : [convergent_lines(_54361, _54359), -(distinct_lines(_54359, _54357)), -(convergent_lines(_54361, _54357))], (114 ^ _50868) ^ [_54693, _54695] : [distinct_lines(_54695, _54693), -(convergent_lines(_54695, _54693))], (120 ^ _50868) ^ [_54907, _54909] : [convergent_lines(parallel_through_point(_54907, _54909), _54907)], (122 ^ _50868) ^ [_55003, _55005] : [apart_point_and_line(_55005, parallel_through_point(_55003, _55005))], (124 ^ _50868) ^ [_55109, _55111, _55113] : [distinct_lines(_55111, _55109), -(apart_point_and_line(_55113, _55111)), -(apart_point_and_line(_55113, _55109)), -(convergent_lines(_55111, _55109))], (138 ^ _50868) ^ [_55537, _55539] : [-(convergent_lines(_55539, _55537)), -(unorthogonal_lines(_55539, _55537))], (144 ^ _50868) ^ [_55762, _55764, _55766] : [convergent_lines(_55766, _55764), unorthogonal_lines(_55766, _55764), 153 ^ _50868 : [(154 ^ _50868) ^ [] : [-(convergent_lines(_55766, _55762))], (156 ^ _50868) ^ [] : [-(unorthogonal_lines(_55766, _55762))]], 157 ^ _50868 : [(158 ^ _50868) ^ [] : [-(convergent_lines(_55764, _55762))], (160 ^ _50868) ^ [] : [-(unorthogonal_lines(_55764, _55762))]]], (162 ^ _50868) ^ [_56305, _56307] : [unorthogonal_lines(orthogonal_through_point(_56305, _56307), _56305)], (164 ^ _50868) ^ [_56401, _56403] : [apart_point_and_line(_56403, orthogonal_through_point(_56401, _56403))], (166 ^ _50868) ^ [_56521, _56523, _56525, _56527] : [distinct_lines(_56525, _56523), -(apart_point_and_line(_56527, _56525)), -(apart_point_and_line(_56527, _56523)), -(unorthogonal_lines(_56525, _56521)), -(unorthogonal_lines(_56523, _56521))], (184 ^ _50868) ^ [_57065, _57067] : [-(convergent_lines(_57067, _57065)), -(unorthogonal_lines(_57067, _57065))], (208 ^ _50868) ^ [_57859, _57861, _57863] : [convergent_lines(_57861, _57859), -(unorthogonal_lines(_57863, _57861)), -(unorthogonal_lines(_57863, _57859))], (190 ^ _50868) ^ [_57294, _57296, _57298] : [193 ^ _50868 : [(194 ^ _50868) ^ [] : [-(convergent_lines(_57298, _57296))], (196 ^ _50868) ^ [] : [-(unorthogonal_lines(_57298, _57296))]], 197 ^ _50868 : [(198 ^ _50868) ^ [] : [-(convergent_lines(_57298, _57294))], (200 ^ _50868) ^ [] : [-(unorthogonal_lines(_57298, _57294))]], convergent_lines(_57296, _57294), unorthogonal_lines(_57296, _57294)], (218 ^ _50868) ^ [_58199, _58201] : [-(line(line_connecting(_58201, _58199))), point(_58201), point(_58199), distinct_points(_58201, _58199)], (232 ^ _50868) ^ [_58587, _58589] : [-(point(intersection_point(_58589, _58587))), line(_58589), line(_58587), convergent_lines(_58589, _58587)], (246 ^ _50868) ^ [_58975, _58977] : [-(line(parallel_through_point(_58977, _58975))), line(_58977), point(_58975)], (256 ^ _50868) ^ [_59254, _59256] : [-(line(orthogonal_through_point(_59256, _59254))), line(_59256), point(_59254)], (266 ^ _50868) ^ [_59588, _59590] : [equal_points(_59590, _59588), distinct_points(_59590, _59588)], (272 ^ _50868) ^ [_59751, _59753] : [-(distinct_points(_59753, _59751)), -(equal_points(_59753, _59751))], (278 ^ _50868) ^ [_59995, _59997] : [equal_lines(_59997, _59995), distinct_lines(_59997, _59995)], (284 ^ _50868) ^ [_60158, _60160] : [-(distinct_lines(_60160, _60158)), -(equal_lines(_60160, _60158))], (290 ^ _50868) ^ [_60402, _60404] : [parallel_lines(_60404, _60402), convergent_lines(_60404, _60402)], (296 ^ _50868) ^ [_60565, _60567] : [-(convergent_lines(_60567, _60565)), -(parallel_lines(_60567, _60565))], (302 ^ _50868) ^ [_60809, _60811] : [incident_point_and_line(_60811, _60809), apart_point_and_line(_60811, _60809)], (308 ^ _50868) ^ [_60972, _60974] : [-(apart_point_and_line(_60974, _60972)), -(incident_point_and_line(_60974, _60972))], (314 ^ _50868) ^ [_61196, _61198] : [orthogonal_lines(_61198, _61196), unorthogonal_lines(_61198, _61196)], (320 ^ _50868) ^ [_61359, _61361] : [-(unorthogonal_lines(_61361, _61359)), -(orthogonal_lines(_61361, _61359))]], input).
% 0.77/1.37 ncf('1',plain,[convergent_lines(parallel_through_point(line_connecting(327 ^ [], 326 ^ []), 325 ^ []), line_connecting(327 ^ [], 326 ^ []))],start(120 ^ 0,bind([[_54907, _54909], [line_connecting(327 ^ [], 326 ^ []), 325 ^ []]]))).
% 0.77/1.37 ncf('1.1',plain,[-(convergent_lines(parallel_through_point(line_connecting(327 ^ [], 326 ^ []), 325 ^ []), line_connecting(327 ^ [], 326 ^ []))), distinct_lines(parallel_through_point(line_connecting(327 ^ [], 326 ^ []), 325 ^ []), line_connecting(327 ^ [], 326 ^ []))],extension(114 ^ 1,bind([[_54693, _54695], [line_connecting(327 ^ [], 326 ^ []), parallel_through_point(line_connecting(327 ^ [], 326 ^ []), 325 ^ [])]]))).
% 0.77/1.37 ncf('1.1.1',plain,[-(distinct_lines(parallel_through_point(line_connecting(327 ^ [], 326 ^ []), 325 ^ []), line_connecting(327 ^ [], 326 ^ []))), distinct_lines(line_connecting(327 ^ [], 326 ^ []), parallel_through_point(line_connecting(327 ^ [], 326 ^ []), 325 ^ [])), -(distinct_lines(line_connecting(327 ^ [], 326 ^ []), line_connecting(327 ^ [], 326 ^ [])))],extension(18 ^ 2,bind([[_51570, _51572, _51574], [line_connecting(327 ^ [], 326 ^ []), parallel_through_point(line_connecting(327 ^ [], 326 ^ []), 325 ^ []), line_connecting(327 ^ [], 326 ^ [])]]))).
% 0.77/1.37 ncf('1.1.1.1',plain,[-(distinct_lines(line_connecting(327 ^ [], 326 ^ []), parallel_through_point(line_connecting(327 ^ [], 326 ^ []), 325 ^ []))), apart_point_and_line(325 ^ [], line_connecting(327 ^ [], 326 ^ [])), -(apart_point_and_line(325 ^ [], parallel_through_point(line_connecting(327 ^ [], 326 ^ []), 325 ^ [])))],extension(94 ^ 3,bind([[_54053, _54055, _54057], [parallel_through_point(line_connecting(327 ^ [], 326 ^ []), 325 ^ []), line_connecting(327 ^ [], 326 ^ []), 325 ^ []]]))).
% 0.77/1.37 ncf('1.1.1.1.1',plain,[-(apart_point_and_line(325 ^ [], line_connecting(327 ^ [], 326 ^ []))), -(incident_point_and_line(325 ^ [], line_connecting(327 ^ [], 326 ^ [])))],extension(308 ^ 4,bind([[_60972, _60974], [line_connecting(327 ^ [], 326 ^ []), 325 ^ []]]))).
% 0.77/1.37 ncf('1.1.1.1.1.1',plain,[incident_point_and_line(325 ^ [], line_connecting(327 ^ [], 326 ^ []))],extension(337 ^ 5)).
% 0.77/1.37 ncf('1.1.1.1.2',plain,[apart_point_and_line(325 ^ [], parallel_through_point(line_connecting(327 ^ [], 326 ^ []), 325 ^ []))],extension(122 ^ 4,bind([[_55003, _55005], [line_connecting(327 ^ [], 326 ^ []), 325 ^ []]]))).
% 0.77/1.37 ncf('1.1.1.2',plain,[distinct_lines(line_connecting(327 ^ [], 326 ^ []), line_connecting(327 ^ [], 326 ^ []))],extension(4 ^ 3,bind([[_51048], [line_connecting(327 ^ [], 326 ^ [])]]))).
% 0.77/1.37 %-----------------------------------------------------
% 0.77/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------