%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO194+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:09 EDT 2023
% Result : Theorem 0.36s 1.37s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO194+3 : TPTP v8.1.2. Released v4.0.0.
% 0.07/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.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri May 19 04:15:20 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.36/1.37
% 0.36/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.36/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 ncf(matrix, plain, [(329 ^ _51526) ^ [] : [-(convergent_lines(325 ^ [], 326 ^ []))], (331 ^ _51526) ^ [] : [-(convergent_lines(327 ^ [], 326 ^ []))], (333 ^ _51526) ^ [] : [-(convergent_lines(325 ^ [], 327 ^ []))], (335 ^ _51526) ^ [] : [-(apart_point_and_line(intersection_point(325 ^ [], 326 ^ []), 327 ^ []))], (337 ^ _51526) ^ [] : [apart_point_and_line(intersection_point(325 ^ [], 327 ^ []), 326 ^ [])], (2 ^ _51526) ^ [_51629] : [distinct_points(_51629, _51629)], (4 ^ _51526) ^ [_51706] : [distinct_lines(_51706, _51706)], (6 ^ _51526) ^ [_51783] : [convergent_lines(_51783, _51783)], (8 ^ _51526) ^ [_51904, _51906, _51908] : [distinct_points(_51908, _51906), -(distinct_points(_51908, _51904)), -(distinct_points(_51906, _51904))], (18 ^ _51526) ^ [_52228, _52230, _52232] : [distinct_lines(_52232, _52230), -(distinct_lines(_52232, _52228)), -(distinct_lines(_52230, _52228))], (28 ^ _51526) ^ [_52552, _52554, _52556] : [convergent_lines(_52556, _52554), -(convergent_lines(_52556, _52552)), -(convergent_lines(_52554, _52552))], (38 ^ _51526) ^ [_52862, _52864] : [distinct_points(_52864, _52862), apart_point_and_line(_52864, line_connecting(_52864, _52862))], (44 ^ _51526) ^ [_53079, _53081] : [distinct_points(_53081, _53079), apart_point_and_line(_53079, line_connecting(_53081, _53079))], (50 ^ _51526) ^ [_53296, _53298] : [convergent_lines(_53298, _53296), apart_point_and_line(intersection_point(_53298, _53296), _53298)], (56 ^ _51526) ^ [_53513, _53515] : [convergent_lines(_53515, _53513), apart_point_and_line(intersection_point(_53515, _53513), _53513)], (62 ^ _51526) ^ [_53758, _53760, _53762, _53764] : [distinct_points(_53764, _53762), distinct_lines(_53760, _53758), -(apart_point_and_line(_53764, _53760)), -(apart_point_and_line(_53764, _53758)), -(apart_point_and_line(_53762, _53760)), -(apart_point_and_line(_53762, _53758))], (84 ^ _51526) ^ [_54387, _54389, _54391] : [apart_point_and_line(_54391, _54389), -(distinct_points(_54391, _54387)), -(apart_point_and_line(_54387, _54389))], (94 ^ _51526) ^ [_54711, _54713, _54715] : [apart_point_and_line(_54715, _54713), -(distinct_lines(_54713, _54711)), -(apart_point_and_line(_54715, _54711))], (104 ^ _51526) ^ [_55015, _55017, _55019] : [convergent_lines(_55019, _55017), -(distinct_lines(_55017, _55015)), -(convergent_lines(_55019, _55015))], (114 ^ _51526) ^ [_55351, _55353] : [distinct_lines(_55353, _55351), -(convergent_lines(_55353, _55351))], (120 ^ _51526) ^ [_55565, _55567] : [convergent_lines(parallel_through_point(_55565, _55567), _55565)], (122 ^ _51526) ^ [_55661, _55663] : [apart_point_and_line(_55663, parallel_through_point(_55661, _55663))], (124 ^ _51526) ^ [_55767, _55769, _55771] : [distinct_lines(_55769, _55767), -(apart_point_and_line(_55771, _55769)), -(apart_point_and_line(_55771, _55767)), -(convergent_lines(_55769, _55767))], (138 ^ _51526) ^ [_56195, _56197] : [-(convergent_lines(_56197, _56195)), -(unorthogonal_lines(_56197, _56195))], (144 ^ _51526) ^ [_56420, _56422, _56424] : [convergent_lines(_56424, _56422), unorthogonal_lines(_56424, _56422), 153 ^ _51526 : [(154 ^ _51526) ^ [] : [-(convergent_lines(_56424, _56420))], (156 ^ _51526) ^ [] : [-(unorthogonal_lines(_56424, _56420))]], 157 ^ _51526 : [(158 ^ _51526) ^ [] : [-(convergent_lines(_56422, _56420))], (160 ^ _51526) ^ [] : [-(unorthogonal_lines(_56422, _56420))]]], (162 ^ _51526) ^ [_56963, _56965] : [unorthogonal_lines(orthogonal_through_point(_56963, _56965), _56963)], (164 ^ _51526) ^ [_57059, _57061] : [apart_point_and_line(_57061, orthogonal_through_point(_57059, _57061))], (166 ^ _51526) ^ [_57179, _57181, _57183, _57185] : [distinct_lines(_57183, _57181), -(apart_point_and_line(_57185, _57183)), -(apart_point_and_line(_57185, _57181)), -(unorthogonal_lines(_57183, _57179)), -(unorthogonal_lines(_57181, _57179))], (184 ^ _51526) ^ [_57723, _57725] : [-(convergent_lines(_57725, _57723)), -(unorthogonal_lines(_57725, _57723))], (208 ^ _51526) ^ [_58517, _58519, _58521] : [convergent_lines(_58519, _58517), -(unorthogonal_lines(_58521, _58519)), -(unorthogonal_lines(_58521, _58517))], (190 ^ _51526) ^ [_57952, _57954, _57956] : [193 ^ _51526 : [(194 ^ _51526) ^ [] : [-(convergent_lines(_57956, _57954))], (196 ^ _51526) ^ [] : [-(unorthogonal_lines(_57956, _57954))]], 197 ^ _51526 : [(198 ^ _51526) ^ [] : [-(convergent_lines(_57956, _57952))], (200 ^ _51526) ^ [] : [-(unorthogonal_lines(_57956, _57952))]], convergent_lines(_57954, _57952), unorthogonal_lines(_57954, _57952)], (218 ^ _51526) ^ [_58857, _58859] : [-(line(line_connecting(_58859, _58857))), point(_58859), point(_58857), distinct_points(_58859, _58857)], (232 ^ _51526) ^ [_59245, _59247] : [-(point(intersection_point(_59247, _59245))), line(_59247), line(_59245), convergent_lines(_59247, _59245)], (246 ^ _51526) ^ [_59633, _59635] : [-(line(parallel_through_point(_59635, _59633))), line(_59635), point(_59633)], (256 ^ _51526) ^ [_59912, _59914] : [-(line(orthogonal_through_point(_59914, _59912))), line(_59914), point(_59912)], (266 ^ _51526) ^ [_60246, _60248] : [equal_points(_60248, _60246), distinct_points(_60248, _60246)], (272 ^ _51526) ^ [_60409, _60411] : [-(distinct_points(_60411, _60409)), -(equal_points(_60411, _60409))], (278 ^ _51526) ^ [_60653, _60655] : [equal_lines(_60655, _60653), distinct_lines(_60655, _60653)], (284 ^ _51526) ^ [_60816, _60818] : [-(distinct_lines(_60818, _60816)), -(equal_lines(_60818, _60816))], (290 ^ _51526) ^ [_61060, _61062] : [parallel_lines(_61062, _61060), convergent_lines(_61062, _61060)], (296 ^ _51526) ^ [_61223, _61225] : [-(convergent_lines(_61225, _61223)), -(parallel_lines(_61225, _61223))], (302 ^ _51526) ^ [_61467, _61469] : [incident_point_and_line(_61469, _61467), apart_point_and_line(_61469, _61467)], (308 ^ _51526) ^ [_61630, _61632] : [-(apart_point_and_line(_61632, _61630)), -(incident_point_and_line(_61632, _61630))], (314 ^ _51526) ^ [_61854, _61856] : [orthogonal_lines(_61856, _61854), unorthogonal_lines(_61856, _61854)], (320 ^ _51526) ^ [_62017, _62019] : [-(unorthogonal_lines(_62019, _62017)), -(orthogonal_lines(_62019, _62017))]], input).
% 0.36/1.37 ncf('1',plain,[apart_point_and_line(intersection_point(325 ^ [], 327 ^ []), 326 ^ [])],start(337 ^ 0)).
% 0.36/1.37 ncf('1.1',plain,[-(apart_point_and_line(intersection_point(325 ^ [], 327 ^ []), 326 ^ [])), distinct_points(intersection_point(325 ^ [], 326 ^ []), intersection_point(325 ^ [], 327 ^ [])), distinct_lines(326 ^ [], 325 ^ []), -(apart_point_and_line(intersection_point(325 ^ [], 326 ^ []), 326 ^ [])), -(apart_point_and_line(intersection_point(325 ^ [], 326 ^ []), 325 ^ [])), -(apart_point_and_line(intersection_point(325 ^ [], 327 ^ []), 325 ^ []))],extension(62 ^ 1,bind([[_53758, _53760, _53762, _53764], [325 ^ [], 326 ^ [], intersection_point(325 ^ [], 327 ^ []), intersection_point(325 ^ [], 326 ^ [])]]))).
% 0.36/1.37 ncf('1.1.1',plain,[-(distinct_points(intersection_point(325 ^ [], 326 ^ []), intersection_point(325 ^ [], 327 ^ []))), apart_point_and_line(intersection_point(325 ^ [], 326 ^ []), 327 ^ []), -(apart_point_and_line(intersection_point(325 ^ [], 327 ^ []), 327 ^ []))],extension(84 ^ 2,bind([[_54387, _54389, _54391], [intersection_point(325 ^ [], 327 ^ []), 327 ^ [], intersection_point(325 ^ [], 326 ^ [])]]))).
% 0.36/1.37 ncf('1.1.1.1',plain,[-(apart_point_and_line(intersection_point(325 ^ [], 326 ^ []), 327 ^ []))],extension(335 ^ 3)).
% 0.36/1.37 ncf('1.1.1.2',plain,[apart_point_and_line(intersection_point(325 ^ [], 327 ^ []), 327 ^ []), convergent_lines(325 ^ [], 327 ^ [])],extension(56 ^ 3,bind([[_53513, _53515], [327 ^ [], 325 ^ []]]))).
% 0.36/1.37 ncf('1.1.1.2.1',plain,[-(convergent_lines(325 ^ [], 327 ^ []))],extension(333 ^ 4)).
% 0.36/1.37 ncf('1.1.2',plain,[-(distinct_lines(326 ^ [], 325 ^ [])), convergent_lines(325 ^ [], 326 ^ []), -(convergent_lines(325 ^ [], 325 ^ []))],extension(104 ^ 2,bind([[_55015, _55017, _55019], [325 ^ [], 326 ^ [], 325 ^ []]]))).
% 0.36/1.37 ncf('1.1.2.1',plain,[-(convergent_lines(325 ^ [], 326 ^ []))],extension(329 ^ 3)).
% 0.36/1.37 ncf('1.1.2.2',plain,[convergent_lines(325 ^ [], 325 ^ [])],extension(6 ^ 3,bind([[_51783], [325 ^ []]]))).
% 0.36/1.37 ncf('1.1.3',plain,[apart_point_and_line(intersection_point(325 ^ [], 326 ^ []), 326 ^ []), convergent_lines(325 ^ [], 326 ^ [])],extension(56 ^ 2,bind([[_53513, _53515], [326 ^ [], 325 ^ []]]))).
% 0.36/1.37 ncf('1.1.3.1',plain,[-(convergent_lines(325 ^ [], 326 ^ []))],extension(329 ^ 3)).
% 0.36/1.37 ncf('1.1.4',plain,[apart_point_and_line(intersection_point(325 ^ [], 326 ^ []), 325 ^ []), convergent_lines(325 ^ [], 326 ^ [])],extension(50 ^ 2,bind([[_53296, _53298], [326 ^ [], 325 ^ []]]))).
% 0.36/1.37 ncf('1.1.4.1',plain,[-(convergent_lines(325 ^ [], 326 ^ []))],extension(329 ^ 3)).
% 0.36/1.37 ncf('1.1.5',plain,[apart_point_and_line(intersection_point(325 ^ [], 327 ^ []), 325 ^ []), convergent_lines(325 ^ [], 327 ^ [])],extension(50 ^ 2,bind([[_53296, _53298], [327 ^ [], 325 ^ []]]))).
% 0.36/1.37 ncf('1.1.5.1',plain,[-(convergent_lines(325 ^ [], 327 ^ []))],extension(333 ^ 3)).
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------