%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO210+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n013.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:14 EDT 2023
% Result : Theorem 0.34s 1.38s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GEO210+3 : TPTP v8.1.2. Released v4.0.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n013.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.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri May 19 03:57:50 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.34/1.38
% 0.34/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.34/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.34/1.38 %-----------------------------------------------------
% 0.34/1.38 ncf(matrix, plain, [(329 ^ _50728) ^ [] : [-(incident_point_and_line(325 ^ [], 326 ^ []))], (331 ^ _50728) ^ [] : [-(orthogonal_lines(326 ^ [], 327 ^ []))], (333 ^ _50728) ^ [] : [equal_lines(326 ^ [], orthogonal_through_point(327 ^ [], 325 ^ []))], (2 ^ _50728) ^ [_50831] : [distinct_points(_50831, _50831)], (4 ^ _50728) ^ [_50908] : [distinct_lines(_50908, _50908)], (6 ^ _50728) ^ [_50985] : [convergent_lines(_50985, _50985)], (8 ^ _50728) ^ [_51106, _51108, _51110] : [distinct_points(_51110, _51108), -(distinct_points(_51110, _51106)), -(distinct_points(_51108, _51106))], (18 ^ _50728) ^ [_51430, _51432, _51434] : [distinct_lines(_51434, _51432), -(distinct_lines(_51434, _51430)), -(distinct_lines(_51432, _51430))], (28 ^ _50728) ^ [_51754, _51756, _51758] : [convergent_lines(_51758, _51756), -(convergent_lines(_51758, _51754)), -(convergent_lines(_51756, _51754))], (38 ^ _50728) ^ [_52064, _52066] : [distinct_points(_52066, _52064), apart_point_and_line(_52066, line_connecting(_52066, _52064))], (44 ^ _50728) ^ [_52281, _52283] : [distinct_points(_52283, _52281), apart_point_and_line(_52281, line_connecting(_52283, _52281))], (50 ^ _50728) ^ [_52498, _52500] : [convergent_lines(_52500, _52498), apart_point_and_line(intersection_point(_52500, _52498), _52500)], (56 ^ _50728) ^ [_52715, _52717] : [convergent_lines(_52717, _52715), apart_point_and_line(intersection_point(_52717, _52715), _52715)], (62 ^ _50728) ^ [_52960, _52962, _52964, _52966] : [distinct_points(_52966, _52964), distinct_lines(_52962, _52960), -(apart_point_and_line(_52966, _52962)), -(apart_point_and_line(_52966, _52960)), -(apart_point_and_line(_52964, _52962)), -(apart_point_and_line(_52964, _52960))], (84 ^ _50728) ^ [_53589, _53591, _53593] : [apart_point_and_line(_53593, _53591), -(distinct_points(_53593, _53589)), -(apart_point_and_line(_53589, _53591))], (94 ^ _50728) ^ [_53913, _53915, _53917] : [apart_point_and_line(_53917, _53915), -(distinct_lines(_53915, _53913)), -(apart_point_and_line(_53917, _53913))], (104 ^ _50728) ^ [_54217, _54219, _54221] : [convergent_lines(_54221, _54219), -(distinct_lines(_54219, _54217)), -(convergent_lines(_54221, _54217))], (114 ^ _50728) ^ [_54553, _54555] : [distinct_lines(_54555, _54553), -(convergent_lines(_54555, _54553))], (120 ^ _50728) ^ [_54767, _54769] : [convergent_lines(parallel_through_point(_54767, _54769), _54767)], (122 ^ _50728) ^ [_54863, _54865] : [apart_point_and_line(_54865, parallel_through_point(_54863, _54865))], (124 ^ _50728) ^ [_54969, _54971, _54973] : [distinct_lines(_54971, _54969), -(apart_point_and_line(_54973, _54971)), -(apart_point_and_line(_54973, _54969)), -(convergent_lines(_54971, _54969))], (138 ^ _50728) ^ [_55397, _55399] : [-(convergent_lines(_55399, _55397)), -(unorthogonal_lines(_55399, _55397))], (144 ^ _50728) ^ [_55622, _55624, _55626] : [convergent_lines(_55626, _55624), unorthogonal_lines(_55626, _55624), 153 ^ _50728 : [(154 ^ _50728) ^ [] : [-(convergent_lines(_55626, _55622))], (156 ^ _50728) ^ [] : [-(unorthogonal_lines(_55626, _55622))]], 157 ^ _50728 : [(158 ^ _50728) ^ [] : [-(convergent_lines(_55624, _55622))], (160 ^ _50728) ^ [] : [-(unorthogonal_lines(_55624, _55622))]]], (162 ^ _50728) ^ [_56165, _56167] : [unorthogonal_lines(orthogonal_through_point(_56165, _56167), _56165)], (164 ^ _50728) ^ [_56261, _56263] : [apart_point_and_line(_56263, orthogonal_through_point(_56261, _56263))], (166 ^ _50728) ^ [_56381, _56383, _56385, _56387] : [distinct_lines(_56385, _56383), -(apart_point_and_line(_56387, _56385)), -(apart_point_and_line(_56387, _56383)), -(unorthogonal_lines(_56385, _56381)), -(unorthogonal_lines(_56383, _56381))], (184 ^ _50728) ^ [_56925, _56927] : [-(convergent_lines(_56927, _56925)), -(unorthogonal_lines(_56927, _56925))], (208 ^ _50728) ^ [_57719, _57721, _57723] : [convergent_lines(_57721, _57719), -(unorthogonal_lines(_57723, _57721)), -(unorthogonal_lines(_57723, _57719))], (190 ^ _50728) ^ [_57154, _57156, _57158] : [193 ^ _50728 : [(194 ^ _50728) ^ [] : [-(convergent_lines(_57158, _57156))], (196 ^ _50728) ^ [] : [-(unorthogonal_lines(_57158, _57156))]], 197 ^ _50728 : [(198 ^ _50728) ^ [] : [-(convergent_lines(_57158, _57154))], (200 ^ _50728) ^ [] : [-(unorthogonal_lines(_57158, _57154))]], convergent_lines(_57156, _57154), unorthogonal_lines(_57156, _57154)], (218 ^ _50728) ^ [_58059, _58061] : [-(line(line_connecting(_58061, _58059))), point(_58061), point(_58059), distinct_points(_58061, _58059)], (232 ^ _50728) ^ [_58447, _58449] : [-(point(intersection_point(_58449, _58447))), line(_58449), line(_58447), convergent_lines(_58449, _58447)], (246 ^ _50728) ^ [_58835, _58837] : [-(line(parallel_through_point(_58837, _58835))), line(_58837), point(_58835)], (256 ^ _50728) ^ [_59114, _59116] : [-(line(orthogonal_through_point(_59116, _59114))), line(_59116), point(_59114)], (266 ^ _50728) ^ [_59448, _59450] : [equal_points(_59450, _59448), distinct_points(_59450, _59448)], (272 ^ _50728) ^ [_59611, _59613] : [-(distinct_points(_59613, _59611)), -(equal_points(_59613, _59611))], (278 ^ _50728) ^ [_59855, _59857] : [equal_lines(_59857, _59855), distinct_lines(_59857, _59855)], (284 ^ _50728) ^ [_60018, _60020] : [-(distinct_lines(_60020, _60018)), -(equal_lines(_60020, _60018))], (290 ^ _50728) ^ [_60262, _60264] : [parallel_lines(_60264, _60262), convergent_lines(_60264, _60262)], (296 ^ _50728) ^ [_60425, _60427] : [-(convergent_lines(_60427, _60425)), -(parallel_lines(_60427, _60425))], (302 ^ _50728) ^ [_60669, _60671] : [incident_point_and_line(_60671, _60669), apart_point_and_line(_60671, _60669)], (308 ^ _50728) ^ [_60832, _60834] : [-(apart_point_and_line(_60834, _60832)), -(incident_point_and_line(_60834, _60832))], (314 ^ _50728) ^ [_61056, _61058] : [orthogonal_lines(_61058, _61056), unorthogonal_lines(_61058, _61056)], (320 ^ _50728) ^ [_61219, _61221] : [-(unorthogonal_lines(_61221, _61219)), -(orthogonal_lines(_61221, _61219))]], input).
% 0.34/1.38 ncf('1',plain,[convergent_lines(326 ^ [], orthogonal_through_point(327 ^ [], 325 ^ [])), apart_point_and_line(intersection_point(326 ^ [], orthogonal_through_point(327 ^ [], 325 ^ [])), 326 ^ [])],start(50 ^ 0,bind([[_52498, _52500], [orthogonal_through_point(327 ^ [], 325 ^ []), 326 ^ []]]))).
% 0.34/1.38 ncf('1.1',plain,[-(convergent_lines(326 ^ [], orthogonal_through_point(327 ^ [], 325 ^ []))), distinct_lines(326 ^ [], orthogonal_through_point(327 ^ [], 325 ^ []))],extension(114 ^ 1,bind([[_54553, _54555], [orthogonal_through_point(327 ^ [], 325 ^ []), 326 ^ []]]))).
% 0.34/1.38 ncf('1.1.1',plain,[-(distinct_lines(326 ^ [], orthogonal_through_point(327 ^ [], 325 ^ []))), -(equal_lines(326 ^ [], orthogonal_through_point(327 ^ [], 325 ^ [])))],extension(284 ^ 2,bind([[_60018, _60020], [orthogonal_through_point(327 ^ [], 325 ^ []), 326 ^ []]]))).
% 0.34/1.38 ncf('1.1.1.1',plain,[equal_lines(326 ^ [], orthogonal_through_point(327 ^ [], 325 ^ []))],extension(333 ^ 3)).
% 0.34/1.38 ncf('1.2',plain,[-(apart_point_and_line(intersection_point(326 ^ [], orthogonal_through_point(327 ^ [], 325 ^ [])), 326 ^ [])), distinct_lines(326 ^ [], orthogonal_through_point(327 ^ [], 325 ^ [])), -(apart_point_and_line(intersection_point(326 ^ [], orthogonal_through_point(327 ^ [], 325 ^ [])), orthogonal_through_point(327 ^ [], 325 ^ []))), -(unorthogonal_lines(326 ^ [], 327 ^ [])), -(unorthogonal_lines(orthogonal_through_point(327 ^ [], 325 ^ []), 327 ^ []))],extension(166 ^ 1,bind([[_56381, _56383, _56385, _56387], [327 ^ [], orthogonal_through_point(327 ^ [], 325 ^ []), 326 ^ [], intersection_point(326 ^ [], orthogonal_through_point(327 ^ [], 325 ^ []))]]))).
% 0.34/1.38 ncf('1.2.1',plain,[-(distinct_lines(326 ^ [], orthogonal_through_point(327 ^ [], 325 ^ []))), -(equal_lines(326 ^ [], orthogonal_through_point(327 ^ [], 325 ^ [])))],extension(284 ^ 2,bind([[_60018, _60020], [orthogonal_through_point(327 ^ [], 325 ^ []), 326 ^ []]]))).
% 0.34/1.38 ncf('1.2.1.1',plain,[equal_lines(326 ^ [], orthogonal_through_point(327 ^ [], 325 ^ []))],extension(333 ^ 3)).
% 0.34/1.38 ncf('1.2.2',plain,[apart_point_and_line(intersection_point(326 ^ [], orthogonal_through_point(327 ^ [], 325 ^ [])), orthogonal_through_point(327 ^ [], 325 ^ [])), convergent_lines(326 ^ [], orthogonal_through_point(327 ^ [], 325 ^ []))],extension(56 ^ 2,bind([[_52715, _52717], [orthogonal_through_point(327 ^ [], 325 ^ []), 326 ^ []]]))).
% 0.34/1.38 ncf('1.2.2.1',plain,[-(convergent_lines(326 ^ [], orthogonal_through_point(327 ^ [], 325 ^ [])))],lemmata('x')).
% 0.34/1.38 ncf('1.2.3',plain,[unorthogonal_lines(326 ^ [], 327 ^ []), orthogonal_lines(326 ^ [], 327 ^ [])],extension(314 ^ 2,bind([[_61056, _61058], [327 ^ [], 326 ^ []]]))).
% 0.34/1.38 ncf('1.2.3.1',plain,[-(orthogonal_lines(326 ^ [], 327 ^ []))],extension(331 ^ 3)).
% 0.34/1.38 ncf('1.2.4',plain,[unorthogonal_lines(orthogonal_through_point(327 ^ [], 325 ^ []), 327 ^ [])],extension(162 ^ 2,bind([[_56165, _56167], [327 ^ [], 325 ^ []]]))).
% 0.34/1.38 %-----------------------------------------------------
% 0.34/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------