%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO193+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n011.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:09 EDT 2023
% Result : Theorem 0.58s 1.37s
% Output : Proof 0.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GEO193+3 : TPTP v8.1.2. Released v4.0.0.
% 0.12/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n011.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:07:33 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.58/1.37
% 0.58/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.58/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.58/1.37 %-----------------------------------------------------
% 0.58/1.37 ncf(matrix, plain, [(329 ^ _51400) ^ [] : [-(convergent_lines(325 ^ [], 326 ^ []))], (331 ^ _51400) ^ [] : [-(convergent_lines(327 ^ [], 326 ^ []))], (333 ^ _51400) ^ [] : [-(convergent_lines(325 ^ [], 327 ^ []))], (335 ^ _51400) ^ [] : [-(apart_point_and_line(intersection_point(325 ^ [], 326 ^ []), 327 ^ []))], (337 ^ _51400) ^ [] : [apart_point_and_line(intersection_point(327 ^ [], 326 ^ []), 325 ^ [])], (2 ^ _51400) ^ [_51503] : [distinct_points(_51503, _51503)], (4 ^ _51400) ^ [_51580] : [distinct_lines(_51580, _51580)], (6 ^ _51400) ^ [_51657] : [convergent_lines(_51657, _51657)], (8 ^ _51400) ^ [_51778, _51780, _51782] : [distinct_points(_51782, _51780), -(distinct_points(_51782, _51778)), -(distinct_points(_51780, _51778))], (18 ^ _51400) ^ [_52102, _52104, _52106] : [distinct_lines(_52106, _52104), -(distinct_lines(_52106, _52102)), -(distinct_lines(_52104, _52102))], (28 ^ _51400) ^ [_52426, _52428, _52430] : [convergent_lines(_52430, _52428), -(convergent_lines(_52430, _52426)), -(convergent_lines(_52428, _52426))], (38 ^ _51400) ^ [_52736, _52738] : [distinct_points(_52738, _52736), apart_point_and_line(_52738, line_connecting(_52738, _52736))], (44 ^ _51400) ^ [_52953, _52955] : [distinct_points(_52955, _52953), apart_point_and_line(_52953, line_connecting(_52955, _52953))], (50 ^ _51400) ^ [_53170, _53172] : [convergent_lines(_53172, _53170), apart_point_and_line(intersection_point(_53172, _53170), _53172)], (56 ^ _51400) ^ [_53387, _53389] : [convergent_lines(_53389, _53387), apart_point_and_line(intersection_point(_53389, _53387), _53387)], (62 ^ _51400) ^ [_53632, _53634, _53636, _53638] : [distinct_points(_53638, _53636), distinct_lines(_53634, _53632), -(apart_point_and_line(_53638, _53634)), -(apart_point_and_line(_53638, _53632)), -(apart_point_and_line(_53636, _53634)), -(apart_point_and_line(_53636, _53632))], (84 ^ _51400) ^ [_54261, _54263, _54265] : [apart_point_and_line(_54265, _54263), -(distinct_points(_54265, _54261)), -(apart_point_and_line(_54261, _54263))], (94 ^ _51400) ^ [_54585, _54587, _54589] : [apart_point_and_line(_54589, _54587), -(distinct_lines(_54587, _54585)), -(apart_point_and_line(_54589, _54585))], (104 ^ _51400) ^ [_54889, _54891, _54893] : [convergent_lines(_54893, _54891), -(distinct_lines(_54891, _54889)), -(convergent_lines(_54893, _54889))], (114 ^ _51400) ^ [_55225, _55227] : [distinct_lines(_55227, _55225), -(convergent_lines(_55227, _55225))], (120 ^ _51400) ^ [_55439, _55441] : [convergent_lines(parallel_through_point(_55439, _55441), _55439)], (122 ^ _51400) ^ [_55535, _55537] : [apart_point_and_line(_55537, parallel_through_point(_55535, _55537))], (124 ^ _51400) ^ [_55641, _55643, _55645] : [distinct_lines(_55643, _55641), -(apart_point_and_line(_55645, _55643)), -(apart_point_and_line(_55645, _55641)), -(convergent_lines(_55643, _55641))], (138 ^ _51400) ^ [_56069, _56071] : [-(convergent_lines(_56071, _56069)), -(unorthogonal_lines(_56071, _56069))], (144 ^ _51400) ^ [_56294, _56296, _56298] : [convergent_lines(_56298, _56296), unorthogonal_lines(_56298, _56296), 153 ^ _51400 : [(154 ^ _51400) ^ [] : [-(convergent_lines(_56298, _56294))], (156 ^ _51400) ^ [] : [-(unorthogonal_lines(_56298, _56294))]], 157 ^ _51400 : [(158 ^ _51400) ^ [] : [-(convergent_lines(_56296, _56294))], (160 ^ _51400) ^ [] : [-(unorthogonal_lines(_56296, _56294))]]], (162 ^ _51400) ^ [_56837, _56839] : [unorthogonal_lines(orthogonal_through_point(_56837, _56839), _56837)], (164 ^ _51400) ^ [_56933, _56935] : [apart_point_and_line(_56935, orthogonal_through_point(_56933, _56935))], (166 ^ _51400) ^ [_57053, _57055, _57057, _57059] : [distinct_lines(_57057, _57055), -(apart_point_and_line(_57059, _57057)), -(apart_point_and_line(_57059, _57055)), -(unorthogonal_lines(_57057, _57053)), -(unorthogonal_lines(_57055, _57053))], (184 ^ _51400) ^ [_57597, _57599] : [-(convergent_lines(_57599, _57597)), -(unorthogonal_lines(_57599, _57597))], (208 ^ _51400) ^ [_58391, _58393, _58395] : [convergent_lines(_58393, _58391), -(unorthogonal_lines(_58395, _58393)), -(unorthogonal_lines(_58395, _58391))], (190 ^ _51400) ^ [_57826, _57828, _57830] : [193 ^ _51400 : [(194 ^ _51400) ^ [] : [-(convergent_lines(_57830, _57828))], (196 ^ _51400) ^ [] : [-(unorthogonal_lines(_57830, _57828))]], 197 ^ _51400 : [(198 ^ _51400) ^ [] : [-(convergent_lines(_57830, _57826))], (200 ^ _51400) ^ [] : [-(unorthogonal_lines(_57830, _57826))]], convergent_lines(_57828, _57826), unorthogonal_lines(_57828, _57826)], (218 ^ _51400) ^ [_58731, _58733] : [-(line(line_connecting(_58733, _58731))), point(_58733), point(_58731), distinct_points(_58733, _58731)], (232 ^ _51400) ^ [_59119, _59121] : [-(point(intersection_point(_59121, _59119))), line(_59121), line(_59119), convergent_lines(_59121, _59119)], (246 ^ _51400) ^ [_59507, _59509] : [-(line(parallel_through_point(_59509, _59507))), line(_59509), point(_59507)], (256 ^ _51400) ^ [_59786, _59788] : [-(line(orthogonal_through_point(_59788, _59786))), line(_59788), point(_59786)], (266 ^ _51400) ^ [_60120, _60122] : [equal_points(_60122, _60120), distinct_points(_60122, _60120)], (272 ^ _51400) ^ [_60283, _60285] : [-(distinct_points(_60285, _60283)), -(equal_points(_60285, _60283))], (278 ^ _51400) ^ [_60527, _60529] : [equal_lines(_60529, _60527), distinct_lines(_60529, _60527)], (284 ^ _51400) ^ [_60690, _60692] : [-(distinct_lines(_60692, _60690)), -(equal_lines(_60692, _60690))], (290 ^ _51400) ^ [_60934, _60936] : [parallel_lines(_60936, _60934), convergent_lines(_60936, _60934)], (296 ^ _51400) ^ [_61097, _61099] : [-(convergent_lines(_61099, _61097)), -(parallel_lines(_61099, _61097))], (302 ^ _51400) ^ [_61341, _61343] : [incident_point_and_line(_61343, _61341), apart_point_and_line(_61343, _61341)], (308 ^ _51400) ^ [_61504, _61506] : [-(apart_point_and_line(_61506, _61504)), -(incident_point_and_line(_61506, _61504))], (314 ^ _51400) ^ [_61728, _61730] : [orthogonal_lines(_61730, _61728), unorthogonal_lines(_61730, _61728)], (320 ^ _51400) ^ [_61891, _61893] : [-(unorthogonal_lines(_61893, _61891)), -(orthogonal_lines(_61893, _61891))]], input).
% 0.58/1.37 ncf('1',plain,[convergent_lines(325 ^ [], 325 ^ [])],start(6 ^ 0,bind([[_51657], [325 ^ []]]))).
% 0.58/1.37 ncf('1.1',plain,[-(convergent_lines(325 ^ [], 325 ^ [])), convergent_lines(325 ^ [], 326 ^ []), -(distinct_lines(326 ^ [], 325 ^ []))],extension(104 ^ 1,bind([[_54889, _54891, _54893], [325 ^ [], 326 ^ [], 325 ^ []]]))).
% 0.58/1.37 ncf('1.1.1',plain,[-(convergent_lines(325 ^ [], 326 ^ []))],extension(329 ^ 2)).
% 0.58/1.37 ncf('1.1.2',plain,[distinct_lines(326 ^ [], 325 ^ []), distinct_points(intersection_point(325 ^ [], 326 ^ []), intersection_point(327 ^ [], 326 ^ [])), -(apart_point_and_line(intersection_point(325 ^ [], 326 ^ []), 326 ^ [])), -(apart_point_and_line(intersection_point(325 ^ [], 326 ^ []), 325 ^ [])), -(apart_point_and_line(intersection_point(327 ^ [], 326 ^ []), 326 ^ [])), -(apart_point_and_line(intersection_point(327 ^ [], 326 ^ []), 325 ^ []))],extension(62 ^ 2,bind([[_53632, _53634, _53636, _53638], [325 ^ [], 326 ^ [], intersection_point(327 ^ [], 326 ^ []), intersection_point(325 ^ [], 326 ^ [])]]))).
% 0.58/1.37 ncf('1.1.2.1',plain,[-(distinct_points(intersection_point(325 ^ [], 326 ^ []), intersection_point(327 ^ [], 326 ^ []))), apart_point_and_line(intersection_point(325 ^ [], 326 ^ []), 327 ^ []), -(apart_point_and_line(intersection_point(327 ^ [], 326 ^ []), 327 ^ []))],extension(84 ^ 3,bind([[_54261, _54263, _54265], [intersection_point(327 ^ [], 326 ^ []), 327 ^ [], intersection_point(325 ^ [], 326 ^ [])]]))).
% 0.58/1.37 ncf('1.1.2.1.1',plain,[-(apart_point_and_line(intersection_point(325 ^ [], 326 ^ []), 327 ^ []))],extension(335 ^ 4)).
% 0.58/1.37 ncf('1.1.2.1.2',plain,[apart_point_and_line(intersection_point(327 ^ [], 326 ^ []), 327 ^ []), convergent_lines(327 ^ [], 326 ^ [])],extension(50 ^ 4,bind([[_53170, _53172], [326 ^ [], 327 ^ []]]))).
% 0.58/1.37 ncf('1.1.2.1.2.1',plain,[-(convergent_lines(327 ^ [], 326 ^ []))],extension(331 ^ 5)).
% 0.58/1.37 ncf('1.1.2.2',plain,[apart_point_and_line(intersection_point(325 ^ [], 326 ^ []), 326 ^ []), convergent_lines(325 ^ [], 326 ^ [])],extension(56 ^ 3,bind([[_53387, _53389], [326 ^ [], 325 ^ []]]))).
% 0.58/1.37 ncf('1.1.2.2.1',plain,[-(convergent_lines(325 ^ [], 326 ^ []))],lemmata('[1].x')).
% 0.58/1.37 ncf('1.1.2.3',plain,[apart_point_and_line(intersection_point(325 ^ [], 326 ^ []), 325 ^ []), convergent_lines(325 ^ [], 326 ^ [])],extension(50 ^ 3,bind([[_53170, _53172], [326 ^ [], 325 ^ []]]))).
% 0.58/1.37 ncf('1.1.2.3.1',plain,[-(convergent_lines(325 ^ [], 326 ^ []))],lemmata('[1].x')).
% 0.58/1.37 ncf('1.1.2.4',plain,[apart_point_and_line(intersection_point(327 ^ [], 326 ^ []), 326 ^ []), convergent_lines(327 ^ [], 326 ^ [])],extension(56 ^ 3,bind([[_53387, _53389], [326 ^ [], 327 ^ []]]))).
% 0.58/1.37 ncf('1.1.2.4.1',plain,[-(convergent_lines(327 ^ [], 326 ^ []))],extension(331 ^ 4)).
% 0.58/1.37 ncf('1.1.2.5',plain,[apart_point_and_line(intersection_point(327 ^ [], 326 ^ []), 325 ^ [])],extension(337 ^ 3)).
% 0.58/1.37 %-----------------------------------------------------
% 0.58/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------